set r = 1 / 2;
let X be infinite Subset of NAT; :: thesis: for i being Nat holds (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2))
let i be Nat; :: thesis: (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2))
defpred S1[ Nat] means (Partial_Sums (X -powers (1 / 2))) . i <= (Partial_Sums (X -powers (1 / 2))) . (i + $1);
not X c= i + 1 ;
then consider a being object such that
A1: a in X and
A2: not a in i + 1 ;
reconsider a = a, j = i as Element of NAT by A1, ORDINAL1:def 12;
A3: (X -powers (1 / 2)) . a = (1 / 2) |^ a by A1, Def5;
A4: now :: thesis: for n being Nat holds 0 <= (X -powers (1 / 2)) . n
let n be Nat; :: thesis: 0 <= (X -powers (1 / 2)) . n
( ( n in X & (X -powers (1 / 2)) . n = (1 / 2) |^ n ) or ( not n in X & (X -powers (1 / 2)) . n = 0 ) ) by Def5;
hence 0 <= (X -powers (1 / 2)) . n by PREPOWER:6; :: thesis: verum
end;
A5: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; :: thesis: S1[k + 1]
i + (k + 1) = (i + k) + 1 ;
then A7: (Partial_Sums (X -powers (1 / 2))) . (j + (k + 1)) = ((Partial_Sums (X -powers (1 / 2))) . (j + k)) + ((X -powers (1 / 2)) . (j + (k + 1))) by SERIES_1:def 1;
(X -powers (1 / 2)) . (j + (k + 1)) >= 0 by A4;
then ((Partial_Sums (X -powers (1 / 2))) . (j + k)) + 0 <= (Partial_Sums (X -powers (1 / 2))) . (j + (k + 1)) by A7, XREAL_1:6;
hence S1[k + 1] by A6, XXREAL_0:2; :: thesis: verum
end;
Segm (j + 1) c= Segm a by A2, ORDINAL1:16;
then j + 1 <= a by NAT_1:39;
then consider k being Nat such that
A8: a = (j + 1) + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
(1 / 2) |^ a > 0 by PREPOWER:6;
then A9: ((Partial_Sums (X -powers (1 / 2))) . i) + ((1 / 2) |^ a) > ((Partial_Sums (X -powers (1 / 2))) . i) + 0 by XREAL_1:6;
A10: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A10, A5);
 then A11: (Partial_Sums (X -powers (1 / 2))) . i <= (Partial_Sums (X -powers (1 / 2))) . (i + k) ;
j + (k + 1) = (j + k) + 1 ;
then (Partial_Sums (X -powers (1 / 2))) . a = ((Partial_Sums (X -powers (1 / 2))) . (j + k)) + ((1 / 2) |^ a) by A3, A8, SERIES_1:def 1;
then ((Partial_Sums (X -powers (1 / 2))) . i) + ((1 / 2) |^ a) <= (Partial_Sums (X -powers (1 / 2))) . a by A11, XREAL_1:6;
then A12: (Partial_Sums (X -powers (1 / 2))) . i < (Partial_Sums (X -powers (1 / 2))) . a by A9, XXREAL_0:2;
(Partial_Sums (X -powers (1 / 2))) . a <= Sum (X -powers (1 / 2)) by Th21, A4, IRRAT_1:29;
hence (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2)) by A12, XXREAL_0:2; :: thesis: verum