[STATEMENT]
lemma (in category) cat_ntcf_rcomp_Hom_ntcf_id:
  assumes "\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>(-,ntcf_id \<FF>-) = ntcf_id Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(-,\<FF>-)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>(-,ntcf_id \<FF>-) = ntcf_id Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(-,\<FF>-)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>(-,ntcf_id \<FF>-) = ntcf_id Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(-,\<FF>-)
[PROOF STEP]
interpret \<FF>: is_functor \<alpha> \<BB> \<CC> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>(-,ntcf_id \<FF>-) = ntcf_id Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(-,\<FF>-)
[PROOF STEP]
from category_axioms assms
[PROOF STATE]
proof (chain)
picking this:
category \<alpha> \<CC>
\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
category \<alpha> \<CC>
\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>(-,ntcf_id \<FF>-) = ntcf_id Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(-,\<FF>-)
[PROOF STEP]
unfolding ntcf_rcomp_Hom_def ntcf_id_components \<FF>.cf_HomCod
[PROOF STATE]
proof (prove)
using this:
category \<alpha> \<CC>
\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>(ntcf_id (dghm_id \<CC>)-,ntcf_id \<FF>-) = ntcf_id Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(-,\<FF>-)
[PROOF STEP]
by (cs_concl cs_simp: ntcf_rcomp_Hom_def cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>(-,ntcf_id \<FF>-) = ntcf_id Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(-,\<FF>-)

goal:
No subgoals!
[PROOF STEP]
qed