let n be Nat; Reci-seq1 . n = ((rseq (0,1,1,(- (1 / 2)))) . n) + ((- (rseq (0,1,1,(1 / 2)))) . n)
A3: Reci-seq1 . n =
(1 / (n - (1 / 2))) - (1 / (n + (1 / 2)))
by Tele1
.=
(1 / (n - (1 / 2))) + (- (1 / (n + (1 / 2))))
;
A1:
(rseq (0,1,1,(- (1 / 2)))) . n = 1 / ((1 * n) + (- (1 / 2)))
by AlgDef;
(- (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
;
hence
Reci-seq1 . n = ((rseq (0,1,1,(- (1 / 2)))) . n) + ((- (rseq (0,1,1,(1 / 2)))) . n)
by A1, A3; verum