let n be Nat; :: thesis: (Partial_Sums Reci-seq1) . n < - 2
set s = Reci-seq1 ;
set a = rseq (0,1,1,(- (1 / 2)));
set b = - (rseq (0,1,1,(1 / 2)));
ff: for k being Nat holds (- (rseq (0,1,1,(1 / 2)))) . k = - ((rseq (0,1,1,(- (1 / 2)))) . (k + 1))

proof

let k be Nat; :: thesis: (- (rseq (0,1,1,(1 / 2)))) . k = - ((rseq (0,1,1,(- (1 / 2)))) . (k + 1))
(- (rseq (0,1,1,(1 / 2)))) . k = - ((rseq (0,1,1,(1 / 2))) . k) by VALUED_1:8
.= - (1 / ((1 * k) + (1 / 2))) by AlgDef
.= - (1 / ((1 * (k + 1)) + (- (1 / 2))))
.= - ((rseq (0,1,1,(- (1 / 2)))) . (k + 1)) by AlgDef ;
hence (- (rseq (0,1,1,(1 / 2)))) . k = - ((rseq (0,1,1,(- (1 / 2)))) . (k + 1)) ; :: thesis: verum

end;

w3: (rseq (0,1,1,(- (1 / 2)))) . 0 = 1 / ((1 * 0) + (- (1 / 2))) by AlgDef
.= - 2 ;
(- (rseq (0,1,1,(1 / 2)))) . n = - ((rseq (0,1,1,(1 / 2))) . n) by VALUED_1:8
.= - (1 / ((1 * n) + (1 / 2))) by AlgDef
.= - (1 / (n + (1 / 2))) ;
then (- 2) + ((- (rseq (0,1,1,(1 / 2)))) . n) < (- 2) + 0 by XREAL_1:8;
hence (Partial_Sums Reci-seq1) . n < - 2 by w3, ff, Telescoping, Tele2; :: thesis: verum