let I be set ; :: thesis: for C being Category
for c being Object of C
for F being Injections_family of c,I st c is_a_coproduct_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds
Hom ((dom (F /. x1)),(dom (F /. x2))) <> {} ) holds
for x being set st x in I holds
F /. x is coretraction
let C be Category; :: thesis: for c being Object of C
for F being Injections_family of c,I st c is_a_coproduct_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds
Hom ((dom (F /. x1)),(dom (F /. x2))) <> {} ) holds
for x being set st x in I holds
F /. x is coretraction
let c be Object of C; :: thesis: for F being Injections_family of c,I st c is_a_coproduct_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds
Hom ((dom (F /. x1)),(dom (F /. x2))) <> {} ) holds
for x being set st x in I holds
F /. x is coretraction
let F be Injections_family of c,I; :: thesis: ( c is_a_coproduct_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds
Hom ((dom (F /. x1)),(dom (F /. x2))) <> {} ) implies for x being set st x in I holds
F /. x is coretraction )
assume that
A1: c is_a_coproduct_wrt F and
A2: for x1, x2 being set st x1 in I & x2 in I holds
Hom ((dom (F /. x1)),(dom (F /. x2))) <> {} ; :: thesis: for x being set st x in I holds
F /. x is coretraction
let x be set ; :: thesis: ( x in I implies F /. x is coretraction )
assume A3: x in I ; :: thesis: F /. x is coretraction
set d = dom (F /. x);
defpred S₁[ set , set ] means ( ( $1 = x implies $2 = id (dom (F /. x)) ) & ( $1 <> x implies $2 in Hom ((dom (F /. $1)),(dom (F /. x))) ) );
A4: 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 ((dom (F /. y)),(dom (F /. x)));
assume y in I ; :: thesis: ex z being set st
( z in the carrier' of C & S₁[y,z] )
then A5: Hom ((dom (F /. y)),(dom (F /. x))) <> {} by A2, A3;
then A6: the Element of Hom ((dom (F /. y)),(dom (F /. x))) is Morphism of dom (F /. y), dom (F /. x) by CAT_1:3;

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

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

take z = id (dom (F /. x)); :: 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 A7; :: thesis: verum

end;

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

take the Element of Hom ((dom (F /. y)),(dom (F /. x))) ; :: thesis: ( the Element of Hom ((dom (F /. y)),(dom (F /. x))) in the carrier' of C & S₁[y, the Element of Hom ((dom (F /. y)),(dom (F /. x)))] )
thus the Element of Hom ((dom (F /. y)),(dom (F /. x))) in the carrier' of C by A6; :: thesis: S₁[y, the Element of Hom ((dom (F /. y)),(dom (F /. x)))]
thus S₁[y, the Element of Hom ((dom (F /. y)),(dom (F /. x)))] by A5, A8; :: thesis: verum

end;

end;

end;

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

now

let y be set ; :: thesis: ( y in I implies (cods F9) /. y = (I --> (dom (F /. x))) /. y )
assume A11: y in I ; :: thesis: (cods F9) /. y = (I --> (dom (F /. x))) /. y
then A12: F9 . y = F9 /. y by FUNCT_2:def 13;
then A13: ( y <> x implies F9 /. y in Hom ((dom (F /. y)),(dom (F /. x))) ) by A10, A11;
( y = x implies F9 /. y = id (dom (F /. x)) ) by A10, A11, A12;
then cod (F9 /. y) = dom (F /. x) by A13, CAT_1:1, CAT_1:19;
hence (cods F9) /. y = dom (F /. x) by A11, Def4
.= (I --> (dom (F /. x))) /. y by A11, Th2 ;
:: thesis: verum

end;

then cods F9 = I --> (dom (F /. x)) by Th1;
then A14: F9 is Injections_family of dom (F /. x),I by Def17;

now

let y be set ; :: thesis: ( y in I implies (doms F9) /. y = (doms F) /. y )
assume A15: y in I ; :: thesis: (doms F9) /. y = (doms F) /. y
then A16: F9 . y = F9 /. y by FUNCT_2:def 13;
then A17: ( y <> x implies F9 /. y in Hom ((dom (F /. y)),(dom (F /. x))) ) by A10, A15;
( y = x implies F9 /. y = id (dom (F /. x)) ) by A10, A15, A16;
then dom (F9 /. y) = dom (F /. y) by A17, CAT_1:1, CAT_1:19;
hence (doms F9) /. y = dom (F /. y) by A15, Def3
.= (doms F) /. y by A15, Def3 ;
:: thesis: verum

end;

then doms F = doms F9 by Th1;
then consider i being Morphism of C such that
A18: i in Hom (c,(dom (F /. x))) and
A19: for k being Morphism of C st k in Hom (c,(dom (F /. x))) holds
( ( for y being set st y in I holds
k * (F /. y) = F9 /. y ) iff i = k ) by A1, A14, Def18;
take i ; :: according to CAT_3:def 9 :: thesis: ( dom i = cod (F /. x) & i * (F /. x) = id (dom (F /. x)) )
thus dom i = c by A18, CAT_1:1
.= cod (F /. x) by A3, Th67 ; :: thesis: i * (F /. x) = id (dom (F /. x))
thus i * (F /. x) = F9 /. x by A3, A18, A19
.= F9 . x by A3, FUNCT_2:def 13
.= id (dom (F /. x)) by A3, A10 ; :: thesis: verum