for G being RealNormSpace
for k being Element of NAT
for s1 being Real_Sequence
for seq being sequence of G holds (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k