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