let n be Nat; :: thesis: for s being Real_Sequence st ( for n being Nat holds s . n = 1 / ((2 -Root (n + 1)) + (2 -Root n)) ) holds

(Partial_Sums s) . n = 2 -Root (n + 1)

let s be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n = 1 / ((2 -Root (n + 1)) + (2 -Root n)) ) implies (Partial_Sums s) . n = 2 -Root (n + 1) )

defpred S_{1}[ Nat] means (Partial_Sums s) . $1 = 2 -Root ($1 + 1);

assume A1: for n being Nat holds s . n = 1 / ((2 -Root (n + 1)) + (2 -Root n)) ; :: thesis: (Partial_Sums s) . n = 2 -Root (n + 1)

A2: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

.= 1 / ((2 -Root (0 + 1)) + (2 -Root 0)) by A1

.= 1 / ((2 -Root (0 + 1)) + 0) by PREPOWER:def 2

.= 1 / 1 by PREPOWER:20

.= 2 -Root (0 + 1) by PREPOWER:20 ;

then A3: S_{1}[ 0 ]
;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A3, A2);

hence (Partial_Sums s) . n = 2 -Root (n + 1) ; :: thesis: verum

(Partial_Sums s) . n = 2 -Root (n + 1)

let s be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n = 1 / ((2 -Root (n + 1)) + (2 -Root n)) ) implies (Partial_Sums s) . n = 2 -Root (n + 1) )

defpred S

assume A1: for n being Nat holds s . n = 1 / ((2 -Root (n + 1)) + (2 -Root n)) ; :: thesis: (Partial_Sums s) . n = 2 -Root (n + 1)

A2: for n being Nat st S

S

proof

(Partial_Sums s) . 0 =
s . 0
by SERIES_1:def 1
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume (Partial_Sums s) . n = 2 -Root (n + 1) ; :: thesis: S_{1}[n + 1]

then (Partial_Sums s) . (n + 1) = (2 -Root (n + 1)) + (s . (n + 1)) by SERIES_1:def 1

.= (2 -Root (n + 1)) + (1 / ((2 -Root ((n + 1) + 1)) + (2 -Root (n + 1)))) by A1

.= (2 -Root (n + 1)) + ((2 -Root (n + 2)) - (2 -Root (n + 1))) by Lm7

.= 2 -Root (n + 2) ;

hence S_{1}[n + 1]
; :: thesis: verum

end;assume (Partial_Sums s) . n = 2 -Root (n + 1) ; :: thesis: S

then (Partial_Sums s) . (n + 1) = (2 -Root (n + 1)) + (s . (n + 1)) by SERIES_1:def 1

.= (2 -Root (n + 1)) + (1 / ((2 -Root ((n + 1) + 1)) + (2 -Root (n + 1)))) by A1

.= (2 -Root (n + 1)) + ((2 -Root (n + 2)) - (2 -Root (n + 1))) by Lm7

.= 2 -Root (n + 2) ;

hence S

.= 1 / ((2 -Root (0 + 1)) + (2 -Root 0)) by A1

.= 1 / ((2 -Root (0 + 1)) + 0) by PREPOWER:def 2

.= 1 / 1 by PREPOWER:20

.= 2 -Root (0 + 1) by PREPOWER:20 ;

then A3: S

for n being Nat holds S

hence (Partial_Sums s) . n = 2 -Root (n + 1) ; :: thesis: verum