(k -' j) ! divides k ! by NAT_D:35, NUMBER08:6;
then consider l being Nat such that
A1: k ! = ((k -' j) !) * l by NAT_D:def 3;
(k !) / ((k -' j) !) is Nat by A1, XCMPLX_1:89;
hence (k !) / ((k -' j) !) is Element of NAT by ORDINAL1:def 12; :: thesis: verum