let I be set ; :: thesis: for C being Category
for c being Object of C
for F being Projections_family of c,I st c is_a_product_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds
Hom ((cod (F /. x1)),(cod (F /. x2))) <> {} ) holds
for x being set st x in I holds
for d being Object of C st d = cod (F /. x) & Hom (c,d) <> {} holds
for f being Morphism of c,d st f = F /. x holds
f is retraction
let C be Category; :: thesis: for c being Object of C
for F being Projections_family of c,I st c is_a_product_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds
Hom ((cod (F /. x1)),(cod (F /. x2))) <> {} ) holds
for x being set st x in I holds
for d being Object of C st d = cod (F /. x) & Hom (c,d) <> {} holds
for f being Morphism of c,d st f = F /. x holds
f is retraction
let c be Object of C; :: thesis: for F being Projections_family of c,I st c is_a_product_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds
Hom ((cod (F /. x1)),(cod (F /. x2))) <> {} ) holds
for x being set st x in I holds
for d being Object of C st d = cod (F /. x) & Hom (c,d) <> {} holds
for f being Morphism of c,d st f = F /. x holds
f is retraction
let F be Projections_family of c,I; :: thesis: ( c is_a_product_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds
Hom ((cod (F /. x1)),(cod (F /. x2))) <> {} ) implies for x being set st x in I holds
for d being Object of C st d = cod (F /. x) & Hom (c,d) <> {} holds
for f being Morphism of c,d st f = F /. x holds
f is retraction )
assume that
A1: c is_a_product_wrt F and
A2: for x1, x2 being set st x1 in I & x2 in I holds
Hom ((cod (F /. x1)),(cod (F /. x2))) <> {} ; :: thesis: for x being set st x in I holds
for d being Object of C st d = cod (F /. x) & Hom (c,d) <> {} holds
for f being Morphism of c,d st f = F /. x holds
f is retraction
let x be set ; :: thesis: ( x in I implies for d being Object of C st d = cod (F /. x) & Hom (c,d) <> {} holds
for f being Morphism of c,d st f = F /. x holds
f is retraction )
assume A3: x in I ; :: thesis: for d being Object of C st d = cod (F /. x) & Hom (c,d) <> {} holds
for f being Morphism of c,d st f = F /. x holds
f is retraction
let d be Object of C; :: thesis: ( d = cod (F /. x) & Hom (c,d) <> {} implies for f being Morphism of c,d st f = F /. x holds
f is retraction )
assume that
A4: d = cod (F /. x) and
A5: Hom (c,d) <> {} ; :: thesis: for f being Morphism of c,d st f = F /. x holds
f is retraction
let f be Morphism of c,d; :: thesis: ( f = F /. x implies f is retraction )
assume A6: f = F /. x ; :: thesis: f is retraction
defpred S₁[ set , set ] means ( ( $1 = x implies $2 = id d ) & ( $1 <> x implies $2 in Hom (d,(cod (F /. $1))) ) );
A7: for y being set st y in I holds
ex z being set st
( z in the carrier' of C & S₁[y,z] )

proof

let y be set ; :: thesis: ( y in I implies ex z being set st
( z in the carrier' of C & S₁[y,z] ) )
set z = the Element of Hom (d,(cod (F /. y)));
assume y in I ; :: thesis: ex z being set st
( z in the carrier' of C & S₁[y,z] )
then A8: Hom (d,(cod (F /. y))) <> {} by A2, A3, A4;
then A9: the Element of Hom (d,(cod (F /. y))) in Hom (d,(cod (F /. y))) ;

per cases ( y = x or y <> x ) ;

suppose A10: y = x ; :: thesis: ex z being set st
( z in the carrier' of C & S₁[y,z] )

take z = id d; :: thesis: ( z in the carrier' of C & S₁[y,z] )
thus z in the carrier' of C ; :: thesis: S₁[y,z]
thus S₁[y,z] by A10; :: thesis: verum

end;

suppose A11: y <> x ; :: thesis: ex z being set st
( z in the carrier' of C & S₁[y,z] )

take the Element of Hom (d,(cod (F /. y))) ; :: thesis: ( the Element of Hom (d,(cod (F /. y))) in the carrier' of C & S₁[y, the Element of Hom (d,(cod (F /. y)))] )
thus the Element of Hom (d,(cod (F /. y))) in the carrier' of C by A9; :: thesis: S₁[y, the Element of Hom (d,(cod (F /. y)))]
thus S₁[y, the Element of Hom (d,(cod (F /. y)))] by A8, A11; :: thesis: verum

end;

end;

end;

consider F9 being Function such that
A12: ( dom F9 = I & rng F9 c= the carrier' of C ) and
A13: for y being set st y in I holds
S₁[y,F9 . y] from FUNCT_1:sch 5(A7);
reconsider F9 = F9 as Function of I, the carrier' of C by A12, FUNCT_2:def 1, RELSET_1:4;

now :: thesis: for y being set st y in I holds
(doms F9) /. y = (I --> d) /. y

let y be set ; :: thesis: ( y in I implies (doms F9) /. y = (I --> d) /. y )
assume A14: y in I ; :: thesis: (doms F9) /. y = (I --> d) /. y
then A15: F9 . y = F9 /. y by FUNCT_2:def 13;
then A16: ( y <> x implies F9 /. y in Hom (d,(cod (F /. y))) ) by A13, A14;
( y = x implies F9 /. y = id d ) by A13, A14, A15;
then dom (F9 /. y) = d by A16, CAT_1:1, CAT_1:58;
hence (doms F9) /. y = d by A14, Def1
.= (I --> d) /. y by A14, Th2 ;
:: thesis: verum

end;

then A17: F9 is Projections_family of d,I by Def13, Th1;

now :: thesis: for y being set st y in I holds
(cods F9) /. y = (cods F) /. y

let y be set ; :: thesis: ( y in I implies (cods F9) /. y = (cods F) /. y )
assume A18: y in I ; :: thesis: (cods F9) /. y = (cods F) /. y
then A19: F9 . y = F9 /. y by FUNCT_2:def 13;
then A20: ( y <> x implies F9 /. y in Hom (d,(cod (F /. y))) ) by A13, A18;
( y = x implies F9 /. y = id d ) by A13, A18, A19;
then cod (F9 /. y) = cod (F /. y) by A20, A4, CAT_1:1, CAT_1:58;
hence (cods F9) /. y = cod (F /. y) by A18, Def2
.= (cods F) /. y by A18, Def2 ;
:: thesis: verum

end;

then consider i being Morphism of C such that
A21: i in Hom (d,c) and
A22: for k being Morphism of C st k in Hom (d,c) holds
( ( for y being set st y in I holds
(F /. y) (*) k = F9 /. y ) iff i = k ) by A1, A17, Def14, Th1;
reconsider i = i as Morphism of d,c by A21, CAT_1:def 5;
thus ( Hom (c,d) <> {} & Hom (d,c) <> {} ) by A21, A5; :: according to CAT_3:def 8 :: thesis: ex g being Morphism of d,c st f * g = id d
take i ; :: thesis: f * i = id d
thus f * i = f (*) i by A21, A5, CAT_1:def 13
.= F9 /. x by A3, A21, A22, A6
.= F9 . x by A3, FUNCT_2:def 13
.= id d by A3, A13 ; :: thesis: verum