let C be Category; :: thesis:
let c, a, b be Object of C; :: thesis:
assume A1: ( Hom c,a <> {} & Hom c,b <> {} ) ; :: thesis:
let p1 be Morphism of c,a; :: thesis:
let p2 be Morphism of c,b; :: thesis:
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:

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

end;

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