let C be Category; :: thesis: for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st f is coretraction & g is coretraction holds
g * f is coretraction
let a, b, c be Object of C; :: thesis: for f being Morphism of a,b
for g being Morphism of b,c st f is coretraction & g is coretraction holds
g * f is coretraction
let f be Morphism of a,b; :: thesis: for g being Morphism of b,c st f is coretraction & g is coretraction holds
g * f is coretraction
let g be Morphism of b,c; :: thesis: ( f is coretraction & g is coretraction implies g * f is coretraction )
assume A1: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ; :: according to CAT_3:def 9 :: thesis: ( for g being Morphism of b,a holds not g * f = id a or not g is coretraction or g * f is coretraction )
given i being Morphism of b,a such that A2: i * f = id a ; :: thesis: ( not g is coretraction or g * f is coretraction )
assume A3: ( Hom (b,c) <> {} & Hom (c,b) <> {} ) ; :: according to CAT_3:def 9 :: thesis: ( for g being Morphism of c,b holds not g * g = id b or g * f is coretraction )
given j being Morphism of c,b such that A4: j * g = id b ; :: thesis: g * f is coretraction
thus A5: ( Hom (a,c) <> {} & Hom (c,a) <> {} ) by A1, A3, CAT_1:24; :: according to CAT_3:def 9 :: thesis: ex g being Morphism of c,a st g * (g * f) = id a
take i * j ; :: thesis: (i * j) * (g * f) = id a
thus (i * j) * (g * f) = i * (j * (g * f)) by A1, A3, A5, CAT_1:25
.= i * ((j * g) * f) by A1, A3, CAT_1:25
.= id a by A1, A2, A4, CAT_1:28 ; :: thesis: verum