theorem Th13: :: RLVECT_2:13

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for S, T being finite Subset of V holds Sum (T \/ S) = ((Sum T) + (Sum S)) - (Sum (T /\ S))