theorem Th17: :: HILB10_4:17

for n, k being Nat st k > 0 & n > (2 * k) |^ (k + 1) holds
k ! = [\((n |^ k) / (n choose k))/]