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 that
A2: <^a,b^> <> {} and
A3: <^b,a^> <> {} ; :: thesis: g is iso
A4: g is coretraction by A1;
g is retraction

proof

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

end;

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