let i, n be Nat; :: thesis: (i + 1) * (eta (((i + 1) + n),n)) = eta ((i + (n + 1)),(n + 1))
(i + 1) * (eta (((i + 1) + n),n)) = ((i + 1) * (((i + 1) + n) !)) / ((i + 1) !)
.= ((i + 1) * (((i + 1) + n) !)) / ((i + 1) * (i !)) by NEWTON:15
.= eta ((i + (n + 1)),(n + 1)) by XCMPLX_1:91 ;
hence (i + 1) * (eta (((i + 1) + n),n)) = eta ((i + (n + 1)),(n + 1)) ; :: thesis: verum