theorem Th17: :: POLNOT_1:17

for P, Q being FinSequence-membered set st P c= Q holds
for n being Nat holds P ^^ n c= Q ^^ n