for X being RealNormSpace
for seq being sequence of X
for m being Nat holds 0 <= ||.seq.|| . m