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 4 :: thesis: (x * y) * z = x * (y * z)
the multF of G is associative ;
hence (x * y) * z = x * (y * z) by BINOP_1:def 3; :: thesis: verum