let C be CategoryStr ; :: thesis: ( C is discrete implies ( C is composable & C is associative ) )
assume A1: C is discrete ; :: thesis: ( C is composable & C is associative )
A2: 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 ) ) )
proof
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, Th21; :: 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 ) :: thesis: ( g |> f & h |> g implies ( h (*) g |> f & h |> g (*) f ) )
proof
assume A3: ( h |> g (*) f & g |> f ) ; :: thesis: h |> g
then ( g (*) f = f & f = g ) by A1, Th21;
hence h |> g by A3; :: thesis: verum
end;
assume A4: g |> f ; :: thesis: ( not h |> g or ( h (*) g |> f & h |> g (*) f ) )
assume A5: h |> g ; :: thesis: ( h (*) g |> f & h |> g (*) f )
thus h (*) g |> f by A4, A5, A1, Th21; :: thesis: h |> g (*) f
( g |> g (*) f & h = g ) by A4, A5, A1, Th21;
hence h |> g (*) f ; :: thesis: verum
end;
A6: for f, g, h being morphism of C st h |> g & g |> f holds
h (*) (g (*) f) = (h (*) g) (*) f
proof
let f, g, h be morphism of C; :: thesis: ( h |> g & g |> f implies h (*) (g (*) f) = (h (*) g) (*) f )
assume A7: h |> g ; :: thesis: ( not g |> f or h (*) (g (*) f) = (h (*) g) (*) f )
assume g |> f ; :: thesis: h (*) (g (*) f) = (h (*) g) (*) f
then A8: ( f = g & g (*) f = f ) by A1, Th21;
thus h (*) (g (*) f) = g by A1, Th21, A7, A8
.= (h (*) g) (*) f by A1, Th21, A7, A8 ; :: thesis: verum
end;
A9: C is left_composable by A2;
for f, f1, f2 being morphism of C st f1 |> f2 holds
( f |> f1 (*) f2 iff f |> f1 ) by A2;
hence ( C is composable & C is associative ) by A6, A9, Def9; :: thesis: verum