set H = addMagma(# the carrier of G, the addF of G #);
addMagma(# the carrier of G, the addF of G #) is addGroup-like
proof
reconsider t = 0_ G as Element of addMagma(# the carrier of G, the addF of G #) ;
take t ; :: according to GROUP_1A:def 2 :: thesis: for h being Element of addMagma(# the carrier of G, the addF of G #) holds
( h + t = h & t + h = h & ex g being Element of addMagma(# the carrier of G, the addF of G #) st
( h + g = t & g + h = t ) )
let a be Element of addMagma(# the carrier of G, the addF of G #); :: thesis: ( a + t = a & t + a = a & ex g being Element of addMagma(# the carrier of G, the addF of G #) st
( a + g = t & g + a = t ) )
reconsider x = a as Element of G ;
thus a + t = x + (0_ G)
.= a by Def4 ; :: thesis: ( t + a = a & ex g being Element of addMagma(# the carrier of G, the addF of G #) st
( a + g = t & g + a = t ) )
thus t + a = (0_ G) + x
.= a by Def4 ; :: thesis: ex g being Element of addMagma(# the carrier of G, the addF of G #) st
( a + g = t & g + a = t )
reconsider s = - x as Element of addMagma(# the carrier of G, the addF of G #) ;
take s ; :: thesis: ( a + s = t & s + a = t )
thus a + s = x + (- x)
.= t by Def5 ; :: thesis: s + a = t
thus s + a = (- x) + x
.= t by Def5 ; :: thesis: verum
end;
then reconsider H = addMagma(# the carrier of G, the addF of G #) as non empty addGroup-like addMagma ;
the addF of H = the addF of G || the carrier of H by RELSET_1:19;
then H is Subgroup of G by DefA5;
hence ex b1 being Subgroup of G st b1 is strict ; :: thesis: verum