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:235;
then n = (n -' 1) + 1 ;
then ((m ! ) / (n ! )) * n = ((m ! ) / (((n -' 1) ! ) * n)) * n by NEWTON:21
.= (m ! ) / ((n -' 1) ! ) by A1, XCMPLX_1:93 ;
hence ((m ! ) / (n ! )) * n = (m ! ) / ((n -' 1) ! ) ; :: thesis: verum