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 Hom (b,c) <> {} & Hom (c,b) <> {} & g * f is coretraction holds

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 Hom (b,c) <> {} & Hom (c,b) <> {} & g * f is coretraction holds

f is coretraction

let f be Morphism of a,b; :: thesis: for g being Morphism of b,c st Hom (b,c) <> {} & Hom (c,b) <> {} & g * f is coretraction holds

f is coretraction

let g be Morphism of b,c; :: thesis: ( Hom (b,c) <> {} & Hom (c,b) <> {} & g * f is coretraction implies f is coretraction )

assume A1: ( Hom (b,c) <> {} & Hom (c,b) <> {} ) ; :: thesis: ( not g * f is coretraction or f is coretraction )

assume A2: ( Hom (a,c) <> {} & Hom (c,a) <> {} ) ; :: according to CAT_3:def 9 :: thesis: ( for g being Morphism of c,a holds not g * (g * f) = id a or f is coretraction )

given i being Morphism of c,a such that A3: i * (g * f) = id a ; :: thesis: f is coretraction

thus A4: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A1, A2, CAT_1:24; :: according to CAT_3:def 9 :: thesis: ex g being Morphism of b,a st g * f = id a

take i * g ; :: thesis: (i * g) * f = id a

thus (i * g) * f = id a by A4, A1, A2, A3, CAT_1:25; :: thesis: verum

for f being Morphism of a,b

for g being Morphism of b,c st Hom (b,c) <> {} & Hom (c,b) <> {} & g * f is coretraction holds

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 Hom (b,c) <> {} & Hom (c,b) <> {} & g * f is coretraction holds

f is coretraction

let f be Morphism of a,b; :: thesis: for g being Morphism of b,c st Hom (b,c) <> {} & Hom (c,b) <> {} & g * f is coretraction holds

f is coretraction

let g be Morphism of b,c; :: thesis: ( Hom (b,c) <> {} & Hom (c,b) <> {} & g * f is coretraction implies f is coretraction )

assume A1: ( Hom (b,c) <> {} & Hom (c,b) <> {} ) ; :: thesis: ( not g * f is coretraction or f is coretraction )

assume A2: ( Hom (a,c) <> {} & Hom (c,a) <> {} ) ; :: according to CAT_3:def 9 :: thesis: ( for g being Morphism of c,a holds not g * (g * f) = id a or f is coretraction )

given i being Morphism of c,a such that A3: i * (g * f) = id a ; :: thesis: f is coretraction

thus A4: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A1, A2, CAT_1:24; :: according to CAT_3:def 9 :: thesis: ex g being Morphism of b,a st g * f = id a

take i * g ; :: thesis: (i * g) * f = id a

thus (i * g) * f = id a by A4, A1, A2, A3, CAT_1:25; :: thesis: verum