set H = addMagma(# the carrier of G, the addF of G #);
addMagma(# the carrier of G, the addF of G #) is addGroup-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 Def2;
reconsider e = e9 as Element of addMagma(# the carrier of G, the addF of G #) ;
take e ; :: according to GROUP_1A:def 2 :: thesis: for h being Element of addMagma(# the carrier of G, the addF of G #) holds
( h + e = h & e + h = h & ex g being Element of addMagma(# the carrier of G, the addF of G #) st
( h + g = e & g + h = e ) )
let h be Element of addMagma(# the carrier of G, the addF of G #); :: thesis: ( h + e = h & e + h = h & ex g being Element of addMagma(# the carrier of G, the addF of G #) st
( h + g = e & g + 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 g being Element of addMagma(# the carrier of G, the addF of G #) st
( h + g = e & g + h = e )
reconsider g = g9 as Element of addMagma(# the carrier of G, the addF 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 = addMagma(# the carrier of G, the addF of G #) as non empty addGroup-like addMagma ;
dom the addF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def 1;
then the addF of H = the addF of G || the carrier of H by RELAT_1:68;
hence addMagma(# the carrier of G, the addF of G #) is strict Subgroup of G by DefA5; :: thesis: verum