theorem Th120: :: HILB10_7:120

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