for X being RealUnitarySpace
for seq being sequence of X holds Sum (seq,1) = (Sum (seq,0)) + (seq . 1)