theorem Th10: :: POLNOT_1:10

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