set H = multMagma(# the carrier of G, the multF of G #);
let x, y, z be Element of multMagma(# the carrier of G, the multF of G #); :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)
thus (x * y) * z = x * (y * z) by BINOP_1:def 3; :: thesis: verum