for X being RealUnitarySpace
for seq being sequence of X
for k, m being Nat holds (seq ^\ k) ^\ m = seq ^\ (k + m)