let k be Nat; :: thesis: for r being Real
for seq being Real_Sequence holds (r (#) seq) ^\ k = r (#) (seq ^\ k)
let r be Real; :: thesis: for seq being Real_Sequence holds (r (#) seq) ^\ k = r (#) (seq ^\ k)
let seq be Real_Sequence; :: thesis: (r (#) seq) ^\ k = r (#) (seq ^\ k)

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

let n be Element of NAT ; :: thesis: ((r (#) seq) ^\ k) . n = (r (#) (seq ^\ k)) . n
thus ((r (#) seq) ^\ k) . n = (r (#) seq) . (n + k) by NAT_1:def 3
.= r * (seq . (n + k)) by SEQ_1:9
.= r * ((seq ^\ k) . n) by NAT_1:def 3
.= (r (#) (seq ^\ k)) . n by SEQ_1:9 ; :: thesis: verum

end;

hence (r (#) seq) ^\ k = r (#) (seq ^\ k) by FUNCT_2:63; :: thesis: verum