for C being category
for o1, o2 being Object of C
for A being Morphism of o1,o2 st A is iso holds
( A is retraction & A is coretraction )