theorem Th7: :: CAT_7:7

for C being composable with_identities CategoryStr
for f1, f2 being morphism of C st f1 |> f2 & f1 is identity & f2 is identity holds
f1 = f2