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 that
A1: ( p1 = o1 & p2 = o2 ) and
A2: m = n and
A3: ( <^p1,p2^> <> {} & <^p2,p1^> <> {} ) ; :: thesis:
thus A4: ( m is retraction implies n is retraction ) :: thesis:

proof

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

end;

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

proof

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

end;

assume m is iso ; :: thesis:
hence n is iso by A3, A4, A6, ALTCAT_3:5, ALTCAT_3:6; :: thesis: