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