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