theorem Th32: :: IRRAT_1:32

for k, n being Nat holds (n !) * (eseq . k) = (n !) / (k !)