proposition: Lemma Eq3_prod : forall (C : Category) (a b : C) (C1 : BinProd a b) (c : C) (f : c --> a) (g : c --> b) (c' : C) (k : c' --> c), k o Together C1 f g =_S Together C1 (k o f) (k o g).
proof: Proof. intros C a b C1 c f g c' k. apply Trans with (Together C1 ((k o Together C1 f g) o Proj1_prod C1) ((k o Together C1 f g) o Proj2_prod C1)). apply Sym. apply (Prf_unique_together (k o Together C1 f g)). apply Trans with (Together C1 (k o f) ((k o Together C1 f g) o Proj2_prod C1)). apply (Prf_map2_congr (Op_together C1 _) (a1:=(k o Together C1 f g) o Proj1_prod C1) (a2:= k o f) ((k o Together C1 f g) o Proj2_prod C1)). apply Trans with (k o Together C1 f g o Proj1_prod C1). apply Ass1. apply Comp_l. apply (Prf_eq1_prod C1 f g). apply (Prf_map2_congl (Op_together C1 _) (b1:=(k o Together C1 f g) o Proj2_prod C1) (b2:= k o g) (k o f)). apply Trans with (k o Together C1 f g o Proj2_prod C1). apply Ass1. apply Comp_l; apply (Prf_eq2_prod C1 f g). Qed.
imports: Category Map2