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