let f be Real_Sequence; :: thesis: for a, r being positive real number st r < 1 & ( for n being natural number 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 number ; :: thesis: ( r < 1 & ( for n being natural number 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 natural number 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)) ) )
assume A2: for n being natural number 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)) )
r to_power 0 = 1 by POWER:29;
then |.((lim f) - (f . 0 )).| <= (a * 1) / (1 - r) by A1, A2, Th9;
hence ( lim f >= (f . 0 ) - (a / (1 - r)) & lim f <= (f . 0 ) + (a / (1 - r)) ) by Th1; :: thesis: verum