proposition: Lemma Fun2_l_comp_law : Fcomp_law FunSET2_l_map.
proof: Proof. unfold Fcomp_law, FunSET2_l_map in |- *; simpl in |- *. unfold FunSET2_l_mor, Ext in |- *; simpl in |- *. unfold FunSET2_l_mor1, FunSET2_l_ob in |- *; simpl in |- *. intros d1xc1 d2xc2 d3xc3 f1xg1 f2xg2 h. elim f1xg1; simpl in |- *; unfold DHom in |- *; intros f1 g1. elim f2xg2; simpl in |- *; unfold DHom in |- *; intros f2 g2; simpl in |- *. apply Trans with (((f2 o f1) o h) o FMor G g1 o FMor G g2). apply Comp_l. apply FComp. apply Trans with ((((f2 o f1) o h) o FMor G g1) o FMor G g2). apply Ass. apply Comp_r. apply Trans with ((f2 o f1 o h) o FMor G g1). apply Comp_r. apply Ass1. apply Ass1. Qed.
imports: SET Dual PROD Functor