for k being Element of NAT
for S being RealNormSpace
for seq being sequence of S st seq is non-zero holds
seq ^\ k is non-zero