for P being FinSequence-membered set holds
( P ^^ 0 = {{}} & ( for n being Nat holds P ^^ (n + 1) = (P ^^ n) ^ P ) )