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 ) )
deffunc H₁( Element of NAT ) -> Element of REAL = p / ($1 + 1);
consider d being Real_Sequence such that
A1: for n being Element of NAT holds d . n = H₁(n) from SEQ_1:sch 1();
x0 in REAL by XREAL_0:def 1;
then reconsider b = NAT --> x0 as Real_Sequence by FUNCOP_1:45;
assume A2: for n being Element of NAT holds a . n = x0 - (p / (n + 1)) ; :: thesis: ( a is convergent & lim a = x0 )

now

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

end;

then A3: a = b - d by FUNCT_2:63;
A4: d is convergent by A1, SEQ_4:31;
hence a is convergent by A3, SEQ_2:11; :: thesis: lim a = x0
A5: lim b = b . 0 by SEQ_4:26
.= x0 by FUNCOP_1:7 ;
lim d = 0 by A1, SEQ_4:31;
hence lim a = x0 - 0 by A4, A5, A3, SEQ_2:12
.= x0 ;
:: thesis: verum