let p be Real; :: thesis: for a being Real_Sequence
for x0 being Real st ( for n being 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 st ( for n being Nat holds a . n = x0 - (p / (n + 1)) ) holds
( a is convergent & lim a = x0 )
let x0 be Real; :: thesis: ( ( for n being Nat holds a . n = x0 - (p / (n + 1)) ) implies ( a is convergent & lim a = x0 ) )
deffunc H₁( Nat) -> set = p / ($1 + 1);
consider d being Real_Sequence such that
A1: for n being Nat holds d . n = H₁(n) from SEQ_1:sch 1();
set b = seq_const x0;
assume A2: for n being Nat holds a . n = x0 - (p / (n + 1)) ; :: thesis: ( a is convergent & lim a = x0 )

now :: thesis: for n being Element of NAT holds ((seq_const x0) - d) . n = a . n

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

end;

then A3: a = (seq_const x0) - d by FUNCT_2:63;
A4: d is convergent by A1, SEQ_4:31;
hence a is convergent by A3; :: thesis: lim a = x0
A5: lim (seq_const x0) = (seq_const x0) . 0 by SEQ_4:26
.= x0 by SEQ_1:57 ;
lim d = 0 by A1, SEQ_4:31;
hence lim a = x0 - 0 by A4, A5, A3, SEQ_2:12
.= x0 ;
:: thesis: verum