theorem Th16: :: CAT_6:16

for C being CategoryStr
for f being morphism of C
for g being morphism of CategoryStr(# the carrier of C, the composition of C #) st f = g holds
( f is left_identity iff g is left_identity )