[STATEMENT]
lemma cf_blcomp_is_functor:
  assumes "\<SS> : \<CC> \<times>\<^sub>C \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "cf_blcomp \<SS> : \<CC> \<times>\<^sub>C\<^sub>3 \<CC> \<times>\<^sub>C\<^sub>3 \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_blcomp \<SS> : \<CC>^\<^sub>C\<^sub>3 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cf_blcomp \<SS> : \<CC>^\<^sub>C\<^sub>3 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<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_blcomp \<SS> : \<CC>^\<^sub>C\<^sub>3 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_blcomp \<SS> : \<CC>^\<^sub>C\<^sub>3 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (cs_concl cs_simp: cat_cs_simps cf_blcomp_def' cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
cf_blcomp \<SS> : \<CC>^\<^sub>C\<^sub>3 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed