let C be category; :: thesis: for o1, o2 being Object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 holds
( A is iso iff ( A is retraction & A is coretraction ) )
let o1, o2 be Object of C; :: thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 holds
( A is iso iff ( A is retraction & A is coretraction ) ) )
assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; :: thesis: for A being Morphism of o1,o2 holds
( A is iso iff ( A is retraction & A is coretraction ) )
let A be Morphism of o1,o2; :: thesis: ( A is iso iff ( A is retraction & A is coretraction ) )
thus ( A is iso implies ( A is retraction & A is coretraction ) ) by Th5; :: thesis: ( A is retraction & A is coretraction implies A is iso )
assume A2: ( A is retraction & A is coretraction ) ; :: thesis: A is iso
then A " is_right_inverse_of A by A1, Def4;
then A3: A * (A ") = idm o2 ;
A " is_left_inverse_of A by A1, A2, Def4;
then (A ") * A = idm o1 ;
hence A is iso by A3; :: thesis: verum