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