let C be category; :: thesis: for o1, o2 being object of C
for A being Morphism of o1,o2 st A is retraction & A is mono & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
A is iso
let o1, o2 be object of C; :: thesis: for A being Morphism of o1,o2 st A is retraction & A is mono & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
A is iso
let A be Morphism of o1,o2; :: thesis: ( A is retraction & A is mono & <^o1,o2^> <> {} & <^o2,o1^> <> {} implies A is iso )
assume that
A1: ( A is retraction & A is mono ) and
A2: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; :: thesis: A is iso
A3: <^o1,o1^> <> {} by ALTCAT_1:23;
consider B being Morphism of o2,o1 such that
A4: B is_right_inverse_of A by A1, Def2;
(A * B) * A = (idm o2) * A by A4, Def1;
then A * (B * A) = (idm o2) * A by A2, ALTCAT_1:25;
then A * (B * A) = A by A2, ALTCAT_1:24;
then A5: A * (B * A) = A * (idm o1) by A2, ALTCAT_1:def 19;
then B * A = idm o1 by A1, A3, Def7;
then A6: B is_left_inverse_of A by Def1;
then A7: A is coretraction by Def3;
then A8: A * (A " ) = A * B by A1, A2, A4, A6, Def4
.= idm o2 by A4, Def1 ;
(A " ) * A = B * A by A1, A2, A4, A6, A7, Def4
.= idm o1 by A1, A3, A5, Def7 ;
hence A is iso by A8, Def5; :: thesis: verum