set H = multMagma(# the carrier of G,the multF of G #);
multMagma(# the carrier of G,the multF of G #) is Group-like

proof

consider e9 being Element of G such that
A1: for h being Element of G holds
( h * e9 = h & e9 * h = h & ex g being Element of G st
( h * g = e9 & g * h = e9 ) ) by GROUP_1:def 3;
reconsider e = e9 as Element of multMagma(# the carrier of G,the multF of G #) ;
take e ; :: according to GROUP_1:def 3 :: thesis: for b₁ being Element of the carrier of multMagma(# the carrier of G,the multF of G #) holds
( b₁ * e = b₁ & e * b₁ = b₁ & ex b₂ being Element of the carrier of multMagma(# the carrier of G,the multF of G #) st
( b₁ * b₂ = e & b₂ * b₁ = e ) )
let h be Element of multMagma(# the carrier of G,the multF of G #); :: thesis: ( h * e = h & e * h = h & ex b₁ being Element of the carrier of multMagma(# the carrier of G,the multF of G #) st
( h * b₁ = e & b₁ * h = e ) )
reconsider h9 = h as Element of G ;
consider g9 being Element of G such that
A2: ( h9 * g9 = e9 & g9 * h9 = e9 ) by A1;
( h9 * e9 = h9 & e9 * h9 = h9 ) by A1;
hence ( h * e = h & e * h = h ) ; :: thesis: ex b₁ being Element of the carrier of multMagma(# the carrier of G,the multF of G #) st
( h * b₁ = e & b₁ * h = e )
reconsider g = g9 as Element of multMagma(# the carrier of G,the multF of G #) ;
take g ; :: thesis: ( h * g = e & g * h = e )
thus ( h * g = e & g * h = e ) by A2; :: thesis: verum

end;

then 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:97;
hence multMagma(# the carrier of G,the multF of G #) is strict Subgroup of G by Def5; :: thesis: verum