set H = multMagma(# the carrier of G, the multF of G #);

multMagma(# the carrier of G, the multF of G #) is Group-like

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

multMagma(# the carrier of G, the multF of G #) is Group-like

proof

then reconsider H = multMagma(# the carrier of G, the multF of G #) as non empty Group-like multMagma ;
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 2;

reconsider e = e9 as Element of multMagma(# the carrier of G, the multF of G #) ;

take e ; :: according to GROUP_1:def 2 :: thesis: for b_{1} being Element of the carrier of multMagma(# the carrier of G, the multF of G #) holds

( b_{1} * e = b_{1} & e * b_{1} = b_{1} & ex b_{2} being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st

( b_{1} * b_{2} = e & b_{2} * b_{1} = e ) )

let h be Element of multMagma(# the carrier of G, the multF of G #); :: thesis: ( h * e = h & e * h = h & ex b_{1} being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st

( h * b_{1} = e & b_{1} * 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_{1} being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st

( h * b_{1} = e & b_{1} * 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;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 2;

reconsider e = e9 as Element of multMagma(# the carrier of G, the multF of G #) ;

take e ; :: according to GROUP_1:def 2 :: thesis: for b

( b

( b

let h be Element of multMagma(# the carrier of G, the multF of G #); :: thesis: ( h * e = h & e * h = h & ex b

( h * b

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

( h * b

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

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