let x1, x2 be set ; :: thesis: for C being Category
for c being Object of C
for p1, p2 being Morphism of C st x1 <> x2 holds
( c is_a_product_wrt p1,p2 iff c is_a_product_wrt (x1,x2) --> (p1,p2) )

let C be Category; :: thesis: for c being Object of C
for p1, p2 being Morphism of C st x1 <> x2 holds
( c is_a_product_wrt p1,p2 iff c is_a_product_wrt (x1,x2) --> (p1,p2) )

let c be Object of C; :: thesis: for p1, p2 being Morphism of C st x1 <> x2 holds
( c is_a_product_wrt p1,p2 iff c is_a_product_wrt (x1,x2) --> (p1,p2) )

let p1, p2 be Morphism of C; :: thesis: ( x1 <> x2 implies ( c is_a_product_wrt p1,p2 iff c is_a_product_wrt (x1,x2) --> (p1,p2) ) )
set F = (x1,x2) --> (p1,p2);
set I = {x1,x2};
assume A1: x1 <> x2 ; :: thesis: ( c is_a_product_wrt p1,p2 iff c is_a_product_wrt (x1,x2) --> (p1,p2) )
thus ( c is_a_product_wrt p1,p2 implies c is_a_product_wrt (x1,x2) --> (p1,p2) ) :: thesis: ( c is_a_product_wrt (x1,x2) --> (p1,p2) implies c is_a_product_wrt p1,p2 )
proof
assume A2: c is_a_product_wrt p1,p2 ; :: thesis: c is_a_product_wrt (x1,x2) --> (p1,p2)
then ( dom p1 = c & dom p2 = c ) ;
hence (x1,x2) --> (p1,p2) is Projections_family of c,{x1,x2} by Th44; :: according to CAT_3:def 14 :: thesis: for b being Object of C
for F9 being Projections_family of b,{x1,x2} st cods ((x1,x2) --> (p1,p2)) = cods F9 holds
ex h being Morphism of C st
( h in Hom (b,c) & ( for k being Morphism of C st k in Hom (b,c) holds
( ( for x being set st x in {x1,x2} holds
(((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x ) iff h = k ) ) )

let b be Object of C; :: thesis: for F9 being Projections_family of b,{x1,x2} st cods ((x1,x2) --> (p1,p2)) = cods F9 holds
ex h being Morphism of C st
( h in Hom (b,c) & ( for k being Morphism of C st k in Hom (b,c) holds
( ( for x being set st x in {x1,x2} holds
(((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x ) iff h = k ) ) )

let F9 be Projections_family of b,{x1,x2}; :: thesis: ( cods ((x1,x2) --> (p1,p2)) = cods F9 implies ex h being Morphism of C st
( h in Hom (b,c) & ( for k being Morphism of C st k in Hom (b,c) holds
( ( for x being set st x in {x1,x2} holds
(((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x ) iff h = k ) ) ) )

assume A3: cods ((x1,x2) --> (p1,p2)) = cods F9 ; :: thesis: ex h being Morphism of C st
( h in Hom (b,c) & ( for k being Morphism of C st k in Hom (b,c) holds
( ( for x being set st x in {x1,x2} holds
(((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x ) iff h = k ) ) )

set f = F9 /. x1;
set g = F9 /. x2;
A4: x1 in {x1,x2} by TARSKI:def 2;
then (cods ((x1,x2) --> (p1,p2))) /. x1 = cod (((x1,x2) --> (p1,p2)) /. x1) by Def2;
then cod (F9 /. x1) = cod (((x1,x2) --> (p1,p2)) /. x1) by A3, A4, Def2;
then A5: cod (F9 /. x1) = cod p1 by ;
A6: x2 in {x1,x2} by TARSKI:def 2;
then (cods ((x1,x2) --> (p1,p2))) /. x2 = cod (((x1,x2) --> (p1,p2)) /. x2) by Def2;
then cod (F9 /. x2) = cod (((x1,x2) --> (p1,p2)) /. x2) by A3, A6, Def2;
then A7: cod (F9 /. x2) = cod p2 by ;
dom (F9 /. x2) = b by ;
then A8: F9 /. x2 in Hom (b,(cod p2)) by A7;
dom (F9 /. x1) = b by ;
then F9 /. x1 in Hom (b,(cod p1)) by A5;
then consider h being Morphism of C such that
A9: h in Hom (b,c) and
A10: for k being Morphism of C st k in Hom (b,c) holds
( ( p1 (*) k = F9 /. x1 & p2 (*) k = F9 /. x2 ) iff h = k ) by A2, A8;
take h ; :: thesis: ( h in Hom (b,c) & ( for k being Morphism of C st k in Hom (b,c) holds
( ( for x being set st x in {x1,x2} holds
(((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x ) iff h = k ) ) )

thus h in Hom (b,c) by A9; :: thesis: for k being Morphism of C st k in Hom (b,c) holds
( ( for x being set st x in {x1,x2} holds
(((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x ) iff h = k )

let k be Morphism of C; :: thesis: ( k in Hom (b,c) implies ( ( for x being set st x in {x1,x2} holds
(((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x ) iff h = k ) )

assume A11: k in Hom (b,c) ; :: thesis: ( ( for x being set st x in {x1,x2} holds
(((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x ) iff h = k )

thus ( ( for x being set st x in {x1,x2} holds
(((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x ) implies h = k ) :: thesis: ( h = k implies for x being set st x in {x1,x2} holds
(((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x )
proof
assume A12: for x being set st x in {x1,x2} holds
(((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x ; :: thesis: h = k
then (((x1,x2) --> (p1,p2)) /. x2) (*) k = F9 /. x2 by A6;
then A13: p2 (*) k = F9 /. x2 by ;
(((x1,x2) --> (p1,p2)) /. x1) (*) k = F9 /. x1 by ;
then p1 (*) k = F9 /. x1 by ;
hence h = k by ; :: thesis: verum
end;
assume h = k ; :: thesis: for x being set st x in {x1,x2} holds
(((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x

then A14: ( p1 (*) k = F9 /. x1 & p2 (*) k = F9 /. x2 ) by ;
let x be set ; :: thesis: ( x in {x1,x2} implies (((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x )
assume x in {x1,x2} ; :: thesis: (((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x
then ( x = x1 or x = x2 ) by TARSKI:def 2;
hence (((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x by A1, A14, Th3; :: thesis: verum
end;
assume A15: c is_a_product_wrt (x1,x2) --> (p1,p2) ; :: thesis: c is_a_product_wrt p1,p2
then A16: (x1,x2) --> (p1,p2) is Projections_family of c,{x1,x2} ;
x2 in {x1,x2} by TARSKI:def 2;
then A17: dom (((x1,x2) --> (p1,p2)) /. x2) = c by ;
x1 in {x1,x2} by TARSKI:def 2;
then dom (((x1,x2) --> (p1,p2)) /. x1) = c by ;
hence ( dom p1 = c & dom p2 = c ) by A1, A17, Th3; :: according to CAT_3:def 15 :: thesis: for d being Object of C
for f, g being Morphism of C st f in Hom (d,(cod p1)) & g in Hom (d,(cod p2)) holds
ex h being Morphism of C st
( h in Hom (d,c) & ( for k being Morphism of C st k in Hom (d,c) holds
( ( p1 (*) k = f & p2 (*) k = g ) iff h = k ) ) )

let d be Object of C; :: thesis: for f, g being Morphism of C st f in Hom (d,(cod p1)) & g in Hom (d,(cod p2)) holds
ex h being Morphism of C st
( h in Hom (d,c) & ( for k being Morphism of C st k in Hom (d,c) holds
( ( p1 (*) k = f & p2 (*) k = g ) iff h = k ) ) )

let f, g be Morphism of C; :: thesis: ( f in Hom (d,(cod p1)) & g in Hom (d,(cod p2)) implies ex h being Morphism of C st
( h in Hom (d,c) & ( for k being Morphism of C st k in Hom (d,c) holds
( ( p1 (*) k = f & p2 (*) k = g ) iff h = k ) ) ) )

assume that
A18: f in Hom (d,(cod p1)) and
A19: g in Hom (d,(cod p2)) ; :: thesis: ex h being Morphism of C st
( h in Hom (d,c) & ( for k being Morphism of C st k in Hom (d,c) holds
( ( p1 (*) k = f & p2 (*) k = g ) iff h = k ) ) )

( dom f = d & dom g = d ) by ;
then reconsider F9 = (x1,x2) --> (f,g) as Projections_family of d,{x1,x2} by Th44;
cods ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((cod p1),(cod p2)) by Th7
.= (x1,x2) --> ((cod f),(cod p2)) by
.= (x1,x2) --> ((cod f),(cod g)) by
.= cods F9 by Th7 ;
then consider h being Morphism of C such that
A20: h in Hom (d,c) and
A21: for k being Morphism of C st k in Hom (d,c) holds
( ( for x being set st x in {x1,x2} holds
(((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x ) iff h = k ) by A15;
take h ; :: thesis: ( h in Hom (d,c) & ( for k being Morphism of C st k in Hom (d,c) holds
( ( p1 (*) k = f & p2 (*) k = g ) iff h = k ) ) )

thus h in Hom (d,c) by A20; :: thesis: for k being Morphism of C st k in Hom (d,c) holds
( ( p1 (*) k = f & p2 (*) k = g ) iff h = k )

let k be Morphism of C; :: thesis: ( k in Hom (d,c) implies ( ( p1 (*) k = f & p2 (*) k = g ) iff h = k ) )
assume A22: k in Hom (d,c) ; :: thesis: ( ( p1 (*) k = f & p2 (*) k = g ) iff h = k )
thus ( p1 (*) k = f & p2 (*) k = g implies h = k ) :: thesis: ( h = k implies ( p1 (*) k = f & p2 (*) k = g ) )
proof
assume A23: ( p1 (*) k = f & p2 (*) k = g ) ; :: thesis: h = k
now :: thesis: for x being set st x in {x1,x2} holds
(((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x
let x be set ; :: thesis: ( x in {x1,x2} implies (((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x )
assume x in {x1,x2} ; :: thesis: (((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x
then ( x = x1 or x = x2 ) by TARSKI:def 2;
then ( ( ((x1,x2) --> (p1,p2)) /. x = p1 & F9 /. x = f ) or ( ((x1,x2) --> (p1,p2)) /. x = p2 & F9 /. x = g ) ) by ;
hence (((x1,x2) --> (p1,p2)) /. x) (*) k = F9 /. x by A23; :: thesis: verum
end;
hence h = k by ; :: thesis: verum
end;
assume A24: h = k ; :: thesis: ( p1 (*) k = f & p2 (*) k = g )
x2 in {x1,x2} by TARSKI:def 2;
then (((x1,x2) --> (p1,p2)) /. x2) (*) k = F9 /. x2 by ;
then A25: (((x1,x2) --> (p1,p2)) /. x2) (*) k = g by ;
x1 in {x1,x2} by TARSKI:def 2;
then (((x1,x2) --> (p1,p2)) /. x1) (*) k = F9 /. x1 by ;
then (((x1,x2) --> (p1,p2)) /. x1) (*) k = f by ;
hence ( p1 (*) k = f & p2 (*) k = g ) by A1, A25, Th3; :: thesis: verum