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 H1( Nat) -> set = p / (\$1 + 1);
consider d being Real_Sequence such that
A1: for n being Nat holds d . n = H1(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 (() + d) . n = a . n
let n be Element of NAT ; :: thesis: (() + d) . n = a . n
thus (() + d) . n = (() . n) + (d . n) by VALUED_1:1
.= x0 + (d . n) by SEQ_1:57
.= x0 + (p / (n + 1)) by A1
.= a . n by A2 ; :: thesis: verum
end;
then A3: a = () + d by FUNCT_2:63;
A4: d is convergent by ;
hence a is convergent by A3; :: thesis: lim a = x0
A5: lim () = () . 0 by SEQ_4:26
.= x0 by SEQ_1:57 ;
lim d = 0 by ;
hence lim a = x0 + 0 by
.= x0 ;
:: thesis: verum