proposition: Lemma Eq_Mor_prod : Mor_prod f f' o Mor_prod g g' =_S Mor_prod (f o g) (f' o g').
proof: Proof. unfold Mor_prod, H_together in |- *. apply Trans with (Together (C1 c c') (Together (C1 b b') (Proj1_prod (C1 a a') o f) (Proj2_prod (C1 a a') o f') o Proj1_prod (C1 b b') o g) (Together (C1 b b') (Proj1_prod (C1 a a') o f) (Proj2_prod (C1 a a') o f') o Proj2_prod (C1 b b') o g')). apply Eq3_prod. apply Trans with (Together (C1 c c') (Proj1_prod (C1 a a') o f o g) (Together (C1 b b') (Proj1_prod (C1 a a') o f) (Proj2_prod (C1 a a') o f') o Proj2_prod (C1 b b') o g')). unfold Together, Together_prod in |- *; apply Map2_r. apply Trans with ((Together (C1 b b') (Proj1_prod (C1 a a') o f) (Proj2_prod (C1 a a') o f') o Proj1_prod (C1 b b')) o g). apply Ass. apply Trans with ((Proj1_prod (C1 a a') o f) o g). apply Comp_r. apply (Prf_eq1_prod (C1 b b') (Proj1_prod (C1 a a') o f) (Proj2_prod (C1 a a') o f')). apply Ass1. unfold Together, Together_prod in |- *; apply Map2_l. apply Trans with ((Together (C1 b b') (Proj1_prod (C1 a a') o f) (Proj2_prod (C1 a a') o f') o Proj2_prod (C1 b b')) o g'). apply Ass. apply Trans with ((Proj2_prod (C1 a a') o f') o g'). apply Comp_r. apply (Prf_eq2_prod (C1 b b') (Proj1_prod (C1 a a') o f) (Proj2_prod (C1 a a') o f')). apply Ass1. Qed.
imports: Category Map2