let C be CategoryStr ; :: thesis: ( C is empty implies ( C is left_composable & C is right_composable & C is with_left_identities & C is with_right_identities & C is associative ) )
assume A1: C is empty ; :: thesis: ( C is left_composable & C is right_composable & C is with_left_identities & C is with_right_identities & C is associative )
for f, f1, f2 being morphism of C st f1 |> f2 holds
( f1 (*) f2 |> f iff f2 |> f ) by A1;
hence C is left_composable ; :: thesis: ( C is right_composable & C is with_left_identities & C is with_right_identities & C is associative )
for f, f1, f2 being morphism of C st f1 |> f2 holds
( f |> f1 (*) f2 iff f |> f1 ) by A1;
hence C is right_composable ; :: thesis: ( C is with_left_identities & C is with_right_identities & C is associative )
thus C is with_left_identities by A1; :: thesis: ( C is with_right_identities & C is associative )
thus C is with_right_identities by A1; :: thesis: C is associative
for f1, f2, f3 being morphism of C st f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 holds
f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 by A1;
hence C is associative ; :: thesis: verum