let k be Nat; :: thesis: for X being non empty set
for s being sequence of X
for N being sequence of NAT holds (s * N) ^\ k = s * (N ^\ k)
let X be non empty set ; :: thesis: for s being sequence of X
for N being sequence of NAT holds (s * N) ^\ k = s * (N ^\ k)
let s be sequence of X; :: thesis: for N being sequence of NAT holds (s * N) ^\ k = s * (N ^\ k)
let N be sequence of NAT; :: thesis: (s * N) ^\ k = s * (N ^\ k)

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

let n be Element of NAT ; :: thesis: ((s * N) ^\ k) . n = (s * (N ^\ k)) . n
thus ((s * N) ^\ k) . n = (s * N) . (n + k) by Def2
.= s . (N . (n + k)) by FUNCT_2:15, ORDINAL1:def 12
.= s . ((N ^\ k) . n) by Def2
.= (s * (N ^\ k)) . n by FUNCT_2:15 ; :: thesis: verum

end;

hence (s * N) ^\ k = s * (N ^\ k) by FUNCT_2:63; :: thesis: verum