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

now

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 8
.= a * ((seq ^\ k) . n) by NAT_1:def 3
.= (a * (seq ^\ k)) . n by NORMSP_1:def 8 ; :: thesis: verum

end;

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