let p be Real; :: thesis: for a being Real_Sequence
for x0 being real number st ( for n being Element of NAT holds a . n = x0 + (p / (n + 1)) ) holds
( a is convergent & lim a = x0 )
let a be Real_Sequence; :: thesis: for x0 being real number st ( for n being Element of NAT holds a . n = x0 + (p / (n + 1)) ) holds
( a is convergent & lim a = x0 )
let x0 be real number ; :: thesis: ( ( for n being Element of NAT holds a . n = x0 + (p / (n + 1)) ) implies ( a is convergent & lim a = x0 ) )
assume A1: for n being Element of NAT holds a . n = x0 + (p / (n + 1)) ; :: thesis: ( a is convergent & lim a = x0 )
x0 in REAL by XREAL_0:def 1;
then reconsider b = NAT --> x0 as Real_Sequence by FUNCOP_1:57;
deffunc H₁( Element of NAT ) -> Element of REAL = p / ($1 + 1);
consider d being Real_Sequence such that
A2: for n being Element of NAT holds d . n = H₁(n) from SEQ_1:sch 1();
A3: ( d is convergent & lim d = 0 ) by A2, SEQ_4:46;
A5: lim b = b . 0 by SEQ_4:41
.= x0 by FUNCOP_1:13 ;

now

let n be Element of NAT ; :: thesis: (b + d) . n = a . n
thus (b + d) . n = (b . n) + (d . n) by VALUED_1:1
.= x0 + (d . n) by FUNCOP_1:13
.= x0 + (p / (n + 1)) by A2
.= a . n by A1 ; :: thesis: verum

end;

then A6: a = b + d by FUNCT_2:113;
hence a is convergent by A3, SEQ_2:19; :: thesis: lim a = x0
thus lim a = x0 + 0 by A3, A5, A6, SEQ_2:20
.= x0 ; :: thesis: verum