let C be Category; for a, b, c being Object of C
for p1 being Morphism of c,a
for p2 being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & c is_a_product_wrt p1,p2 & Hom (a,b) <> {} & Hom (b,a) <> {} holds
( p1 is retraction & p2 is retraction )
let a, b, c be Object of C; for p1 being Morphism of c,a
for p2 being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & c is_a_product_wrt p1,p2 & Hom (a,b) <> {} & Hom (b,a) <> {} holds
( p1 is retraction & p2 is retraction )
let p1 be Morphism of c,a; for p2 being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & c is_a_product_wrt p1,p2 & Hom (a,b) <> {} & Hom (b,a) <> {} holds
( p1 is retraction & p2 is retraction )
let p2 be Morphism of c,b; ( Hom (c,a) <> {} & Hom (c,b) <> {} & c is_a_product_wrt p1,p2 & Hom (a,b) <> {} & Hom (b,a) <> {} implies ( p1 is retraction & p2 is retraction ) )
assume that
A1:
( Hom (c,a) <> {} & Hom (c,b) <> {} )
and
A2:
c is_a_product_wrt p1,p2
and
A3:
( Hom (a,b) <> {} & Hom (b,a) <> {} )
; ( p1 is retraction & p2 is retraction )
set I = {0,{0}};
( dom p1 = c & dom p2 = c )
by A2;
then reconsider F = (0,{0}) --> (p1,p2) as Projections_family of c,{0,{0}} by Th44;
A4:
F /. 0 = p1
by Th3;
A5:
F /. {0} = p2
by Th3;
A6:
now ( F is Projections_family of c,{0,{0}} & c is_a_product_wrt F & ( for x1, x2 being set st x1 in {0,{0}} & x2 in {0,{0}} holds
Hom ((cod (F /. x1)),(cod (F /. x2))) <> {} ) )thus
F is
Projections_family of
c,
{0,{0}}
;
( c is_a_product_wrt F & ( for x1, x2 being set st x1 in {0,{0}} & x2 in {0,{0}} holds
Hom ((cod (F /. x1)),(cod (F /. x2))) <> {} ) )thus
c is_a_product_wrt F
by A2, Th54;
for x1, x2 being set st x1 in {0,{0}} & x2 in {0,{0}} holds
Hom ((cod (F /. x1)),(cod (F /. x2))) <> {} let x1,
x2 be
set ;
( x1 in {0,{0}} & x2 in {0,{0}} implies Hom ((cod (F /. x1)),(cod (F /. x2))) <> {} )assume that A7:
x1 in {0,{0}}
and A8:
x2 in {0,{0}}
;
Hom ((cod (F /. x1)),(cod (F /. x2))) <> {} A9:
(
x2 = 0 or
x2 = {0} )
by A8, TARSKI:def 2;
(
x1 = 0 or
x1 = {0} )
by A7, TARSKI:def 2;
then A10:
(
cod (F /. x1) = a or
cod (F /. x1) = b )
by A4, A5, A1, CAT_1:5;
(
cod (F /. x2) = a or
cod (F /. x2) = b )
by A9, A4, A5, A1, CAT_1:5;
hence
Hom (
(cod (F /. x1)),
(cod (F /. x2)))
<> {}
by A3, A10;
verum end;
A11:
{0} in {0,{0}}
by TARSKI:def 2;
A12:
0 in {0,{0}}
by TARSKI:def 2;
( cod (F /. 0) = a & cod (F /. {0}) = b )
by A4, A5, A1, CAT_1:5;
hence
( p1 is retraction & p2 is retraction )
by A4, A6, A11, Th49, A5, A1, A12; verum