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_{1}( Nat) -> set = p / ($1 + 1);

consider d being Real_Sequence such that

A1: for n being Nat holds d . n = H_{1}(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 )

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

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

consider d being Real_Sequence such that

A1: for n being Nat holds d . n = H

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

then A3:
a = (seq_const x0) - d
by FUNCT_2:63;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;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

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