let C be composable CategoryStr ; :: thesis: ( C is associative iff for f, g, h being morphism of C st h |> g & g |> f holds
h (*) (g (*) f) = (h (*) g) (*) f )
hereby :: thesis: ( ( for f, g, h being morphism of C st h |> g & g |> f holds
h (*) (g (*) f) = (h (*) g) (*) f ) implies C is associative )
assume A1: C is associative ; :: thesis: for f, g, h being morphism of C st h |> g & g |> f holds
h (*) (g (*) f) = (h (*) g) (*) f
A2: ( C is left_composable & C is right_composable ) by Def11;
let f, g, h be morphism of C; :: thesis: ( h |> g & g |> f implies h (*) (g (*) f) = (h (*) g) (*) f )
assume A3: ( h |> g & g |> f ) ; :: thesis: h (*) (g (*) f) = (h (*) g) (*) f
then ( h (*) g |> f & h |> g (*) f ) by A2;
hence h (*) (g (*) f) = (h (*) g) (*) f by A3, A1; :: thesis: verum
end;
assume for f, g, h being morphism of C st h |> g & g |> f holds
h (*) (g (*) f) = (h (*) g) (*) f ; :: thesis: C is associative
hence C is associative ; :: thesis: verum