let C be category; :: thesis:
let D be non empty full 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 A1: ( p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} ) ; :: thesis:
thus A2: ( m is retraction implies n is retraction ) :: thesis:

proof

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

end;

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

proof

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

end;

assume m is iso ; :: thesis:
hence n is iso by A1, A2, A4, ALTCAT_3:5, ALTCAT_3:6; :: thesis: