for V being non empty Abelian add-associative right_zeroed addLoopStr
for S, T being finite Subset of V holds Sum (T \+\ S) = (Sum (T \ S)) + (Sum (S \ T)) by Th12, XBOOLE_1:82;