[STATEMENT]
lemma cf_brcomp_def':
  assumes "\<SS> : \<CC> \<times>\<^sub>C \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "cf_brcomp \<SS> = cf_rcomp \<CC> \<SS> \<SS> \<circ>\<^sub>C\<^sub>F cf_cat_prod_12_of_3 \<CC> \<CC> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_brcomp \<SS> = cf_rcomp \<CC> \<SS> \<SS> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_cat_prod_12_of_3 \<CC> \<CC> \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cf_brcomp \<SS> = cf_rcomp \<CC> \<SS> \<SS> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_cat_prod_12_of_3 \<CC> \<CC> \<CC>
[PROOF STEP]
interpret \<SS>: is_functor \<alpha> \<open>\<CC> \<times>\<^sub>C \<CC>\<close> \<CC> \<SS>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<SS> : \<CC> \<times>\<^sub>C \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cf_brcomp \<SS> = cf_rcomp \<CC> \<SS> \<SS> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_cat_prod_12_of_3 \<CC> \<CC> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_brcomp \<SS> = cf_rcomp \<CC> \<SS> \<SS> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_cat_prod_12_of_3 \<CC> \<CC> \<CC>
[PROOF STEP]
by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_cs_simps cf_brcomp_def cs_intro: cat_cs_intros
      )
[PROOF STATE]
proof (state)
this:
cf_brcomp \<SS> = cf_rcomp \<CC> \<SS> \<SS> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_cat_prod_12_of_3 \<CC> \<CC> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed