let C be category; for c1, c2, d being Object of C
for p1 being Morphism of d,c1
for p2 being Morphism of d,c2 st Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 holds
d,p2,p1 is_product_of c2,c1
let c1, c2, d be Object of C; for p1 being Morphism of d,c1
for p2 being Morphism of d,c2 st Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 holds
d,p2,p1 is_product_of c2,c1
let p1 be Morphism of d,c1; for p2 being Morphism of d,c2 st Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 holds
d,p2,p1 is_product_of c2,c1
let p2 be Morphism of d,c2; ( Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 implies d,p2,p1 is_product_of c2,c1 )
assume A1:
( Hom (d,c1) <> {} & Hom (d,c2) <> {} )
; ( not d,p1,p2 is_product_of c1,c2 or d,p2,p1 is_product_of c2,c1 )
assume A2:
d,p1,p2 is_product_of c1,c2
; d,p2,p1 is_product_of c2,c1
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 ) ) )
proof
let d1 be
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 g2 be
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 g1 be
Morphism of
d1,
c1;
( Hom (d1,c2) <> {} & Hom (d1,c1) <> {} implies ( 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 ) ) ) )
assume A3:
(
Hom (
d1,
c2)
<> {} &
Hom (
d1,
c1)
<> {} )
;
( 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 ) ) )
hence
Hom (
d1,
d)
<> {}
by A2, A1, Def10;
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 ) )
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
;
( p2 * h = g2 & p1 * h = g1 & ( for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1 holds
h = h1 ) )
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;
verum
end;
hence
d,p2,p1 is_product_of c2,c1
by A1, Def10; verum