let r, g be real number ; :: thesis: for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = g / (n + r) ) holds
( seq is convergent & lim seq = 0 )
let seq be Real_Sequence; :: thesis: ( 0 <= r & ( for n being Element of NAT holds seq . n = g / (n + r) ) implies ( seq is convergent & lim seq = 0 ) )
assume that
A1: 0 <= r and
A2: for n being Element of NAT holds seq . n = g / (n + r) ; :: thesis: ( seq is convergent & lim seq = 0 )
reconsider r1 = r as Real by XREAL_0:def 1;
deffunc H₁( Element of NAT ) -> Element of COMPLEX = 1 / ($1 + r1);
consider seq1 being Real_Sequence such that
A3: for n being Element of NAT holds seq1 . n = H₁(n) from SEQ_1:sch 1();

A4: now

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

end;

A5: g (#) seq1 is convergent by A1, A3, Th43, SEQ_2:21;
lim (g (#) seq1) = g * (lim seq1) by A1, A3, Th43, SEQ_2:22
.= g * 0 by A1, A3, Th44
.= 0 ;
hence ( seq is convergent & lim seq = 0 ) by A5, A4, FUNCT_2:113; :: thesis: verum