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