let X be non empty set ; :: thesis: for s being sequence of X
for k being Nat
for N being sequence of NAT holds (s * N) ^\ k = s * (N ^\ k)
let s be sequence of X; :: thesis: for k being Nat
for N being sequence of NAT holds (s * N) ^\ k = s * (N ^\ k)
let k be Nat; :: 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

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 Def3
.= s . (N . (n + k)) by FUNCT_2:21
.= s . ((N ^\ k) . n) by Def3
.= (s * (N ^\ k)) . n by FUNCT_2:21 ; :: thesis: verum

end;

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