theorem Th35: :: NAT_1:48

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