for k being Element of NAT
for S being RealNormSpace
for seq, seq1 being sequence of S holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)