let C be category; :: thesis: ( ( for o1, o2 being object of C
for f being Morphism of o1,o2 holds f is coretraction ) implies for a, b being object of C
for g being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
g is iso )
assume A1: for o1, o2 being object of C
for f being Morphism of o1,o2 holds f is coretraction ; :: thesis: for a, b being object of C
for g being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
g is iso
let a, b be object of C; :: thesis: for g being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
g is iso
let g be Morphism of a,b; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies g is iso )
assume A2: ( <^a,b^> <> {} & <^b,a^> <> {} ) ; :: thesis: g is iso
A3: g is coretraction by A1;
g is retraction

proof

consider f being Morphism of b,a such that
A4: f is_left_inverse_of g by A3, ALTCAT_3:def 3;
take f ; :: according to ALTCAT_3:def 2 :: thesis: g is_left_inverse_of f
A5: f is mono by A1, A2, ALTCAT_3:16;
f * (g * f) = (f * g) * f by A2, ALTCAT_1:25
.= (idm a) * f by A4, ALTCAT_3:def 1
.= f by A2, ALTCAT_1:24
.= f * (idm b) by A2, ALTCAT_1:def 19 ;
hence g * f = idm b by A5, ALTCAT_3:def 7; :: according to ALTCAT_3:def 1 :: thesis: verum

end;

hence g is iso by A2, A3, ALTCAT_3:6; :: thesis: verum