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