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