for P being FinSequence-membered set
for m, n being Nat holds P ^^ (m + n) = (P ^^ m) ^ (P ^^ n)