theorem Th4: :: POLNOT_1:4

for P being FinSequence-membered set holds {} in P ^^ 0