let C be category; :: thesis:
let D be non empty subcategory of C; :: thesis:
let o1, o2 be Object of C; :: thesis:
let p1, p2 be Object of D; :: thesis:
let m be Morphism of o1,o2; :: thesis:
let n be Morphism of p1,p2; :: thesis:
assume that
A1: ( p1 = o1 & p2 = o2 ) and
A2: m = n and
A3: <^p1,p2^> <> {} and
A4: <^p2,p1^> <> {} ; :: thesis:
A5: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A1, A3, A4, ALTCAT_2:31, XBOOLE_1:3;
thus A6: ( n is retraction implies m is retraction ) :: thesis:

proof

assume n is retraction ; :: thesis:
then consider B being Morphism of p2,p1 such that
A7: B is_right_inverse_of n ;
reconsider B1 = B as Morphism of o2,o1 by A1, A4, ALTCAT_2:33;
take B1 ; :: according to ALTCAT_3:def 2 :: thesis:
thus m is_left_inverse_of B1 by A1, A2, A3, A4, A7, Th38; :: thesis:

end;

thus A8: ( n is coretraction implies m is coretraction ) :: thesis:

proof

assume n is coretraction ; :: thesis:
then consider B being Morphism of p2,p1 such that
A9: B is_left_inverse_of n ;
reconsider B1 = B as Morphism of o2,o1 by A1, A4, ALTCAT_2:33;
take B1 ; :: according to ALTCAT_3:def 3 :: thesis:
thus B1 is_left_inverse_of m by A1, A2, A3, A4, A9, Th38; :: thesis:

end;

assume n is iso ; :: thesis:
hence m is iso by A6, A8, A5, ALTCAT_3:5, ALTCAT_3:6; :: thesis: