let X be ComplexUnitarySpace; :: thesis: for z being Complex
for seq being sequence of X
for k being Nat holds (z * seq) ^\ k = z * (seq ^\ k)
let z be Complex; :: thesis: for seq being sequence of X
for k being Nat holds (z * seq) ^\ k = z * (seq ^\ k)
let seq be sequence of X; :: thesis: for k being Nat holds (z * seq) ^\ k = z * (seq ^\ k)
let k be Nat; :: thesis: (z * seq) ^\ k = z * (seq ^\ k)

now :: thesis: for n being Element of NAT holds ((z * seq) ^\ k) . n = (z * (seq ^\ k)) . n

let n be Element of NAT ; :: thesis: ((z * seq) ^\ k) . n = (z * (seq ^\ k)) . n
thus ((z * seq) ^\ k) . n = (z * seq) . (n + k) by NAT_1:def 3
.= z * (seq . (n + k)) by CLVECT_1:def 14
.= z * ((seq ^\ k) . n) by NAT_1:def 3
.= (z * (seq ^\ k)) . n by CLVECT_1:def 14 ; :: thesis: verum

end;

hence (z * seq) ^\ k = z * (seq ^\ k) by FUNCT_2:63; :: thesis: verum