theorem Th122: :: HILB10_7:122

for n, k, m being Nat
for f, g being FinSequence st f in doms (k,n) & g in doms (k,m) holds
f ^ g in doms (k,(n + m))