theorem Th2: :: ALTCAT_3:2

for C being category
for o1, o2 being Object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
( (A ") * A = idm o1 & A * (A ") = idm o2 )