theorem :: ALTCAT_4:39

for C being category
for D being non empty full subcategory of C
for o1, o2 being Object of C
for p1, p2 being Object of D
for m being Morphism of o1,o2
for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds
( ( m is retraction implies n is retraction ) & ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) )