proposition: Lemma Fun_prod_map_law : Map_law Fun_prod_mor.
proof: Proof. unfold Map_law in |- *; intros f g H. unfold Fun_prod_mor, Mor_prod in |- *. apply (Map2_r (Op_together (C1 c2 a) _) (a1:=H_proj1_prod C1 c1 a o f) (a2:=H_proj1_prod C1 c1 a o g) (H_proj2_prod C1 c1 a o Id a)). apply Comp_l; trivial. Qed.
imports: Binary_Products Functor