let X be RealUnitarySpace; :: thesis: for a being Real
for seq being sequence of X
for k being Nat holds (a * seq) ^\ k = a * (seq ^\ k)
let a be Real; :: thesis: for seq being sequence of X
for k being Nat holds (a * seq) ^\ k = a * (seq ^\ k)
let seq be sequence of X; :: thesis: for k being Nat holds (a * seq) ^\ k = a * (seq ^\ k)
let k be Nat; :: thesis: (a * seq) ^\ k = a * (seq ^\ k)

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

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

end;

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