theorem Th5: :: POLNOT_1:5

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