theorem Th121: :: HILB10_7:121

for n, k being Nat
for f being FinSequence st f in doms (n,k) holds
len f = k