let X be non empty set ; :: thesis: for s being sequence of X
for k, m being Nat holds (s ^\ k) ^\ m = s ^\ (k + m)
let s be sequence of X; :: thesis: for k, m being Nat holds (s ^\ k) ^\ m = s ^\ (k + m)
let k, m be Nat; :: thesis: (s ^\ k) ^\ m = s ^\ (k + m)

now

let n be Element of NAT ; :: thesis: ((s ^\ k) ^\ m) . n = (s ^\ (k + m)) . n
thus ((s ^\ k) ^\ m) . n = (s ^\ k) . (n + m) by Def3
.= s . ((n + m) + k) by Def3
.= s . (n + (k + m))
.= (s ^\ (k + m)) . n by Def3 ; :: thesis: verum

end;

hence (s ^\ k) ^\ m = s ^\ (k + m) by FUNCT_2:113; :: thesis: verum