let k, n be Nat; :: thesis: (n !) * (k !) <= (n + k) !
set s = (n + k) choose n;
set l = n + k;
( k = (n + k) - n & n + k >= n + 0 ) by XREAL_1:6;
then A2: ((n + k) choose n) * ((n !) * (k !)) = (((n + k) !) / ((n !) * (k !))) * ((n !) * (k !)) by NEWTON:def 3
.= (n + k) ! by XCMPLX_1:87 ;
((n + k) choose n) * ((n !) * (k !)) >= 1 * ((n !) * (k !)) by XREAL_1:64, NAT_1:14;
hence (n !) * (k !) <= (n + k) ! by A2; :: thesis: verum