let C be Category; :: thesis: for c, a, b being Object of C st Hom c,a <> {} & Hom c,b <> {} holds
for p1 being Morphism of c,a
for p2 being Morphism of c,b holds
( c is_a_product_wrt p1,p2 iff for d being Object of C st Hom d,a <> {} & Hom d,b <> {} holds
( Hom d,c <> {} & ( for f being Morphism of d,a
for g being Morphism of d,b ex h being Morphism of d,c st
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) ) ) )
let c, a, b be Object of C; :: thesis: ( Hom c,a <> {} & Hom c,b <> {} implies for p1 being Morphism of c,a
for p2 being Morphism of c,b holds
( c is_a_product_wrt p1,p2 iff for d being Object of C st Hom d,a <> {} & Hom d,b <> {} holds
( Hom d,c <> {} & ( for f being Morphism of d,a
for g being Morphism of d,b ex h being Morphism of d,c st
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) ) ) ) )
assume that
A1: Hom c,a <> {} and
A2: Hom c,b <> {} ; :: thesis: for p1 being Morphism of c,a
for p2 being Morphism of c,b holds
( c is_a_product_wrt p1,p2 iff for d being Object of C st Hom d,a <> {} & Hom d,b <> {} holds
( Hom d,c <> {} & ( for f being Morphism of d,a
for g being Morphism of d,b ex h being Morphism of d,c st
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) ) ) )
let p1 be Morphism of c,a; :: thesis: for p2 being Morphism of c,b holds
( c is_a_product_wrt p1,p2 iff for d being Object of C st Hom d,a <> {} & Hom d,b <> {} holds
( Hom d,c <> {} & ( for f being Morphism of d,a
for g being Morphism of d,b ex h being Morphism of d,c st
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) ) ) )
let p2 be Morphism of c,b; :: thesis: ( c is_a_product_wrt p1,p2 iff for d being Object of C st Hom d,a <> {} & Hom d,b <> {} holds
( Hom d,c <> {} & ( for f being Morphism of d,a
for g being Morphism of d,b ex h being Morphism of d,c st
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) ) ) )
thus ( c is_a_product_wrt p1,p2 implies for d being Object of C st Hom d,a <> {} & Hom d,b <> {} holds
( Hom d,c <> {} & ( for f being Morphism of d,a
for g being Morphism of d,b ex h being Morphism of d,c st
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) ) ) ) :: thesis: ( ( for d being Object of C st Hom d,a <> {} & Hom d,b <> {} holds
( Hom d,c <> {} & ( for f being Morphism of d,a
for g being Morphism of d,b ex h being Morphism of d,c st
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) ) ) ) implies c is_a_product_wrt p1,p2 )

proof

assume that
dom p1 = c and
dom p2 = c and
A3: 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 ) ) ) ; :: according to CAT_3:def 16 :: thesis: for d being Object of C st Hom d,a <> {} & Hom d,b <> {} holds
( Hom d,c <> {} & ( for f being Morphism of d,a
for g being Morphism of d,b ex h being Morphism of d,c st
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) ) )
let d be Object of C; :: thesis: ( Hom d,a <> {} & Hom d,b <> {} implies ( Hom d,c <> {} & ( for f being Morphism of d,a
for g being Morphism of d,b ex h being Morphism of d,c st
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) ) ) )
assume that
A4: Hom d,a <> {} and
A5: Hom d,b <> {} ; :: thesis: ( Hom d,c <> {} & ( for f being Morphism of d,a
for g being Morphism of d,b ex h being Morphism of d,c st
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) ) )
consider f being Morphism of d,a, g being Morphism of d,b;
A6: cod p2 = b by A2, CAT_1:23;
then A7: g in Hom d,(cod p2) by A5, CAT_1:def 7;
A8: cod p1 = a by A1, CAT_1:23;
then f in Hom d,(cod p1) by A4, CAT_1:def 7;
then A9: 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 ) ) ) by A3, A7;
hence Hom d,c <> {} ; :: thesis: for f being Morphism of d,a
for g being Morphism of d,b ex h being Morphism of d,c st
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k )
let f be Morphism of d,a; :: thesis: for g being Morphism of d,b ex h being Morphism of d,c st
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k )
let g be Morphism of d,b; :: thesis: ex h being Morphism of d,c st
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k )
A10: g in Hom d,(cod p2) by A5, A6, CAT_1:def 7;
f in Hom d,(cod p1) by A4, A8, CAT_1:def 7;
then consider h being Morphism of C such that
A11: h in Hom d,c and
A12: for k being Morphism of C st k in Hom d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) by A3, A10;
reconsider h = h as Morphism of d,c by A11, CAT_1:def 7;
take h ; :: thesis: for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k )
let k be Morphism of d,c; :: thesis: ( ( p1 * k = f & p2 * k = g ) iff h = k )
A13: k in Hom d,c by A9, CAT_1:def 7;
( p1 * k = p1 * k & p2 * k = p2 * k ) by A1, A2, A9, CAT_1:def 13;
hence ( ( p1 * k = f & p2 * k = g ) iff h = k ) by A12, A13; :: thesis: verum

end;

assume A14: for d being Object of C st Hom d,a <> {} & Hom d,b <> {} holds
( Hom d,c <> {} & ( for f being Morphism of d,a
for g being Morphism of d,b ex h being Morphism of d,c st
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) ) ) ; :: thesis: c is_a_product_wrt p1,p2
thus ( dom p1 = c & dom p2 = c ) by A1, A2, CAT_1:23; :: according to CAT_3:def 16 :: 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
A15: f in Hom d,(cod p1) and
A16: 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 ) ) )
A17: Hom d,a <> {} by A1, A15, CAT_1:23;
A18: cod p1 = a by A1, CAT_1:23;
then A19: f is Morphism of d,a by A15, CAT_1:def 7;
A20: cod p2 = b by A2, CAT_1:23;
then g is Morphism of d,b by A16, CAT_1:def 7;
then consider h being Morphism of d,c such that
A21: for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) by A14, A16, A20, A19, A17;
reconsider h9 = h as Morphism of C ;
take h9 ; :: thesis: ( h9 in Hom d,c & ( for k being Morphism of C st k in Hom d,c holds
( ( p1 * k = f & p2 * k = g ) iff h9 = k ) ) )
A22: Hom d,c <> {} by A14, A15, A16, A18, A20;
hence h9 in Hom d,c by CAT_1:def 7; :: thesis: for k being Morphism of C st k in Hom d,c holds
( ( p1 * k = f & p2 * k = g ) iff h9 = k )
let k be Morphism of C; :: thesis: ( k in Hom d,c implies ( ( p1 * k = f & p2 * k = g ) iff h9 = k ) )
assume k in Hom d,c ; :: thesis: ( ( p1 * k = f & p2 * k = g ) iff h9 = k )
then reconsider k9 = k as Morphism of d,c by CAT_1:def 7;
( p1 * k = p1 * k9 & p2 * k = p2 * k9 ) by A1, A2, A22, CAT_1:def 13;
hence ( ( p1 * k = f & p2 * k = g ) iff h9 = k ) by A21; :: thesis: verum