let r, g be Real; :: thesis: for seq being Real_Sequence st ( for n being Nat holds seq . n = g / (n + r) ) holds
( seq is convergent & lim seq = 0 )
let seq be Real_Sequence; :: thesis: ( ( for n being Nat holds seq . n = g / (n + r) ) implies ( seq is convergent & lim seq = 0 ) )
assume A2: for n being Nat holds seq . n = g / (n + r) ; :: thesis: ( seq is convergent & lim seq = 0 )
reconsider r1 = r as Real ;
deffunc H₁( Nat) -> set = 1 / ($1 + r1);
consider seq1 being Real_Sequence such that
A3: for n being Nat holds seq1 . n = H₁(n) from SEQ_1:sch 1();

A4: now :: thesis: for n being Element of NAT holds (g (#) seq1) . n = seq . n

let n be Element of NAT ; :: thesis: (g (#) seq1) . n = seq . n
thus (g (#) seq1) . n = g * (seq1 . n) by SEQ_1:9
.= g * (1 / (n + r)) by A3
.= g * (1 * ((n + r) "))
.= g / (n + r)
.= seq . n by A2 ; :: thesis: verum

end;

A5: g (#) seq1 is convergent by A3, Th28, SEQ_2:7;
lim (g (#) seq1) = g * (lim seq1) by A3, Th28, SEQ_2:8
.= g * 0 by A3, Th29
.= 0 ;
hence ( seq is convergent & lim seq = 0 ) by A5, A4, FUNCT_2:63; :: thesis: verum