let X be infinite Subset of NAT ; :: thesis: for i being natural number holds (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2))
let i be natural number ; :: thesis: (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2))
set r = 1 / 2;
A1: X -powers (1 / 2) is summable by Th21;

A2: now

let n be Element of 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:13; :: thesis: verum

end;

not X c= i + 1 ;
then consider a being set such that
A3: ( a in X & not a in i + 1 ) by TARSKI:def 3;
reconsider a = a, j = i as Element of NAT by A3, ORDINAL1:def 13;
A4: (Partial_Sums (X -powers (1 / 2))) . a <= Sum (X -powers (1 / 2)) by A1, A2, IRRAT_1:30;
j + 1 c= a by A3, ORDINAL1:26;
then j + 1 <= a by NAT_1:40;
then consider k being Nat such that
A5: a = (j + 1) + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
defpred S₁[ Element of NAT ] means (Partial_Sums (X -powers (1 / 2))) . i <= (Partial_Sums (X -powers (1 / 2))) . (i + $1);
A6: S₁[ 0 ] ;

A7: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

i + (k + 1) = (i + k) + 1 ;
then A9: (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 A2;
then ((Partial_Sums (X -powers (1 / 2))) . (j + k)) + 0 <= (Partial_Sums (X -powers (1 / 2))) . (j + (k + 1)) by A9, XREAL_1:8;
hence S₁[k + 1] by A8, XXREAL_0:2; :: thesis: verum

end;

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A6, A7);
then A10: (Partial_Sums (X -powers (1 / 2))) . i <= (Partial_Sums (X -powers (1 / 2))) . (i + k) ;
( (X -powers (1 / 2)) . a = (1 / 2) |^ a & j + (k + 1) = (j + k) + 1 ) by A3, Def5;
then (Partial_Sums (X -powers (1 / 2))) . a = ((Partial_Sums (X -powers (1 / 2))) . (j + k)) + ((1 / 2) |^ a) by A5, SERIES_1:def 1;
then A11: ((Partial_Sums (X -powers (1 / 2))) . i) + ((1 / 2) |^ a) <= (Partial_Sums (X -powers (1 / 2))) . a by A10, XREAL_1:8;
(1 / 2) |^ a > 0 by PREPOWER:13;
then ((Partial_Sums (X -powers (1 / 2))) . i) + ((1 / 2) |^ a) > ((Partial_Sums (X -powers (1 / 2))) . i) + 0 by XREAL_1:8;
then (Partial_Sums (X -powers (1 / 2))) . i < (Partial_Sums (X -powers (1 / 2))) . a by A11, XXREAL_0:2;
hence (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2)) by A4, XXREAL_0:2; :: thesis: verum