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

for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds

for f being Morphism of d,c st f = F /. x holds

f 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

for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds

for f being Morphism of d,c st f = F /. x holds

f 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

for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds

for f being Morphism of d,c st f = F /. x holds

f 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

for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds

for f being Morphism of d,c st f = F /. x holds

f 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

for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds

for f being Morphism of d,c st f = F /. x holds

f is coretraction

let x be set ; :: thesis: ( x in I implies for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds

for f being Morphism of d,c st f = F /. x holds

f is coretraction )

assume A3: x in I ; :: thesis: for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds

for f being Morphism of d,c st f = F /. x holds

f is coretraction

let d be Object of C; :: thesis: ( d = dom (F /. x) & Hom (d,c) <> {} implies for f being Morphism of d,c st f = F /. x holds

f is coretraction )

assume that

A4: d = dom (F /. x) and

A5: Hom (d,c) <> {} ; :: thesis: for f being Morphism of d,c st f = F /. x holds

f is coretraction

let f be Morphism of d,c; :: thesis: ( f = F /. x implies f is coretraction )

assume A6: f = F /. x ; :: thesis: f is coretraction

defpred S_{1}[ object , object ] means ( ( $1 = x implies $2 = id d ) & ( $1 <> x implies $2 in Hom ((dom (F /. $1)),d) ) );

A7: for y being object st y in I holds

ex z being object st

( z in the carrier' of C & S_{1}[y,z] )

A12: ( dom F9 = I & rng F9 c= the carrier' of C ) and

A13: for y being object st y in I holds

S_{1}[y,F9 . y]
from FUNCT_1:sch 6(A7);

reconsider F9 = F9 as Function of I, the carrier' of C by A12, FUNCT_2:def 1, RELSET_1:4;

A21: i in Hom (c,d) and

A22: for k being Morphism of C st k in Hom (c,d) holds

( ( for y being set st y in I holds

k (*) (F /. y) = F9 /. y ) iff i = k ) by A1, A17, Th1;

thus ( Hom (d,c) <> {} & Hom (c,d) <> {} ) by A21, A5; :: according to CAT_3:def 9 :: thesis: ex g being Morphism of c,d st g * f = id d

reconsider i = i as Morphism of c,d by A21, CAT_1:def 5;

take i ; :: thesis: i * f = id d

thus i * f = i (*) (F /. x) by A6, A21, A5, CAT_1:def 13

.= F9 /. x by A3, A21, A22

.= F9 . x by A3, FUNCT_2:def 13

.= id d by A3, A13 ; :: thesis: verum

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

for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds

for f being Morphism of d,c st f = F /. x holds

f 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

for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds

for f being Morphism of d,c st f = F /. x holds

f 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

for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds

for f being Morphism of d,c st f = F /. x holds

f 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

for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds

for f being Morphism of d,c st f = F /. x holds

f 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

for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds

for f being Morphism of d,c st f = F /. x holds

f is coretraction

let x be set ; :: thesis: ( x in I implies for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds

for f being Morphism of d,c st f = F /. x holds

f is coretraction )

assume A3: x in I ; :: thesis: for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds

for f being Morphism of d,c st f = F /. x holds

f is coretraction

let d be Object of C; :: thesis: ( d = dom (F /. x) & Hom (d,c) <> {} implies for f being Morphism of d,c st f = F /. x holds

f is coretraction )

assume that

A4: d = dom (F /. x) and

A5: Hom (d,c) <> {} ; :: thesis: for f being Morphism of d,c st f = F /. x holds

f is coretraction

let f be Morphism of d,c; :: thesis: ( f = F /. x implies f is coretraction )

assume A6: f = F /. x ; :: thesis: f is coretraction

defpred S

A7: for y being object st y in I holds

ex z being object st

( z in the carrier' of C & S

proof

consider F9 being Function such that
let y be object ; :: thesis: ( y in I implies ex z being object st

( z in the carrier' of C & S_{1}[y,z] ) )

set z = the Element of Hom ((dom (F /. y)),d);

assume y in I ; :: thesis: ex z being object st

( z in the carrier' of C & S_{1}[y,z] )

then A8: Hom ((dom (F /. y)),d) <> {} by A2, A3, A4;

then A9: the Element of Hom ((dom (F /. y)),d) in Hom ((dom (F /. y)),d) ;

end;( z in the carrier' of C & S

set z = the Element of Hom ((dom (F /. y)),d);

assume y in I ; :: thesis: ex z being object st

( z in the carrier' of C & S

then A8: Hom ((dom (F /. y)),d) <> {} by A2, A3, A4;

then A9: the Element of Hom ((dom (F /. y)),d) in Hom ((dom (F /. y)),d) ;

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

end;

suppose A10:
y = x
; :: thesis: ex z being object st

( z in the carrier' of C & S_{1}[y,z] )

( z in the carrier' of C & S

take z = id d; :: thesis: ( z in the carrier' of C & S_{1}[y,z] )

thus z in the carrier' of C ; :: thesis: S_{1}[y,z]

thus S_{1}[y,z]
by A10; :: thesis: verum

end;thus z in the carrier' of C ; :: thesis: S

thus S

suppose A11:
y <> x
; :: thesis: ex z being object st

( z in the carrier' of C & S_{1}[y,z] )

( z in the carrier' of C & S

take
the Element of Hom ((dom (F /. y)),d)
; :: thesis: ( the Element of Hom ((dom (F /. y)),d) in the carrier' of C & S_{1}[y, the Element of Hom ((dom (F /. y)),d)] )

thus the Element of Hom ((dom (F /. y)),d) in the carrier' of C by A9; :: thesis: S_{1}[y, the Element of Hom ((dom (F /. y)),d)]

thus S_{1}[y, the Element of Hom ((dom (F /. y)),d)]
by A8, A11; :: thesis: verum

end;thus the Element of Hom ((dom (F /. y)),d) in the carrier' of C by A9; :: thesis: S

thus S

A12: ( dom F9 = I & rng F9 c= the carrier' of C ) and

A13: for y being object st y in I holds

S

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

(cods F9) /. y = (I --> d) /. y

then A17:
F9 is Injections_family of d,I
by Def16, Th1;(cods F9) /. y = (I --> d) /. y

let y be set ; :: thesis: ( y in I implies (cods F9) /. y = (I --> d) /. y )

assume A14: y in I ; :: thesis: (cods 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 ((dom (F /. y)),d) ) by A13, A14;

( y = x implies F9 /. y = id d ) by A13, A14, A15;

then cod (F9 /. y) = d by A16, CAT_1:1;

hence (cods F9) /. y = d by A14, Def2

.= (I --> d) /. y by A14, Th2 ;

:: thesis: verum

end;assume A14: y in I ; :: thesis: (cods 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 ((dom (F /. y)),d) ) by A13, A14;

( y = x implies F9 /. y = id d ) by A13, A14, A15;

then cod (F9 /. y) = d by A16, CAT_1:1;

hence (cods F9) /. y = d by A14, Def2

.= (I --> d) /. y by A14, Th2 ;

:: thesis: verum

now :: thesis: for y being set st y in I holds

(doms F9) /. y = (doms F) /. y

then consider i being Morphism of C such that (doms F9) /. y = (doms F) /. y

let y be set ; :: thesis: ( y in I implies (doms F9) /. y = (doms F) /. y )

assume A18: y in I ; :: thesis: (doms F9) /. y = (doms F) /. y

then A19: F9 . y = F9 /. y by FUNCT_2:def 13;

then A20: ( y <> x implies F9 /. y in Hom ((dom (F /. y)),d) ) by A13, A18;

( y = x implies F9 /. y = id d ) by A13, A18, A19;

then dom (F9 /. y) = dom (F /. y) by A20, A4, CAT_1:1;

hence (doms F9) /. y = dom (F /. y) by A18, Def1

.= (doms F) /. y by A18, Def1 ;

:: thesis: verum

end;assume A18: y in I ; :: thesis: (doms F9) /. y = (doms F) /. y

then A19: F9 . y = F9 /. y by FUNCT_2:def 13;

then A20: ( y <> x implies F9 /. y in Hom ((dom (F /. y)),d) ) by A13, A18;

( y = x implies F9 /. y = id d ) by A13, A18, A19;

then dom (F9 /. y) = dom (F /. y) by A20, A4, CAT_1:1;

hence (doms F9) /. y = dom (F /. y) by A18, Def1

.= (doms F) /. y by A18, Def1 ;

:: thesis: verum

A21: i in Hom (c,d) and

A22: for k being Morphism of C st k in Hom (c,d) holds

( ( for y being set st y in I holds

k (*) (F /. y) = F9 /. y ) iff i = k ) by A1, A17, Th1;

thus ( Hom (d,c) <> {} & Hom (c,d) <> {} ) by A21, A5; :: according to CAT_3:def 9 :: thesis: ex g being Morphism of c,d st g * f = id d

reconsider i = i as Morphism of c,d by A21, CAT_1:def 5;

take i ; :: thesis: i * f = id d

thus i * f = i (*) (F /. x) by A6, A21, A5, CAT_1:def 13

.= F9 /. x by A3, A21, A22

.= F9 . x by A3, FUNCT_2:def 13

.= id d by A3, A13 ; :: thesis: verum