let C be CategoryStr ; :: thesis:

hereby :: thesis:

assume C is composable ; :: thesis:
then A1: ( C is left_composable & C is right_composable ) ;
let f, g, h be morphism of C; :: thesis:
thus ( h (*) g |> f & h |> g implies g |> f ) by A1; :: thesis:
thus ( h |> g (*) f & g |> f implies h |> g ) by A1; :: thesis:
assume A2: g |> f ; :: thesis:
assume A3: h |> g ; :: thesis:
thus h (*) g |> f by A2, A3, A1; :: thesis:
thus h |> g (*) f by A2, A3, A1; :: thesis:

end;

assume A4: for f, g, h being morphism of C holds
( ( h (*) g |> f & h |> g implies g |> f ) & ( h |> g (*) f & g |> f implies h |> g ) & ( g |> f & h |> g implies ( h (*) g |> f & h |> g (*) f ) ) ) ; :: thesis:
then A5: C is left_composable ;
for f, f1, f2 being morphism of C st f1 |> f2 holds
( f |> f1 (*) f2 iff f |> f1 ) by A4;
hence C is composable by A5, Def9; :: thesis: