let C be Category; :: thesis: for f being Morphism of C st f is coretraction & f is epi holds
f is invertible
let f be Morphism of C; :: thesis: ( f is coretraction & f is epi implies f is invertible )
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 f is epi or f is invertible )
assume A3: f is epi ; :: thesis: f is invertible
take i ; :: according to CAT_1:def 9 :: thesis: ( dom i = cod f & cod i = dom f & f * i = id (cod f) & i * f = id (dom f) )
thus dom i = cod f by A1; :: thesis: ( cod i = dom f & f * i = id (cod f) & i * f = id (dom f) )
thus A4: cod i = cod (i * f) by A1, CAT_1:17
.= dom f by A2, CAT_1:19 ; :: thesis: ( f * i = id (cod f) & i * f = id (dom f) )
then A5: dom (f * i) = cod f by A1, CAT_1:17;
A6: dom (id (cod f)) = cod f by CAT_1:19;
A7: cod (f * i) = cod f by A4, CAT_1:17
.= cod (id (cod f)) by CAT_1:19 ;
(f * i) * f = f * (id (dom f)) by A1, A2, A4, CAT_1:18
.= f by CAT_1:22
.= (id (cod f)) * f by CAT_1:21 ;
hence f * i = id (cod f) by A3, A7, A5, A6, CAT_1:def 8; :: thesis: i * f = id (dom f)
thus i * f = id (dom f) by A2; :: thesis: verum