theorem Th3: :: CAT_7:3

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