defpred S1[ set , set , set ] means for a, b being R_eal
for s being Nat st s = $1 & a = $2 & b = $3 holds
b = a / 2;
let eps be ExtReal; :: thesis: ( 0. < eps implies ex F being sequence of ExtREAL st
( ( for n being Nat holds 0. < F . n ) & SUM F < eps ) )
assume 0. < eps ; :: thesis: ex F being sequence of ExtREAL st
( ( for n being Nat holds 0. < F . n ) & SUM F < eps )
then consider x0 being Real such that
A1: 0. < x0 and
A2: x0 < eps by XXREAL_3:3;
consider x being Real such that
A3: 0. < x and
A4: x + x < x0 by A1, XXREAL_3:50;
reconsider x = x as Element of ExtREAL by XXREAL_0:def 1;
A5: for n being Nat
for x being Element of ExtREAL ex y being Element of ExtREAL st S1[n,x,y]
proof
let n be 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 sequence of ExtREAL such that
A6: ( F . 0 = x & ( for n being Nat holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A5);
 take F ; :: thesis: ( ( for n being Nat holds 0. < F . n ) & SUM F < eps )
defpred S2[ Nat] means 0. < F . $1;
A7: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A8: 0. < F . k ; :: thesis: S2[k + 1]
F . (k + 1) = (F . k) / 2 by A6;
hence S2[k + 1] by A8; :: thesis: verum
end;
A9: S2[ 0 ] by A3, A6;
thus A10: for n being Nat holds S2[n] from NAT_1:sch 2(A9, A7); :: thesis: SUM F < eps
then for n being Element of NAT holds 0. <= F . n ;
then A11: F is nonnegative by SUPINF_2:39;
for s being ExtReal st s in rng (Ser F) holds
s <= x0
proof
defpred S3[ Nat] means ((Ser F) . $1) + (F . $1) < x0;
let s be ExtReal; :: thesis: ( s in rng (Ser F) implies s <= x0 )
assume s in rng (Ser F) ; :: thesis: s <= x0
then consider n being object such that
A12: n in dom (Ser F) and
A13: s = (Ser F) . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A12;
A14: for l being Nat st S3[l] holds
S3[l + 1]
proof
let l be Nat; :: thesis: ( S3[l] implies S3[l + 1] )
F . (l + 1) = (F . l) / 2 by A6;
then A15: ((Ser F) . l) + ((F . (l + 1)) + (F . (l + 1))) <= ((Ser F) . l) + (F . l) by XXREAL_3:105;
( 0. <= (Ser F) . l & 0. <= F . (l + 1) ) by A10, A11, SUPINF_2:40;
then A16: ( ((Ser F) . (l + 1)) + (F . (l + 1)) = (((Ser F) . l) + (F . (l + 1))) + (F . (l + 1)) & (((Ser F) . l) + (F . (l + 1))) + (F . (l + 1)) <= ((Ser F) . l) + (F . l) ) by A15, SUPINF_2:def 11, XXREAL_3:44;
assume ((Ser F) . l) + (F . l) < x0 ; :: thesis: S3[l + 1]
hence S3[l + 1] by A16, XXREAL_0:2; :: thesis: verum
end;
A17: S3[ 0 ] by A4, A6, SUPINF_2:def 11;
for k being Nat holds S3[k] from NAT_1:sch 2(A17, A14);
 then A18: ((Ser F) . n) + (F . n) < x0 ;
( 0. <= (Ser F) . n & 0. <= F . n ) by A10, A11, SUPINF_2:40;
hence s <= x0 by A13, A18, XXREAL_3:48; :: thesis: verum
end;
then x0 is UpperBound of rng (Ser F) by XXREAL_2:def 1;
then A19: sup (rng (Ser F)) <= x0 by XXREAL_2:def 3;
per cases ( SUM F < x0 or SUM F = x0 ) by A19, XXREAL_0:1;
suppose SUM F < x0 ; :: thesis: SUM F < eps
hence SUM F < eps by A2, XXREAL_0:2; :: thesis: verum
end;
suppose SUM F = x0 ; :: thesis: SUM F < eps
hence SUM F < eps by A2; :: thesis: verum
end;
end;