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 e' being Element of G such that
A1: for h being Element of G holds
( h * e' = h & e' * h = h & ex g being Element of G st
( h * g = e' & g * h = e' ) ) by GROUP_1:def 3;
reconsider e = e' 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 h' = h as Element of G ;
( h' * e' = h' & e' * h' = h' ) 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 )
consider g' being Element of G such that
A2: ( h' * g' = e' & g' * h' = e' ) by A1;
reconsider g = g' 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 ;
H is Subgroup of G

proof

thus the carrier of H c= the carrier of G ; :: according to GROUP_2:def 5 :: thesis: the multF of H = the multF of G || the carrier of H
dom the multF of G = [:the carrier of G,the carrier of G:] by FUNCT_2:def 1;
hence the multF of H = the multF of G || the carrier of H by RELAT_1:97; :: thesis: verum

end;

hence multMagma(# the carrier of G,the multF of G #) is strict Subgroup of G ; :: thesis: verum