for P being FinSequence-membered set holds P ^^ 1 = P