( not C1 is empty & not C2 is empty implies ( ex f being morphism of (C1 [x] C2) st
( (pr1 (C1,C2)) . f = f1 & (pr2 (C1,C2)) . f = f2 ) & ( for f11, f22 being morphism of (C1 [x] C2) st (pr1 (C1,C2)) . f11 = f1 & (pr2 (C1,C2)) . f11 = f2 & (pr1 (C1,C2)) . f22 = f1 & (pr2 (C1,C2)) . f22 = f2 holds
f11 = f22 ) ) )

proof

assume A1: ( not C1 is empty & not C2 is empty ) ; :: thesis: ( ex f being morphism of (C1 [x] C2) st
( (pr1 (C1,C2)) . f = f1 & (pr2 (C1,C2)) . f = f2 ) & ( for f11, f22 being morphism of (C1 [x] C2) st (pr1 (C1,C2)) . f11 = f1 & (pr2 (C1,C2)) . f11 = f2 & (pr1 (C1,C2)) . f22 = f1 & (pr2 (C1,C2)) . f22 = f2 holds
f11 = f22 ) )
reconsider D1 = C1, D2 = C2 as non empty category by A1;
reconsider g1 = f1 as morphism of D1 ;
reconsider g2 = f2 as morphism of D2 ;
D1 [x] D2, pr1 (D1,D2), pr2 (D1,D2) is_product_of D1,D2 by Th48;
then consider H being Functor of (OrdC 2),(D1 [x] D2) such that
A2: ( H is covariant & (pr1 (D1,D2)) (*) H = MORPHISM g1 & (pr2 (D1,D2)) (*) H = MORPHISM g2 & ( for H1 being Functor of (OrdC 2),(D1 [x] D2) st H1 is covariant & (pr1 (D1,D2)) (*) H1 = MORPHISM g1 & (pr2 (D1,D2)) (*) H1 = MORPHISM g2 holds
H = H1 ) ) by Def17;
consider g12 being morphism of (OrdC 2) such that
A3: ( not g12 is identity & Ob (OrdC 2) = {(dom g12),(cod g12)} & Mor (OrdC 2) = {(dom g12),(cod g12),g12} & dom g12, cod g12,g12 are_mutually_distinct ) by CAT_7:39;
reconsider f = H . g12 as morphism of (C1 [x] C2) ;
thus ex f being morphism of (C1 [x] C2) st
( (pr1 (C1,C2)) . f = f1 & (pr2 (C1,C2)) . f = f2 ) :: thesis: for f11, f22 being morphism of (C1 [x] C2) st (pr1 (C1,C2)) . f11 = f1 & (pr2 (C1,C2)) . f11 = f2 & (pr1 (C1,C2)) . f22 = f1 & (pr2 (C1,C2)) . f22 = f2 holds
f11 = f22

proof

take f ; :: thesis: ( (pr1 (C1,C2)) . f = f1 & (pr2 (C1,C2)) . f = f2 )
thus (pr1 (C1,C2)) . f = ((pr1 (D1,D2)) (*) H) . g12 by A2, CAT_6:34
.= f1 by A2, A3, CAT_7:def 16 ; :: thesis: (pr2 (C1,C2)) . f = f2
thus (pr2 (C1,C2)) . f = ((pr2 (D1,D2)) (*) H) . g12 by A2, CAT_6:34
.= f2 by A2, A3, CAT_7:def 16 ; :: thesis: verum

end;

let f11, f22 be morphism of (C1 [x] C2); :: thesis: ( (pr1 (C1,C2)) . f11 = f1 & (pr2 (C1,C2)) . f11 = f2 & (pr1 (C1,C2)) . f22 = f1 & (pr2 (C1,C2)) . f22 = f2 implies f11 = f22 )
reconsider g11 = f11 as morphism of (D1 [x] D2) ;
reconsider g22 = f22 as morphism of (D1 [x] D2) ;
assume A4: ( (pr1 (C1,C2)) . f11 = f1 & (pr2 (C1,C2)) . f11 = f2 ) ; :: thesis: ( not (pr1 (C1,C2)) . f22 = f1 or not (pr2 (C1,C2)) . f22 = f2 or f11 = f22 )
assume A5: ( (pr1 (C1,C2)) . f22 = f1 & (pr2 (C1,C2)) . f22 = f2 ) ; :: thesis: f11 = f22
set H1 = MORPHISM g11;
set H2 = MORPHISM g22;
A6: (pr1 (D1,D2)) (*) (MORPHISM g11) is covariant by CAT_6:35;
((pr1 (D1,D2)) (*) (MORPHISM g11)) . g12 = (pr1 (D1,D2)) . ((MORPHISM g11) . g12) by CAT_6:34
.= (pr1 (D1,D2)) . g11 by A3, CAT_7:def 16
.= (MORPHISM g1) . g12 by A4, A3, CAT_7:def 16 ;
then A7: (pr1 (D1,D2)) (*) (MORPHISM g11) = MORPHISM g1 by A6, A3, Th17;
A8: (pr2 (D1,D2)) (*) (MORPHISM g11) is covariant by CAT_6:35;
((pr2 (D1,D2)) (*) (MORPHISM g11)) . g12 = (pr2 (D1,D2)) . ((MORPHISM g11) . g12) by CAT_6:34
.= (pr2 (D1,D2)) . g11 by A3, CAT_7:def 16
.= (MORPHISM g2) . g12 by A4, A3, CAT_7:def 16 ;
then (pr2 (D1,D2)) (*) (MORPHISM g11) = MORPHISM g2 by A8, A3, Th17;
then A9: MORPHISM g11 = H by A7, A2;
A10: (pr1 (D1,D2)) (*) (MORPHISM g22) is covariant by CAT_6:35;
((pr1 (D1,D2)) (*) (MORPHISM g22)) . g12 = (pr1 (D1,D2)) . ((MORPHISM g22) . g12) by CAT_6:34
.= (pr1 (D1,D2)) . g22 by A3, CAT_7:def 16
.= (MORPHISM g1) . g12 by A5, A3, CAT_7:def 16 ;
then A11: (pr1 (D1,D2)) (*) (MORPHISM g22) = MORPHISM g1 by A10, A3, Th17;
A12: (pr2 (D1,D2)) (*) (MORPHISM g22) is covariant by CAT_6:35;
((pr2 (D1,D2)) (*) (MORPHISM g22)) . g12 = (pr2 (D1,D2)) . ((MORPHISM g22) . g12) by CAT_6:34
.= (pr2 (D1,D2)) . g22 by A3, CAT_7:def 16
.= (MORPHISM g2) . g12 by A5, A3, CAT_7:def 16 ;
then (pr2 (D1,D2)) (*) (MORPHISM g22) = MORPHISM g2 by A12, A3, Th17;
hence f11 = f22 by A2, A11, A9, Th16; :: thesis: verum

end;

hence ( ( for b₁ being morphism of (C1 [x] C2) holds verum ) & ( not C1 is empty & not C2 is empty implies ex b₁ being morphism of (C1 [x] C2) st
( (pr1 (C1,C2)) . b₁ = f1 & (pr2 (C1,C2)) . b₁ = f2 ) ) & ( ( C1 is empty or C2 is empty ) implies ex b₁ being morphism of (C1 [x] C2) st b₁ = the morphism of (C1 [x] C2) ) & ( for b₁, b₂ being morphism of (C1 [x] C2) holds
( ( not C1 is empty & not C2 is empty & (pr1 (C1,C2)) . b₁ = f1 & (pr2 (C1,C2)) . b₁ = f2 & (pr1 (C1,C2)) . b₂ = f1 & (pr2 (C1,C2)) . b₂ = f2 implies b₁ = b₂ ) & ( ( C1 is empty or C2 is empty ) & b₁ = the morphism of (C1 [x] C2) & b₂ = the morphism of (C1 [x] C2) implies b₁ = b₂ ) ) ) ) ; :: thesis: verum