theorem Th123: :: HILB10_7:123

for n, k, m being Nat holds (doms (k,n)) ^ (doms (k,m)) = doms (k,(n + m))