let C be Category; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) <> {} ) ; :: thesis: ( 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;

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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) <> {} ) ; :: thesis: ( 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 :: thesis: ( 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))) <> {} ) )

A11:
{0} in {0,{0}}
by TARSKI:def 2;Hom ((cod (F /. x1)),(cod (F /. x2))) <> {} ) )

thus
F is Projections_family of c,{0,{0}}
; :: thesis: ( 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; :: thesis: 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 ; :: thesis: ( 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}} ; :: thesis: 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; :: thesis: verum

end;Hom ((cod (F /. x1)),(cod (F /. x2))) <> {} ) )

thus c is_a_product_wrt F by A2, Th54; :: thesis: 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 ; :: thesis: ( 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}} ; :: thesis: 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; :: thesis: verum

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; :: thesis: verum