theorem Th41: :: YELLOW18:41

for C being semi-functional para-functional category
for a, b being Object of C st <^a,b^> <> {} holds
for f being Morphism of a,b st f is one-to-one & f " in <^b,a^> holds
f is iso