theorem Th2: :: LOPBAN_3:2

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