let k, j be Nat; :: thesis: ( j <= k implies (j !) * (k choose j) = eta (k,j) )
assume A1: j <= k ; :: thesis: (j !) * (k choose j) = eta (k,j)
then 0 <= k - j by XREAL_1:48;
then reconsider kj1 = k - j as Nat by INT_1:3, ORDINAL1:def 12;
(j !) * (k choose j) = (j !) * ((k !) / ((j !) * (kj1 !))) by A1, NEWTON:def 3
.= ((j !) * (k !)) / ((j !) * (kj1 !))
.= (k !) / (kj1 !) by XCMPLX_1:91
.= eta (k,j) by A1, XREAL_1:233 ;
hence (j !) * (k choose j) = eta (k,j) ; :: thesis: verum