let k, n be Nat; :: thesis: ( (n !) * (k !) = (n + k) ! iff ( n = 0 or k = 0 ) )
( n = (n + k) - k & n + k >= 0 + k ) by XREAL_1:6;
then ((n + k) choose (k * 1)) * ((n !) * (k !)) = (((n + k) !) / ((n !) * (k !))) * ((n !) * (k !)) by NEWTON:def 3
.= (n + k) ! by XCMPLX_1:87 ;
hence ( (n !) * (k !) = (n + k) ! iff ( n = 0 or k = 0 ) ) by NCK, XCMPLX_1:7; :: thesis: verum