theorem Th48: :: HILB10_7:48

for F, G being FinSequence-yielding FinSequence
for f, g being FinSequence st f in doms F & g in doms G holds
f ^ g in doms (F ^ G)