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 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 b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( b1 * b2 = e & b2 * b1 = e ) )
let h be Element of multMagma(# the carrier of G, the multF of G #); :: thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( h * b1 = e & b1 * 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 b1 being Element of the carrier of multMagma(# the carrier of G, the multF of G #) st
( h * b1 = e & b1 * 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:68;
hence multMagma(# the carrier of G, the multF of G #) is strict Subgroup of G by Def5; :: thesis: verum