let n be Nat; :: thesis: 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; :: thesis: verum