let C be Category; for a, b, c 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 a, b, c be Object of C; ( 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) <> {}
; 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; 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; ( 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 ) ) ) )
( ( 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 ) ) )
;
CAT_3:def 15 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;
( 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)
<> {}
;
( 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 ) ) )
set f = the
Morphism of
d,
a;
set g = the
Morphism of
d,
b;
A6:
cod p2 = b
by A2, CAT_1:5;
then A7:
the
Morphism of
d,
b in Hom (
d,
(cod p2))
by A5, CAT_1:def 5;
A8:
cod p1 = a
by A1, CAT_1:5;
then
the
Morphism of
d,
a in Hom (
d,
(cod p1))
by A4, CAT_1:def 5;
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 = the
Morphism of
d,
a &
p2 (*) k = the
Morphism of
d,
b ) iff
h = k ) ) )
by A3, A7;
hence
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 f be
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 g be
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 )
A10:
g in Hom (
d,
(cod p2))
by A5, A6, CAT_1:def 5;
f in Hom (
d,
(cod p1))
by A4, A8, CAT_1:def 5;
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 5;
take
h
;
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k )
let k be
Morphism of
d,
c;
( ( p1 * k = f & p2 * k = g ) iff h = k )
A13:
k in Hom (
d,
c)
by A9, CAT_1:def 5;
(
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;
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 ) ) )
; c is_a_product_wrt p1,p2
thus
( dom p1 = c & dom p2 = c )
by A1, A2, CAT_1:5; CAT_3:def 15 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; 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; ( 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))
; 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:5;
A18:
cod p1 = a
by A1, CAT_1:5;
then A19:
f is Morphism of d,a
by A15, CAT_1:def 5;
A20:
cod p2 = b
by A2, CAT_1:5;
then
g is Morphism of d,b
by A16, CAT_1:def 5;
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
; ( 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 5; 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; ( k in Hom (d,c) implies ( ( p1 (*) k = f & p2 (*) k = g ) iff h9 = k ) )
assume
k in Hom (d,c)
; ( ( p1 (*) k = f & p2 (*) k = g ) iff h9 = k )
then reconsider k9 = k as Morphism of d,c by CAT_1:def 5;
( 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; verum