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