let G be RealNormSpace; :: thesis: for k being Element of NAT
for s1 being Real_Sequence
for seq being sequence of G holds (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k
let k be Element of NAT ; :: thesis: for s1 being Real_Sequence
for seq being sequence of G holds (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k
let s1 be Real_Sequence; :: thesis: for seq being sequence of G holds (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k
let seq be sequence of G; :: thesis: (s1 ^\ k) (#) (seq ^\ k) = (s1 (#) seq) ^\ k

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

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

end;

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