let k be Element of NAT ; :: thesis: (1 / (k + 1)) * (1 / (k !)) = 1 / ((k + 1) !)
thus (1 / (k + 1)) * (1 / (k !)) = 1 / ((k + 1) * (k !)) by XCMPLX_1:103
.= 1 / ((k + 1) !) by NEWTON:21 ; :: thesis: verum