for S being RealNormSpace
for seq, seq1 being sequence of S
for k being Nat holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)