theorem Th15: :: HILB10_4:15

for n, k, u being Nat st u > n |^ k & n >= k holds
[\(((u + 1) |^ n) / (u |^ k))/] mod u = n choose k