for P being FinSequence-membered set
for a being object holds
( a in P * iff ex n being Nat st a in P ^^ n )