theorem Th8: :: POLNOT_1:8

for P being FinSequence-membered set
for n being Nat holds P ^^ n c= P * by Th5;