theorem :: CLVECT_2:89

for X being ComplexUnitarySpace
for z being Complex
for seq being sequence of X
for k being Nat holds (z * seq) ^\ k = z * (seq ^\ k)