set H = multMagma(# the carrier of G, the multF of G #);
for x, y, z being Element of multMagma(# the carrier of G, the multF of G #) holds (x * y) * z = x * (y * z)

proof

let x, y, z be Element of multMagma(# the carrier of G, the multF of G #); :: thesis: (x * y) * z = x * (y * z)
reconsider xx = x, yy = y, zz = z as Element of G ;
(x * y) * z = (xx * yy) * zz
.= xx * (yy * zz) by Def3
.= x * (y * z) ;
hence (x * y) * z = x * (y * z) ; :: thesis: verum

end;

hence multMagma(# the carrier of G, the multF of G #) is associative ; :: thesis: verum