let eps be R_eal; :: thesis: ( 0. < eps implies ex F being Function of NAT ,ExtREAL st
( ( for n being Element of NAT holds 0. < F . n ) & SUM F < eps ) )
assume 0. < eps ; :: thesis: ex F being Function of NAT ,ExtREAL st
( ( for n being Element of NAT holds 0. < F . n ) & SUM F < eps )
then consider x0 being real number such that
A1: ( 0. < x0 & x0 < eps ) by XXREAL_3:3;
consider x being real number such that
A2: ( 0. < x & x + x < x0 ) by A1, XXREAL_3:56;
reconsider x = x as Element of ExtREAL by XXREAL_0:def 1;
defpred S1[ set , set , set ] means for a, b being R_eal
for s being Element of NAT st s = $1 & a = $2 & b = $3 holds
b = a / 2;
A3: for n being Element of NAT
for x being Element of ExtREAL ex y being Element of ExtREAL st S1[n,x,y]
proof
let n be Element of NAT ; :: thesis: for x being Element of ExtREAL ex y being Element of ExtREAL st S1[n,x,y]
let x be Element of ExtREAL ; :: thesis: ex y being Element of ExtREAL st S1[n,x,y]
reconsider m = x / 2 as Element of ExtREAL by XXREAL_0:def 1;
take m ; :: thesis: S1[n,x,m]
thus S1[n,x,m] ; :: thesis: verum
end;
consider F being Function of NAT ,ExtREAL such that
A4: ( F . 0 = x & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A3);
 take F ; :: thesis: ( ( for n being Element of NAT holds 0. < F . n ) & SUM F < eps )
defpred S2[ Element of NAT ] means 0. < F . $1;
A5: S2[ 0 ] by A2, A4;
A6: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 1] )
assume A7: 0. < F . k ; :: thesis: S2[k + 1]
F . (k + 1) = (F . k) / 2 by A4;
hence S2[k + 1] by A7; :: thesis: verum
end;
thus A8: for n being Element of NAT holds S2[n] from NAT_1:sch 1(A5, A6); :: thesis: SUM F < eps
then for n being Element of NAT holds 0. <= F . n ;
then A9: F is nonnegative by SUPINF_2:58;
for s being ext-real number st s in rng (Ser F) holds
s <= x0
proof
let s be ext-real number ; :: thesis: ( s in rng (Ser F) implies s <= x0 )
assume s in rng (Ser F) ; :: thesis: s <= x0
then consider n being set such that
A10: ( n in dom (Ser F) & s = (Ser F) . n ) by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A10;
defpred S3[ Element of NAT ] means ((Ser F) . $1) + (F . $1) < x0;
A11: S3[ 0 ] by A2, A4, SUPINF_2:63;
A12: for l being Element of NAT st S3[l] holds
S3[l + 1]
proof
let l be Element of NAT ; :: thesis: ( S3[l] implies S3[l + 1] )
assume A13: ((Ser F) . l) + (F . l) < x0 ; :: thesis: S3[l + 1]
A14: ((Ser F) . (l + 1)) + (F . (l + 1)) = (((Ser F) . l) + (F . (l + 1))) + (F . (l + 1)) by SUPINF_2:63;
B15: F . (l + 1) = (F . l) / 2 by A4;
A17: 0. <= (Ser F) . l by A9, SUPINF_2:59;
A18: ((Ser F) . l) + ((F . (l + 1)) + (F . (l + 1))) <= ((Ser F) . l) + (F . l) by B15, XXREAL_3:117;
0. <= F . (l + 1) by A8;
then (((Ser F) . l) + (F . (l + 1))) + (F . (l + 1)) <= ((Ser F) . l) + (F . l) by A17, A18, XXREAL_3:48;
hence S3[l + 1] by A13, A14, XXREAL_0:2; :: thesis: verum
end;
for k being Element of NAT holds S3[k] from NAT_1:sch 1(A11, A12);
 then A19: ((Ser F) . n) + (F . n) < x0 ;
( 0. <= (Ser F) . n & 0. <= F . n ) by A8, A9, SUPINF_2:59;
hence s <= x0 by A10, A19, XXREAL_3:53; :: thesis: verum
end;
then x0 is UpperBound of rng (Ser F) by XXREAL_2:def 1;
then A20: ( sup (rng (Ser F)) <= x0 & SUM F = sup (rng (Ser F)) ) by XXREAL_2:def 3;
per cases ( SUM F < x0 or SUM F = x0 ) by A20, XXREAL_0:1;
suppose SUM F < x0 ; :: thesis: SUM F < eps
hence SUM F < eps by A1, XXREAL_0:2; :: thesis: verum
end;
suppose SUM F = x0 ; :: thesis: SUM F < eps
hence SUM F < eps by A1; :: thesis: verum
end;
end;