let C be Category; :: thesis: for g, f being Morphism of C st dom g = cod f & g * f is coretraction holds
f is coretraction
let g, f be Morphism of C; :: thesis: ( dom g = cod f & g * f is coretraction implies f is coretraction )
assume A1: dom g = cod f ; :: thesis: ( not g * f is coretraction or f is coretraction )
given i being Morphism of C such that A2: dom i = cod (g * f) and
A3: i * (g * f) = id (dom (g * f)) ; :: according to CAT_3:def 11 :: thesis: f is coretraction
take i * g ; :: according to CAT_3:def 11 :: thesis: ( dom (i * g) = cod f & (i * g) * f = id (dom f) )
A4: cod g = cod (g * f) by A1, CAT_1:42;
hence dom (i * g) = cod f by A1, A2, CAT_1:42; :: thesis: (i * g) * f = id (dom f)
thus (i * g) * f = id (dom (g * f)) by A1, A2, A3, A4, CAT_1:43
.= id (dom f) by A1, CAT_1:42 ; :: thesis: verum