theorem Th47: :: CAT_6:46

for C being non empty category
for f being morphism of C holds
( f is identity iff ex o being Object of (Alter C) st f = id o )