let C, D be Category; :: thesis: for f being Morphism of C
for T being Functor of C,D st f is retraction holds
T . f is retraction
let f be Morphism of C; :: thesis: for T being Functor of C,D st f is retraction holds
T . f is retraction
let T be Functor of C,D; :: thesis: ( f is retraction implies T . 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 8 :: thesis: T . f is retraction
take T . i ; :: according to CAT_3:def 8 :: thesis: ( cod (T . i) = dom (T . f) & (T . f) * (T . i) = id (cod (T . f)) )
thus cod (T . i) = T . (dom f) by A1, CAT_1:72
.= dom (T . f) by CAT_1:72 ; :: thesis: (T . f) * (T . i) = id (cod (T . f))
thus (T . f) * (T . i) = T . (id (cod f)) by A1, A2, CAT_1:64
.= id (cod (T . f)) by CAT_1:63 ; :: thesis: verum