let C be associative composable CategoryStr ; :: thesis: for f1, f2, f3 being morphism of C st f1 |> f2 & f2 |> f3 holds
(f1 (*) f2) (*) f3 = f1 (*) (f2 (*) f3)
let f1, f2, f3 be morphism of C; :: thesis: ( f1 |> f2 & f2 |> f3 implies (f1 (*) f2) (*) f3 = f1 (*) (f2 (*) f3) )
assume A1: ( f1 |> f2 & f2 |> f3 ) ; :: thesis: (f1 (*) f2) (*) f3 = f1 (*) (f2 (*) f3)
( C is left_composable & C is right_composable ) by CAT_6:def 11;
then ( f1 (*) f2 |> f3 & f1 |> f2 (*) f3 ) by A1, CAT_6:def 8, CAT_6:def 9;
hence (f1 (*) f2) (*) f3 = f1 (*) (f2 (*) f3) by A1, CAT_6:def 10; :: thesis: verum