consider m being Nat such that
A1: (n + k) ! = (n !) * m by MDF, NAT_D:def 3;
thus ((n + k) !) / (n !) is natural by A1, XCMPLX_1:89; :: thesis: verum