for A, B being category st A,B are_opposite holds
for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f & f is retraction & f is coretraction holds
f9 " = f "