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