for X being RealUnitarySpace
for a being Real
for seq being sequence of X
for k being Nat holds (a * seq) ^\ k = a * (seq ^\ k)