let k be Nat; :: thesis: (1 / (k + 1)) * (1 / (k !)) = 1 / ((k + 1) !)
thus (1 / (k + 1)) * (1 / (k !)) = 1 / ((k + 1) * (k !)) by XCMPLX_1:102
.= 1 / ((k + 1) !) by NEWTON:15 ; :: thesis: verum