let C be category; :: thesis: ( ( for o1, o2 being Object of C
for A1 being Morphism of o1,o2 holds A1 is retraction ) implies for a, b being Object of C
for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
A is iso )
assume A1: for o1, o2 being Object of C
for A1 being Morphism of o1,o2 holds A1 is retraction ; :: thesis: for a, b being Object of C
for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
A is iso
thus for a, b being Object of C
for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
A is iso :: thesis: verum

proof

let a, b be Object of C; :: thesis: for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
A is iso
let A be Morphism of a,b; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies A is iso )
assume that
A2: <^a,b^> <> {} and
A3: <^b,a^> <> {} ; :: thesis: A is iso
A4: A is retraction by A1;
A is coretraction

proof

consider A1 being Morphism of b,a such that
A5: A1 is_right_inverse_of A by A4;
A1 * (A * A1) = A1 * (idm b) by A5;
then A1 * (A * A1) = A1 by A3, ALTCAT_1:def 17;
then (A1 * A) * A1 = A1 by A2, A3, ALTCAT_1:21;
then A6: (A1 * A) * A1 = (idm a) * A1 by A3, ALTCAT_1:20;
( A1 is epi & <^a,a^> <> {} ) by A1, A2, A3, Th15, ALTCAT_1:19;
then A1 * A = idm a by A6;
then A1 is_left_inverse_of A ;
hence A is coretraction ; :: thesis: verum

end;

hence A is iso by A2, A3, A4, Th6; :: thesis: verum

end;