for C being category
for o1, o2 being Object of C
for f being Morphism of o1,o2
for g, h being Morphism of o2,o1 st h * f = idm o1 & f * g = idm o2 & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
g = h