theorem Th7: :: POLNOT_1:7

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