let n be Nat; :: thesis: (Partial_Sums ReciTriangRS) . n = 2 - (2 / (n + 1))
defpred S₁[ Nat] means (Partial_Sums ReciTriangRS) . $1 = 2 - (2 / ($1 + 1));
A1: S₁[ 0 ]

proof

ReciTriangRS . 0 = 0 ;
hence S₁[ 0 ] by SERIES_1:def 1; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
A4: ReciTriangRS . (k + 1) = 1 / (Triangle (k + 1)) by Def13
.= 2 / ((k + 1) * ((k + 1) + 1)) by Th83
.= 2 / (((k * k) + (3 * k)) + 2) ;
A5: (k + 2) / (k + 2) = 1 by XCMPLX_1:60;
A6: (k + 1) / (k + 1) = 1 by XCMPLX_1:60;
(Partial_Sums ReciTriangRS) . (k + 1) = ((2 * ((k + 2) / (k + 2))) - ((2 / (k + 1)) * 1)) + (2 / ((k + 1) * (k + 2))) by A5, A3, A4, SERIES_1:def 1
.= (((2 * (k + 2)) / (k + 2)) - ((2 / (k + 1)) * ((k + 2) / (k + 2)))) + (2 / ((k + 1) * (k + 2))) by XCMPLX_1:74, A5
.= ((((2 * (k + 2)) / (k + 2)) * ((k + 1) / (k + 1))) - ((2 * (k + 2)) / ((k + 1) * (k + 2)))) + (2 / ((k + 1) * (k + 2))) by A6, XCMPLX_1:76
.= ((((2 * (k + 2)) * (k + 1)) / ((k + 2) * (k + 1))) - ((2 * (k + 2)) / ((k + 1) * (k + 2)))) + (2 / ((k + 1) * (k + 2))) by XCMPLX_1:76
.= ((((((2 * k) * k) + (6 * k)) + 4) - ((2 * k) + 4)) / ((k + 2) * (k + 1))) + (2 / ((k + 1) * (k + 2))) by XCMPLX_1:120
.= ((((((2 * k) * k) + (6 * k)) + 4) - ((2 * k) + 4)) + 2) / ((k + 2) * (k + 1)) by XCMPLX_1:62
.= ((2 * (k + 1)) * (k + 1)) / ((k + 2) * (k + 1))
.= ((2 * (k + 2)) - 2) / (k + 2) by XCMPLX_1:91
.= ((2 * (k + 2)) / (k + 2)) - (2 / (k + 2)) by XCMPLX_1:120
.= 2 - (2 / (k + 2)) by XCMPLX_1:89 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence (Partial_Sums ReciTriangRS) . n = 2 - (2 / (n + 1)) ; :: thesis: verum