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 10 :: 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 12 :: 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:42
.= cod f by A2, CAT_1:44 ; :: thesis: ( cod i = dom f & f * i = id (cod f) & i * f = id (dom f) )
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)

now

thus dom (i * f) = dom f by A4, CAT_1:42
.= dom (id (dom f)) by CAT_1:44 ; :: thesis: ( cod (i * f) = dom f & cod (id (dom f)) = dom f & f * (i * f) = f * (id (dom f)) )
thus cod (i * f) = dom f by A1, A4, CAT_1:42; :: thesis: ( cod (id (dom f)) = dom f & f * (i * f) = f * (id (dom f)) )
thus cod (id (dom f)) = dom f by CAT_1:44; :: thesis: f * (i * f) = f * (id (dom f))
thus f * (i * f) = (id (cod f)) * f by A1, A2, A4, CAT_1:43
.= f by CAT_1:46
.= f * (id (dom f)) by CAT_1:47 ; :: thesis: verum

end;

hence i * f = id (dom f) by A3, CAT_1:def 10; :: thesis: verum