let n, m be Element of NAT ; :: thesis: ( n > 1 implies ((m !) / (n !)) * n = (m !) / ((n -' 1) !) )
assume A1: n > 1 ; :: thesis: ((m !) / (n !)) * n = (m !) / ((n -' 1) !)
then n - 1 = n -' 1 by XREAL_1:233;
then n = (n -' 1) + 1 ;
then ((m !) / (n !)) * n = ((m !) / (((n -' 1) !) * n)) * n by NEWTON:15
.= (m !) / ((n -' 1) !) by A1, XCMPLX_1:92 ;
hence ((m !) / (n !)) * n = (m !) / ((n -' 1) !) ; :: thesis: verum