:: deftheorem Def1 defines + RLAFFIN1:def 1 :
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for LG being Linear_Combination of G
for g being Element of G
for b₄ being Linear_Combination of G holds
( b₄ = g + LG iff for h being Element of G holds b₄ . h = LG . (h - g) );