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 9 :: 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 9 :: thesis: ( not dom g = cod f or g * f is coretraction )
A5: cod j = cod (j * g) by A3, CAT_1:17
.= dom g by A4, CAT_1:19 ;
assume A6: dom g = cod f ; :: thesis: g * f is coretraction
take i * j ; :: according to CAT_3:def 9 :: thesis: ( dom (i * j) = cod (g * f) & (i * j) * (g * f) = id (dom (g * f)) )
A7: cod g = cod (g * f) by A6, CAT_1:17;
hence dom (i * j) = cod (g * f) by A1, A3, A6, A5, CAT_1:17; :: thesis: (i * j) * (g * f) = id (dom (g * f))
thus (i * j) * (g * f) = i * (j * (g * f)) by A1, A3, A6, A5, A7, CAT_1:18
.= i * ((j * g) * f) by A3, A6, CAT_1:18
.= id (dom f) by A2, A4, A6, CAT_1:21
.= id (dom (g * f)) by A6, CAT_1:17 ; :: thesis: verum