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

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

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 Def2
.= s . ((n + m) + k) by Def2
.= s . (n + (k + m))
.= (s ^\ (k + m)) . n by Def2 ; :: thesis: verum

end;

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