reconsider x = multMagma(# the carrier of M, the multF of M #) as Subgroup of G by A1;

now

let a be Element of G; :: thesis: a * x = x * a
thus a * x = a * M
.= M * a by GROUP_3:117
.= x * a ; :: thesis: verum

end;

then x is normal Subgroup of G by GROUP_3:117;
hence multMagma(# the carrier of M, the multF of M #) is strict normal Subgroup of B by A1, Th9; :: thesis: verum