let C be CategoryStr ; :: thesis: ( C is composable iff 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 ) ) ) )

hereby :: thesis: ( ( 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 ) ) ) ) implies C is composable )

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

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: C is composable
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: verum