let C be composable CategoryStr ; :: thesis: for f1, f2, f3 being morphism of C st f1 |> f2 & f2 |> f3 & f2 is identity holds
f1 |> f3
let f1, f2, f3 be morphism of C; :: thesis: ( f1 |> f2 & f2 |> f3 & f2 is identity implies f1 |> f3 )
A1: C is right_composable by CAT_6:def 11;
assume A2: ( f1 |> f2 & f2 |> f3 ) ; :: thesis: ( not f2 is identity or f1 |> f3 )
assume f2 is identity ; :: thesis: f1 |> f3
then f2 (*) f3 = f3 by A2, CAT_6:def 14, CAT_6:def 4;
hence f1 |> f3 by A2, A1, CAT_6:def 9; :: thesis: verum