let f be summable Real_Sequence; :: thesis: for n being Nat st f is positive-yielding holds
Sum (f ^\ (n + 1)) > 0
let n be Nat; :: thesis: ( f is positive-yielding implies Sum (f ^\ (n + 1)) > 0 )
assume A0: f is positive-yielding ; :: thesis: Sum (f ^\ (n + 1)) > 0
set LS = f ^\ (n + 1);
A2: for i being Nat holds 0 <= (f ^\ (n + 1)) . i
proof
let i be Nat; :: thesis: 0 <= (f ^\ (n + 1)) . i
a1: (f ^\ (n + 1)) . i = f . ((n + 1) + i) by NAT_1:def 3;
(n + 1) + i in NAT by ORDINAL1:def 12;
then (n + 1) + i in dom f by FUNCT_2:def 1;
then f . ((n + 1) + i) in rng f by FUNCT_1:3;
hence 0 <= (f ^\ (n + 1)) . i by PARTFUN3:def 1, A0, a1; :: thesis: verum
end;
ex i being Nat st
( i in dom (f ^\ (n + 1)) & 0 < (f ^\ (n + 1)) . i )
proof
consider j being Nat such that
A3: n + 1 <= j ;
j - (n + 1) in NAT by A3, INT_1:5;
then reconsider i = j - (n + 1) as Nat ;
take i ; :: thesis: ( i in dom (f ^\ (n + 1)) & 0 < (f ^\ (n + 1)) . i )
A4: (n + 1) + i = j ;
aa: dom (f ^\ (n + 1)) = NAT by FUNCT_2:def 1;
A6: (f ^\ (n + 1)) . i = f . j by NAT_1:def 3, A4;
j in NAT by ORDINAL1:def 12;
then j in dom f by FUNCT_2:def 1;
then f . j in rng f by FUNCT_1:3;
hence ( i in dom (f ^\ (n + 1)) & 0 < (f ^\ (n + 1)) . i ) by aa, A6, A0, PARTFUN3:def 1, ORDINAL1:def 12; :: thesis: verum
end;
then consider k being Nat such that
A6: ( k in dom (f ^\ (n + 1)) & (f ^\ (n + 1)) . k > 0 ) ;
f ^\ (n + 1) is summable by SERIES_1:12;
hence Sum (f ^\ (n + 1)) > 0 by A6, RSSPACE2:3, A2; :: thesis: verum