let C be category; :: thesis:
let c1, c2, d be Object of C; :: thesis:
let p1 be Morphism of d,c1; :: thesis:
let p2 be Morphism of d,c2; :: thesis:
assume A1: ( Hom (d,c1) <> {} & Hom (d,c2) <> {} ) ; :: thesis:
assume A2: d,p1,p2 is_product_of c1,c2 ; :: thesis:
for d1 being Object of C
for g2 being Morphism of d1,c2
for g1 being Morphism of d1,c1 st Hom (d1,c2) <> {} & Hom (d1,c1) <> {} holds
( Hom (d1,d) <> {} & ex h being Morphism of d1,d st
( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds
h = h1 ) ) )

let d1 be Object of C; :: thesis:
let g2 be Morphism of d1,c2; :: thesis:
let g1 be Morphism of d1,c1; :: thesis:
assume A3: ( Hom (d1,c2) <> {} & Hom (d1,c1) <> {} ) ; :: thesis:
hence Hom (d1,d) <> {} by A2, A1, Def10; :: thesis:
consider h being Morphism of d1,d such that
A4: ( p1 * h = g1 & p2 * h = g2 & ( for h1 being Morphism of d1,d st p1 * h1 = g1 & p2 * h1 = g2 holds
h = h1 ) ) by A3, A2, A1, Def10;
take h ; :: thesis:
thus ( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds
h = h1 ) ) by A4; :: thesis:

end;