proposition: Lemma Fun2_r_comp_law : Fcomp_law FunSET2_r_map.
proof: Proof. unfold Fcomp_law, FunSET2_r_map in |- *; simpl in |- *. unfold FunSET2_r_mor, Ext in |- *; simpl in |- *. unfold FunSET2_r_mor1, FunSET2_r_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 (((FMor F (f2 o f1) o h) o g1) o g2). apply Ass. apply Comp_r. apply Trans with ((FMor F f2 o FMor F f1 o h) o g1). apply Comp_r. apply Trans with ((FMor F f2 o FMor F f1) o h). apply Comp_r. apply FComp. apply Ass1. apply Ass1. Qed.
imports: SET Dual PROD Functor