theorem Th17: :: E_TRANS1:5

for k, j being Nat st j <= k holds
(j !) * (k choose j) = eta (k,j)