let n be Nat; :: thesis: Reci-seq1 . n = (1 / (n - (1 / 2))) - (1 / (n + (1 / 2)))
set a = 1 / 2;
1 / 2 is not Nat

proof

assume A4: 1 / 2 is Nat ; :: thesis: contradiction
( 0 <= 1 / 2 & 1 / 2 <= 0 + 1 ) ;
hence contradiction by A4, NAT_1:9; :: thesis: verum

end;

then A2: n - (1 / 2) <> 0 ;
(1 / (n - (1 / 2))) - (1 / (n + (1 / 2))) = ((1 * (n + (1 / 2))) / ((n - (1 / 2)) * (n + (1 / 2)))) - (1 / (n + (1 / 2))) by XCMPLX_1:91
.= ((1 * (n + (1 / 2))) / ((n - (1 / 2)) * (n + (1 / 2)))) - ((1 * (n - (1 / 2))) / ((n + (1 / 2)) * (n - (1 / 2)))) by A2, XCMPLX_1:91
.= ((n + (1 / 2)) - (n - (1 / 2))) / ((n + (1 / 2)) * (n - (1 / 2))) by XCMPLX_1:120
.= 1 / ((n ^2) - (1 / 4)) ;
hence Reci-seq1 . n = (1 / (n - (1 / 2))) - (1 / (n + (1 / 2))) by MyDef; :: thesis: verum