let f be Real_Sequence; :: thesis: for a, r being positive Real st r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds
( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) )
let a, r be positive Real; :: thesis: ( r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) implies ( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) ) )
assume A1: r < 1 ; :: thesis: ( ex n being Nat st not |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) or ( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) ) )
A2: r to_power 0 = 1 by POWER:24;
assume for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ; :: thesis: ( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) )
then |.((lim f) - (f . 0)).| <= (a * 1) / (1 - r) by A1, A2, Th7;
hence ( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) ) by Th1; :: thesis: verum