theorem Th49: :: HILB10_7:49

for F, G being FinSequence-yielding FinSequence
for P, S being FinSequence-membered set st P c= doms F & S c= doms G holds
P ^ S c= doms (F ^ G)