let n be Nat; :: thesis: ( 1 - (1 / (n + 2)) = (n + 1) / (n + 2) & 1 / ((n + 1) !) = (n + 2) / (((n + 1) !) * (n + 2)) )
n >= 0 by NAT_1:2;
then n + 1 > 0 by NAT_1:13;
then A1: (n + 1) + 1 > 0 by NAT_1:13;
then A2: 1 / ((n + 1) !) = (1 * (n + 2)) / (((n + 1) !) * (n + 2)) by XCMPLX_1:91;
(n + 1) / (n + 2) = ((n + 2) - 1) / (n + 2)
.= ((n + 2) / (n + 2)) - (1 / (n + 2)) by XCMPLX_1:120
.= 1 - (1 / (n + 2)) by A1, XCMPLX_1:60 ;
hence ( 1 - (1 / (n + 2)) = (n + 1) / (n + 2) & 1 / ((n + 1) !) = (n + 2) / (((n + 1) !) * (n + 2)) ) by A2; :: thesis: verum