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