theorem Th42: :: CAT_6:41

for A being Category
for f being morphism of (alter A) holds
( f is identity iff ex o being Object of A st f = id o )