theorem Th5: :: RUSUB_6:6

for V being RealUnitarySpace
for u being Point of V
for n being Nat
for x being FinSequence of V st 1 <= n & n <= len x & ( for i being Nat st 1 <= i & i <= len x & n <> i holds
u .|. (x /. i) = 0 ) holds
u .|. (Sum x) = u .|. (x /. n)