let r, g be Real; :: thesis: for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = g / ((n * n) + r) ) holds
( seq is convergent & lim seq = 0 )
let seq be Real_Sequence; :: thesis: ( 0 <= r & ( for n being Nat holds seq . n = g / ((n * n) + r) ) implies ( seq is convergent & lim seq = 0 ) )
assume that
A1: 0 <= r and
A2: for n being Nat holds seq . n = g / ((n * n) + r) ; :: thesis: ( seq is convergent & lim seq = 0 )
reconsider r1 = r as Real ;
deffunc H₁( Nat) -> set = 1 / (($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 * n) + r)) by A3
.= g * (1 * (((n * n) + r) "))
.= g / ((n * n) + r)
.= seq . n by A2 ; :: thesis: verum

end;

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