let C be CategoryStr ; :: thesis: ( C is associative iff CategoryStr(# the carrier of C, the composition of C #) is associative )

hereby :: thesis: ( CategoryStr(# the carrier of C, the composition of C #) is associative implies C is associative )

assume A1: C is associative ; :: thesis: CategoryStr(# the carrier of C, the composition of C #) is associative
for g1, g2, g3 being morphism of CategoryStr(# the carrier of C, the composition of C #) st g1 |> g2 & g2 |> g3 & g1 (*) g2 |> g3 & g1 |> g2 (*) g3 holds
g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3

proof

let g1, g2, g3 be morphism of CategoryStr(# the carrier of C, the composition of C #); :: thesis: ( g1 |> g2 & g2 |> g3 & g1 (*) g2 |> g3 & g1 |> g2 (*) g3 implies g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 )
reconsider f1 = g1, f2 = g2, f3 = g3 as morphism of C ;
assume ( g1 |> g2 & g2 |> g3 ) ; :: thesis: ( not g1 (*) g2 |> g3 or not g1 |> g2 (*) g3 or g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 )
then A2: ( f1 |> f2 & f2 |> f3 ) ;
A3: ( f1 (*) f2 = g1 (*) g2 & f2 (*) f3 = g2 (*) g3 ) by A2, Th11;
assume ( g1 (*) g2 |> g3 & g1 |> g2 (*) g3 ) ; :: thesis: g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3
then A4: ( f1 (*) f2 |> f3 & f1 |> f2 (*) f3 ) by A2, Th11;
then f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 by A2, A1;
hence g1 (*) (g2 (*) g3) = (f1 (*) f2) (*) f3 by A4, A3, Th11
.= (g1 (*) g2) (*) g3 by A4, A3, Th11 ;
:: thesis: verum

end;

hence CategoryStr(# the carrier of C, the composition of C #) is associative ; :: thesis: verum

end;

assume A5: CategoryStr(# the carrier of C, the composition of C #) is associative ; :: 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 )
reconsider g1 = f1, g2 = f2, g3 = f3 as morphism of CategoryStr(# the carrier of C, the composition of C #) ;
assume A6: ( f1 |> f2 & f2 |> f3 ) ; :: thesis: ( not f1 (*) f2 |> f3 or not f1 |> f2 (*) f3 or f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 )
then A7: ( g1 |> g2 & g2 |> g3 ) ;
A8: ( f1 (*) f2 = g1 (*) g2 & f2 (*) f3 = g2 (*) g3 ) by A6, Th11;
assume A9: ( f1 (*) f2 |> f3 & f1 |> f2 (*) f3 ) ; :: thesis: f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3
then ( g1 (*) g2 |> g3 & g1 |> g2 (*) g3 ) by A6, Th11;
then g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 by A7, A5;
hence f1 (*) (f2 (*) f3) = (g1 (*) g2) (*) g3 by A9, A8, Th11
.= (f1 (*) f2) (*) f3 by A9, A8, Th11 ;
:: thesis: verum

end;

hence C is associative ; :: thesis: verum