let n be Nat; :: thesis: for a, b being Real holds (rseq (0,1,a,b)) . n = 1 / ((a * n) + b)
let a, b be Real; :: thesis: (rseq (0,1,a,b)) . n = 1 / ((a * n) + b)
(rseq (0,1,a,b)) . n = ((0 * n) + 1) / ((a * n) + b) by BASEL_1:5;
hence (rseq (0,1,a,b)) . n = 1 / ((a * n) + b) ; :: thesis: verum