for X being RealUnitarySpace
for seq being sequence of X holds Sum (seq,0) = seq . 0 by Def1;