set H = multMagma(# the carrier of G, the multF of G #);
reconsider H = multMagma(# the carrier of G, the multF of G #) as non empty Group-like multMagma ;
dom the multF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def 1;
then the multF of H = the multF of G || the carrier of H by RELAT_1:68;
hence multMagma(# the carrier of G, the multF of G #) is strict Subgroup of G by Def5; :: thesis: verum