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