for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for LG being Linear_Combination of G
for g, h being Element of G holds g + (h + LG) = (g + h) + LG