theorem Th25: :: CAT_6:25

for C1, C2 being with_identities CategoryStr st CategoryStr(# the carrier of C1, the composition of C1 #) = CategoryStr(# the carrier of C2, the composition of C2 #) holds
for f1 being morphism of C1
for f2 being morphism of C2 st f1 = f2 holds
( f1 is identity iff f2 is identity )