let C be category; :: thesis: for o1, o2 being object of C
for A being Morphism of o1,o2 st A is iso holds
( A is retraction & A is coretraction )
let o1, o2 be object of C; :: thesis: for A being Morphism of o1,o2 st A is iso holds
( A is retraction & A is coretraction )
let A be Morphism of o1,o2; :: thesis: ( A is iso implies ( A is retraction & A is coretraction ) )
assume A1: A is iso ; :: thesis: ( A is retraction & A is coretraction )
then A * (A ") = idm o2 by Def5;
then A " is_right_inverse_of A by Def1;
hence A is retraction by Def2; :: thesis: A is coretraction
(A ") * A = idm o1 by A1, Def5;
then A " is_left_inverse_of A by Def1;
hence A is coretraction by Def3; :: thesis: verum