for G being addGroup
for a being Element of G holds
( ([#] the carrier of G) + a = the carrier of G & a + ([#] the carrier of G) = the carrier of G ) by ThX17;