theorem Th4: :: RUSUB_6:5

for V being RealUnitarySpace
for u being Point of V
for x being FinSequence of V holds u .|. (Sum x) = Sum (u .|. x)