let C be composable with_identities CategoryStr ; :: thesis: ( C is preorder implies C is associative )
assume A1: C is preorder ; :: thesis: C is associative

per cases ( C is empty or not C is empty ) ;

suppose C is empty ; :: thesis: C is associative

hence C is associative ; :: thesis: verum

end;

suppose A2: not C is empty ; :: 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

proof

let f1, f2, f3 be morphism of C; :: thesis: ( f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 implies f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )
assume A3: ( f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 ) ; :: thesis: f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3
set f11 = f1 (*) (f2 (*) f3);
set f22 = (f1 (*) f2) (*) f3;
A4: dom (f1 (*) (f2 (*) f3)) = dom (f2 (*) f3) by A3, Th4
.= dom f3 by A3, Th4
.= dom ((f1 (*) f2) (*) f3) by A3, Th4 ;
cod (f1 (*) (f2 (*) f3)) = cod f1 by A3, Th4
.= cod (f1 (*) f2) by A3, Th4
.= cod ((f1 (*) f2) (*) f3) by A3, Th4 ;
then ( f1 (*) (f2 (*) f3) in Hom ((dom (f1 (*) (f2 (*) f3))),(cod (f1 (*) (f2 (*) f3)))) & (f1 (*) f2) (*) f3 in Hom ((dom (f1 (*) (f2 (*) f3))),(cod (f1 (*) (f2 (*) f3)))) ) by A4, A2, Th19;
hence f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 by A1; :: thesis: verum

end;

hence C is associative by CAT_6:def 10; :: thesis: verum

end;

end;