let I be Element of Family_of_Intervals ; :: thesis: ( not I is empty & I is closed_interval implies diameter I <= OS_Meas . I )
assume A1: ( not I is empty & I is closed_interval ) ; :: thesis: diameter I <= OS_Meas . I
then consider a, b being Real such that
A2: I = [.a,b.] by MEASURE5:def 3;
reconsider a1 = a, b1 = b as R_eal by XXREAL_0:def 1;
A3: diameter I = b1 - a1 by A1, A2, XXREAL_1:29, MEASURE5:6;
then A4: diameter I < +infty by XXREAL_0:4;
A5: OS_Meas . I <= diameter I by A1, Th44;
OS_Meas is V115() by MEASURE4:def 1;
then ( -infty < 0 & 0 <= OS_Meas . I ) by SUPINF_2:51;
then A6: OS_Meas . I in REAL by A4, A5, XXREAL_0:14;
then reconsider DI = diameter I, LI = OS_Meas . I as Real by A3;
A7: inf (Svc I) in REAL by A6, MEASURE7:def 10;
Svc2 I c= Svc I by Th30;
then A8: Svc I is non empty Subset of ExtREAL ;
for e being Real st 0 < e holds
DI <= LI + e
proof
let e be Real; :: thesis: ( 0 < e implies DI <= LI + e )
assume A9: 0 < e ; :: thesis: DI <= LI + e
consider x being ExtReal such that
A10: ( x in Svc I & x < (inf (Svc I)) + (e / 2) ) by A7, A8, MEASURE6:5, A9, XREAL_1:215;
consider F being Interval_Covering of I such that
A11: x = vol F by A10, MEASURE7:def 8;
defpred S1[ Element of NAT , object ] means ( ( ( F . $1 = {+infty} or F . $1 = {-infty} ) implies $2 = {} ) & ( F . $1 = {+infty} or F . $1 = {-infty} or $2 = F . $1 ) );
A12: for n being Element of NAT ex A being Element of bool REAL st S1[n,A]
proof
let n be Element of NAT ; :: thesis: ex A being Element of bool REAL st S1[n,A]
per cases ( F . n = {+infty} or F . n = {-infty} or ( not F . n = {+infty} & not F . n = {-infty} ) ) ;
suppose A13: ( F . n = {+infty} or F . n = {-infty} ) ; :: thesis: ex A being Element of bool REAL st S1[n,A]
{} c= REAL ;
then reconsider A = {} as Element of bool REAL ;
take A ; :: thesis: S1[n,A]
thus S1[n,A] by A13; :: thesis: verum
end;
suppose A14: ( not F . n = {+infty} & not F . n = {-infty} ) ; :: thesis: ex A being Element of bool REAL st S1[n,A]
take A = F . n; :: thesis: S1[n,A]
thus S1[n,A] by A14; :: thesis: verum
end;
end;
end;
consider F2 being Function of NAT,(bool REAL) such that
A15: for n being Element of NAT holds S1[n,F2 . n] from FUNCT_2:sch 3(A12);
 reconsider F2 = F2 as sequence of (bool REAL) ;
now :: thesis: for x being object st x in I holds
x in union (rng F2)
let x be object ; :: thesis: ( x in I implies x in union (rng F2) )
assume A16: x in I ; :: thesis: x in union (rng F2)
then reconsider x1 = x as Real ;
I c= union (rng F) by MEASURE7:def 2;
then consider A being set such that
A17: ( x in A & A in rng F ) by A16, TARSKI:def 4;
consider n being Element of NAT such that
A18: A = F . n by A17, FUNCT_2:113;
A19: dom F2 = NAT by FUNCT_2:def 1;
( F . n <> {+infty} & F . n <> {-infty} ) by A17, A18, TARSKI:def 1;
then ( x in F2 . n & F2 . n in rng F2 ) by A15, A17, A18, A19, FUNCT_1:3;
hence x in union (rng F2) by TARSKI:def 4; :: thesis: verum
end;
then A20: I c= union (rng F2) ;
now :: thesis: for n being Element of NAT holds F2 . n is Interval
let n be Element of NAT ; :: thesis: F2 . b1 is Interval
per cases ( F . n = {+infty} or F . n = {-infty} or ( not F . n = {+infty} & not F . n = {-infty} ) ) ;
suppose ( F . n = {+infty} or F . n = {-infty} ) ; :: thesis: F2 . b1 is Interval
hence F2 . n is Interval by A15; :: thesis: verum
end;
suppose ( not F . n = {+infty} & not F . n = {-infty} ) ; :: thesis: F2 . b1 is Interval
hence F2 . n is Interval by A15; :: thesis: verum
end;
end;
end;
then reconsider F2 = F2 as Interval_Covering of I by A20, MEASURE7:def 2;
A21: for n being Element of NAT holds (F vol) . n = (F2 vol) . n
proof
let n be Element of NAT ; :: thesis: (F vol) . n = (F2 vol) . n
per cases ( F . n = {+infty} or F . n = {-infty} or ( not F . n = {+infty} & not F . n = {-infty} ) ) ;
suppose A22: ( F . n = {+infty} or F . n = {-infty} ) ; :: thesis: (F vol) . n = (F2 vol) . n
then diameter (F . n) = (sup (F . n)) - (inf (F . n)) by MEASURE5:def 6;
then A23: diameter (F . n) = (sup (F . n)) + (- (inf (F . n))) by XXREAL_3:def 4;
( F . n = [.+infty,+infty.] or F . n = [.-infty,-infty.] ) by A22, XXREAL_1:17;
then ( ( sup (F . n) = +infty & inf (F . n) = +infty ) or ( sup (F . n) = -infty & inf (F . n) = -infty ) ) by XXREAL_2:25, XXREAL_2:29;
then A24: (F vol) . n = 0 by A23, XXREAL_3:6, MEASURE7:def 4;
F2 . n = {} by A22, A15;
then diameter (F2 . n) = 0 by MEASURE5:def 6;
hence (F vol) . n = (F2 vol) . n by A24, MEASURE7:def 4; :: thesis: verum
end;
suppose ( not F . n = {+infty} & not F . n = {-infty} ) ; :: thesis: (F vol) . n = (F2 vol) . n
then F2 . n = F . n by A15;
then (F2 vol) . n = diameter (F . n) by MEASURE7:def 4;
hence (F vol) . n = (F2 vol) . n by MEASURE7:def 4; :: thesis: verum
end;
end;
end;
then F vol = F2 vol by FUNCT_2:def 8;
then vol F2 = SUM (F vol) by MEASURE7:def 6;
then A25: x = vol F2 by A11, MEASURE7:def 6;
A26: now :: thesis: for n being Nat holds not diameter (F2 . n) = +infty
assume ex n being Nat st diameter (F2 . n) = +infty ; :: thesis: contradiction
then consider N being Nat such that
A27: diameter (F2 . N) = +infty ;
A28: N is Element of NAT by ORDINAL1:def 12;
then (F2 vol) . N = +infty by A27, MEASURE7:def 4;
then SUM (F2 vol) = +infty by A28, SUPINF_2:45, MEASURE7:12;
then vol F2 = +infty by MEASURE7:def 6;
hence contradiction by A10, A25, XXREAL_0:3; :: thesis: verum
end;
A29: for n being Element of NAT holds
( F2 . n <> {+infty} & F2 . n <> {-infty} )
proof
let n be Element of NAT ; :: thesis: ( F2 . n <> {+infty} & F2 . n <> {-infty} )
now :: thesis: ( not F2 . n = {+infty} & not F2 . n = {-infty} )
assume A30: ( F2 . n = {+infty} or F2 . n = {-infty} ) ; :: thesis: contradiction
per cases ( F . n = {+infty} or F . n = {-infty} or ( not F . n = {+infty} & not F . n = {-infty} ) ) ;
end;
end;
hence ( F2 . n <> {+infty} & F2 . n <> {-infty} ) ; :: thesis: verum
end;
defpred S2[ Element of NAT , object ] means ( ( F2 . $1 <> {} implies $2 = ].((inf (F2 . $1)) - (e / (2 |^ ($1 + 3)))),((sup (F2 . $1)) + (e / (2 |^ ($1 + 3)))).[ ) & ( F2 . $1 = {} implies $2 = ].(- (e / (2 |^ ($1 + 3)))),(e / (2 |^ ($1 + 3))).[ ) );
A31: for n being Element of NAT ex A being Element of bool REAL st S2[n,A]
proof
let n be Element of NAT ; :: thesis: ex A being Element of bool REAL st S2[n,A]
per cases ( F2 . n <> {} or F2 . n = {} ) ;
suppose A32: F2 . n <> {} ; :: thesis: ex A being Element of bool REAL st S2[n,A]
reconsider A = ].((inf (F2 . n)) - (e / (2 |^ (n + 3)))),((sup (F2 . n)) + (e / (2 |^ (n + 3)))).[ as Subset of REAL ;
take A ; :: thesis: S2[n,A]
thus S2[n,A] by A32; :: thesis: verum
end;
suppose A33: F2 . n = {} ; :: thesis: ex A being Element of bool REAL st S2[n,A]
reconsider A = ].(- (e / (2 |^ (n + 3)))),(e / (2 |^ (n + 3))).[ as Subset of REAL ;
take A ; :: thesis: S2[n,A]
thus S2[n,A] by A33; :: thesis: verum
end;
end;
end;
consider FF being Function of NAT,(bool REAL) such that
A34: for n being Element of NAT holds S2[n,FF . n] from FUNCT_2:sch 3(A31);
 A35: for n being Element of NAT holds F2 . n c= FF . n
proof
let n be Element of NAT ; :: thesis: F2 . n c= FF . n
now :: thesis: for x being ExtReal st x in F2 . n holds
x in FF . n
let x be ExtReal; :: thesis: ( x in F2 . n implies b1 in FF . n )
assume A36: x in F2 . n ; :: thesis: b1 in FF . n
then A37: diameter (F2 . n) = (sup (F2 . n)) - (inf (F2 . n)) by MEASURE5:def 6;
A38: now :: thesis: not inf (F2 . n) = -infty
assume A39: inf (F2 . n) = -infty ; :: thesis: contradiction
sup (F2 . n) <> -infty by A39, XXREAL_2:70, A29;
hence contradiction by A26, A37, A39, XXREAL_3:14; :: thesis: verum
end;
A40: now :: thesis: not sup (F2 . n) = +infty
assume A41: sup (F2 . n) = +infty ; :: thesis: contradiction
inf (F2 . n) <> +infty by A41, XXREAL_2:70, A29;
then diameter (F2 . n) = +infty by A37, A41, XXREAL_3:13;
hence contradiction by A26; :: thesis: verum
end;
reconsider ee = e / (2 |^ (n + 3)) as R_eal by XXREAL_0:def 1;
A42: 2 |^ (n + 3) > 0 by NEWTON:83;
per cases ( F2 . n is open_interval or F2 . n is left_open_interval or F2 . n is right_open_interval or F2 . n is closed_interval ) by MEASURE5:1;
suppose F2 . n is open_interval ; :: thesis: b1 in FF . n
then consider p, q being R_eal such that
A43: F2 . n = ].p,q.[ by MEASURE5:def 2;
F2 . n = ].(inf (F2 . n)),(sup (F2 . n)).[ by A36, A43, XXREAL_2:78;
then A44: ( inf (F2 . n) < x & x < sup (F2 . n) ) by A36, XXREAL_1:4;
then ( inf (F2 . n) <> +infty & sup (F2 . n) <> -infty ) by XXREAL_0:3, XXREAL_0:5;
then ( inf (F2 . n) in REAL & sup (F2 . n) in REAL ) by A38, A40, XXREAL_0:14;
then reconsider p1 = inf (F2 . n), q1 = sup (F2 . n) as Real ;
( p1 - (e / (2 |^ (n + 3))) < p1 & q1 < q1 + (e / (2 |^ (n + 3))) ) by A42, A9, XREAL_1:139, XREAL_1:29, XREAL_1:44;
then ( (inf (F2 . n)) - ee < inf (F2 . n) & sup (F2 . n) < (sup (F2 . n)) + ee ) by Lm9, XXREAL_3:def 2;
then ( (inf (F2 . n)) - (e / (2 |^ (n + 3))) < x & x < (sup (F2 . n)) + (e / (2 |^ (n + 3))) ) by A44, XXREAL_0:2;
then x in ].((inf (F2 . n)) - (e / (2 |^ (n + 3)))),((sup (F2 . n)) + (e / (2 |^ (n + 3)))).[ by XXREAL_1:4;
hence x in FF . n by A34, A36; :: thesis: verum
end;
suppose F2 . n is left_open_interval ; :: thesis: b1 in FF . n
then consider p being R_eal, q being Real such that
A45: F2 . n = ].p,q.] by MEASURE5:def 5;
( p < x & x <= q ) by A36, A45, XXREAL_1:2;
then p < q by XXREAL_0:2;
then F2 . n is right_end by A45, XXREAL_2:35;
then F2 . n = ].(inf (F2 . n)),(sup (F2 . n)).] by A45, XXREAL_2:76;
then A46: ( inf (F2 . n) < x & x <= sup (F2 . n) ) by A36, XXREAL_1:2;
then inf (F2 . n) < sup (F2 . n) by XXREAL_0:2;
then ( inf (F2 . n) <> +infty & sup (F2 . n) <> -infty ) by XXREAL_0:3, XXREAL_0:5;
then ( inf (F2 . n) in REAL & sup (F2 . n) in REAL ) by A38, A40, XXREAL_0:14;
then reconsider p1 = inf (F2 . n), q1 = sup (F2 . n) as Real ;
( p1 - (e / (2 |^ (n + 3))) < p1 & q1 < q1 + (e / (2 |^ (n + 3))) ) by A42, A9, XREAL_1:139, XREAL_1:29, XREAL_1:44;
then ( (inf (F2 . n)) - ee < inf (F2 . n) & sup (F2 . n) < (sup (F2 . n)) + ee ) by Lm9, XXREAL_3:def 2;
then ( (inf (F2 . n)) - (e / (2 |^ (n + 3))) < x & x < (sup (F2 . n)) + (e / (2 |^ (n + 3))) ) by A46, XXREAL_0:2;
then x in ].((inf (F2 . n)) - (e / (2 |^ (n + 3)))),((sup (F2 . n)) + (e / (2 |^ (n + 3)))).[ by XXREAL_1:4;
hence x in FF . n by A34, A36; :: thesis: verum
end;
suppose F2 . n is right_open_interval ; :: thesis: b1 in FF . n
then consider p being Real, q being R_eal such that
A47: F2 . n = [.p,q.[ by MEASURE5:def 4;
( p <= x & x < q ) by A36, A47, XXREAL_1:3;
then p < q by XXREAL_0:2;
then F2 . n is left_end by A47, XXREAL_2:34;
then F2 . n = [.(inf (F2 . n)),(sup (F2 . n)).[ by A47, XXREAL_2:77;
then A48: ( inf (F2 . n) <= x & x < sup (F2 . n) ) by A36, XXREAL_1:3;
then inf (F2 . n) < sup (F2 . n) by XXREAL_0:2;
then ( inf (F2 . n) <> +infty & sup (F2 . n) <> -infty ) by XXREAL_0:3, XXREAL_0:5;
then ( inf (F2 . n) in REAL & sup (F2 . n) in REAL ) by A38, A40, XXREAL_0:14;
then reconsider p1 = inf (F2 . n), q1 = sup (F2 . n) as Real ;
( p1 - (e / (2 |^ (n + 3))) < p1 & q1 < q1 + (e / (2 |^ (n + 3))) ) by A42, A9, XREAL_1:139, XREAL_1:29, XREAL_1:44;
then ( (inf (F2 . n)) - ee < inf (F2 . n) & sup (F2 . n) < (sup (F2 . n)) + ee ) by Lm9, XXREAL_3:def 2;
then ( (inf (F2 . n)) - (e / (2 |^ (n + 3))) < x & x < (sup (F2 . n)) + (e / (2 |^ (n + 3))) ) by A48, XXREAL_0:2;
then x in ].((inf (F2 . n)) - (e / (2 |^ (n + 3)))),((sup (F2 . n)) + (e / (2 |^ (n + 3)))).[ by XXREAL_1:4;
hence x in FF . n by A34, A36; :: thesis: verum
end;
suppose F2 . n is closed_interval ; :: thesis: b1 in FF . n
then consider p, q being Real such that
A49: F2 . n = [.p,q.] by MEASURE5:def 3;
( p <= x & x <= q ) by A36, A49, XXREAL_1:1;
then p <= q by XXREAL_0:2;
then ( F2 . n is left_end & F2 . n is right_end ) by A49, XXREAL_2:33;
then F2 . n = [.(inf (F2 . n)),(sup (F2 . n)).] by XXREAL_2:75;
then A50: ( inf (F2 . n) <= x & x <= sup (F2 . n) ) by A36, XXREAL_1:1;
then ( inf (F2 . n) <> +infty & sup (F2 . n) <> -infty ) by A38, A40, XXREAL_0:2, XXREAL_0:4, XXREAL_0:6;
then ( inf (F2 . n) in REAL & sup (F2 . n) in REAL ) by A38, A40, XXREAL_0:14;
then reconsider p1 = inf (F2 . n), q1 = sup (F2 . n) as Real ;
( p1 - (e / (2 |^ (n + 3))) < p1 & q1 < q1 + (e / (2 |^ (n + 3))) ) by A42, A9, XREAL_1:139, XREAL_1:29, XREAL_1:44;
then ( (inf (F2 . n)) - ee < inf (F2 . n) & sup (F2 . n) < (sup (F2 . n)) + ee ) by Lm9, XXREAL_3:def 2;
then ( (inf (F2 . n)) - (e / (2 |^ (n + 3))) < x & x < (sup (F2 . n)) + (e / (2 |^ (n + 3))) ) by A50, XXREAL_0:2;
then x in ].((inf (F2 . n)) - (e / (2 |^ (n + 3)))),((sup (F2 . n)) + (e / (2 |^ (n + 3)))).[ by XXREAL_1:4;
hence x in FF . n by A34, A36; :: thesis: verum
end;
end;
end;
hence F2 . n c= FF . n ; :: thesis: verum
end;
now :: thesis: for x being object st x in I holds
x in union (rng FF)
let x be object ; :: thesis: ( x in I implies x in union (rng FF) )
assume A51: x in I ; :: thesis: x in union (rng FF)
then reconsider x1 = x as ExtReal ;
I c= union (rng F2) by MEASURE7:def 2;
then consider A being set such that
A52: ( x in A & A in rng F2 ) by A51, TARSKI:def 4;
consider n being Element of NAT such that
A53: A = F2 . n by A52, FUNCT_2:113;
A54: F2 . n c= FF . n by A35;
dom FF = NAT by FUNCT_2:def 1;
then FF . n in rng FF by FUNCT_1:3;
hence x in union (rng FF) by A52, A53, A54, TARSKI:def 4; :: thesis: verum
end;
then A55: I c= union (rng FF) ;
A56: for n being Element of NAT holds FF . n is open_interval
proof
let n be Element of NAT ; :: thesis: FF . n is open_interval
per cases ( F2 . n <> {} or F2 . n = {} ) ;
suppose A57: F2 . n <> {} ; :: thesis: FF . n is open_interval
reconsider e1 = e / (2 |^ (n + 3)) as R_eal by XXREAL_0:def 1;
FF . n = ].((inf (F2 . n)) - e1),((sup (F2 . n)) + e1).[ by A57, A34;
hence FF . n is open_interval by MEASURE5:def 2; :: thesis: verum
end;
suppose F2 . n = {} ; :: thesis: FF . n is open_interval
then A58: FF . n = ].(- (e / (2 |^ (n + 3)))),(e / (2 |^ (n + 3))).[ by A34;
reconsider e1 = e / (2 |^ (n + 3)) as R_eal by XXREAL_0:def 1;
FF . n = ].(- e1),e1.[ by A58, XXREAL_3:def 3;
hence FF . n is open_interval by MEASURE5:def 2; :: thesis: verum
end;
end;
end;
for n being Element of NAT holds FF . n is Interval
proof
let n be Element of NAT ; :: thesis: FF . n is Interval
FF . n is open_interval by A56;
hence FF . n is Interval ; :: thesis: verum
end;
then reconsider FF = FF as Interval_Covering of I by A55, MEASURE7:def 2;
reconsider FF = FF as Open_Interval_Covering of I by A56, Def5;
deffunc H1( Nat) -> set = (e / 2) / (2 |^ ($1 + 1));
consider S being Real_Sequence such that
A59: for n being Nat holds S . n = H1(n) from SEQ_1:sch 1();
 rng S c= ExtREAL by NUMBERS:31;
then reconsider SS = S as ExtREAL_sequence by FUNCT_2:6;
S . 0 = (e / 2) / (2 |^ (0 + 1)) by A59;
then A60: S . 0 = (e / 2) / 2 by NEWTON:5;
A61: |.(1 / 2).| < 1 by LIOUVIL1:7;
A62: for n being Nat holds S . (n + 1) = (1 / 2) * (S . n)
proof
let n be Nat; :: thesis: S . (n + 1) = (1 / 2) * (S . n)
A63: ( S . (n + 1) = (e / 2) / (2 |^ ((n + 1) + 1)) & S . n = (e / 2) / (2 |^ (n + 1)) ) by A59;
then S . (n + 1) = (e / 2) / ((2 |^ (n + 1)) * (2 |^ 1)) by NEWTON:8;
then S . (n + 1) = (e / 2) / ((2 |^ (n + 1)) * 2) by NEWTON:5;
then S . (n + 1) = ((e / 2) / (2 |^ (n + 1))) / 2 by XCMPLX_1:78;
hence S . (n + 1) = (1 / 2) * (S . n) by A63; :: thesis: verum
end;
A64: ( S is summable & Sum S = (S . 0) / (1 - (1 / 2)) ) by A61, A62, SERIES_1:25;
A65: Partial_Sums S is convergent by A61, A62, SERIES_1:25, SERIES_1:def 2;
Partial_Sums S = Partial_Sums SS
proof
rng (Partial_Sums S) c= ExtREAL by NUMBERS:31;
then A66: Partial_Sums S is ExtREAL_sequence by FUNCT_2:6;
defpred S3[ Nat] means (Partial_Sums S) . $1 = (Partial_Sums SS) . $1;
(Partial_Sums S) . 0 = SS . 0 by SERIES_1:def 1;
then A67: S3[ 0 ] by MESFUNC9:def 1;
A68: for n being Nat st S3[n] holds
S3[n + 1]
proof
let n be Nat; :: thesis: ( S3[n] implies S3[n + 1] )
assume A69: S3[n] ; :: thesis: S3[n + 1]
(Partial_Sums S) . (n + 1) = ((Partial_Sums S) . n) + (S . (n + 1)) by SERIES_1:def 1;
then (Partial_Sums S) . (n + 1) = ((Partial_Sums SS) . n) + (SS . (n + 1)) by A69, XXREAL_3:def 2;
hence S3[n + 1] by MESFUNC9:def 1; :: thesis: verum
end;
for n being Nat holds S3[n] from NAT_1:sch 2(A67, A68);
 then for n being Element of NAT holds (Partial_Sums S) . n = (Partial_Sums SS) . n ;
hence Partial_Sums S = Partial_Sums SS by A66, FUNCT_2:def 8; :: thesis: verum
end;
then lim (Partial_Sums SS) = lim (Partial_Sums S) by A65, RINFSUP2:14;
then Sum SS = lim (Partial_Sums S) by MESFUNC9:def 3;
then A70: Sum SS = Sum S by SERIES_1:def 3;
for n being object st n in dom SS holds
SS . n >= 0
proof
let n be object ; :: thesis: ( n in dom SS implies SS . n >= 0 )
assume n in dom SS ; :: thesis: SS . n >= 0
then reconsider n1 = n as Nat ;
SS . n = (e / 2) / (2 |^ (n1 + 1)) by A59;
hence SS . n >= 0 by A9; :: thesis: verum
end;
then A71: ( F2 vol is V115() & SS is V115() ) by MEASURE7:12, SUPINF_2:52;
then A72: SUM SS = e / 2 by A64, A60, A70, MEASURE8:2;
for n being Nat holds (FF vol) . n = ((F2 vol) . n) + (SS . n)
proof
let n be Nat; :: thesis: (FF vol) . n = ((F2 vol) . n) + (SS . n)
A73: n is Element of NAT by ORDINAL1:def 12;
then A74: (FF vol) . n = diameter (FF . n) by MEASURE7:def 4;
reconsider e1 = e / (2 |^ (n + 3)) as R_eal by XXREAL_0:def 1;
A75: - e1 = - (e / (2 |^ (n + 3))) by XXREAL_3:def 3;
A76: 2 |^ (n + 3) > 0 by NEWTON:83;
then A77: e / (2 |^ (n + 3)) > 0 by A9, XREAL_1:139;
per cases ( F2 . n = {} or F2 . n <> {} ) ;
suppose A78: F2 . n = {} ; :: thesis: (FF vol) . n = ((F2 vol) . n) + (SS . n)
then FF . n = ].(- e1),e1.[ by A75, A73, A34;
then (FF vol) . n = e1 - (- e1) by A74, A77, MEASURE5:5;
then (FF vol) . n = (e / (2 |^ (n + 3))) - (- (e / (2 |^ (n + 3)))) by A75, Lm9;
then (FF vol) . n = 2 * (e / (2 |^ ((n + 2) + 1))) ;
then (FF vol) . n = 2 * (e / ((2 |^ (n + 2)) * 2)) by NEWTON:6;
then A79: (FF vol) . n = 2 * ((e / (2 |^ (n + 2))) / 2) by XCMPLX_1:78;
diameter (F2 . n) = 0 by A78, MEASURE5:def 6;
then A80: (F2 vol) . n = 0 by A73, MEASURE7:def 4;
SS . n = (e / 2) / (2 |^ (n + 1)) by A59;
then SS . n = e / (2 * (2 |^ (n + 1))) by XCMPLX_1:78;
then SS . n = e / (2 |^ ((n + 1) + 1)) by NEWTON:6;
hence (FF vol) . n = ((F2 vol) . n) + (SS . n) by A79, A80, XXREAL_3:4; :: thesis: verum
end;
suppose A81: F2 . n <> {} ; :: thesis: (FF vol) . n = ((F2 vol) . n) + (SS . n)
then A82: FF . n = ].((inf (F2 . n)) - e1),((sup (F2 . n)) + e1).[ by A73, A34;
A83: inf (F2 . n) <= sup (F2 . n) by A81, XXREAL_2:40;
A84: diameter (F2 . n) = (sup (F2 . n)) - (inf (F2 . n)) by A81, MEASURE5:def 6;
A85: now :: thesis: ( sup (F2 . n) = +infty implies not inf (F2 . n) <> +infty )
assume ( sup (F2 . n) = +infty & inf (F2 . n) <> +infty ) ; :: thesis: contradiction
then diameter (F2 . n) = +infty by A84, XXREAL_3:13;
hence contradiction by A26; :: thesis: verum
end;
then inf (F2 . n) <> -infty by A84, XXREAL_3:14, A26;
then ( -infty < inf (F2 . n) & sup (F2 . n) < +infty ) by A85, A86, XXREAL_0:4, XXREAL_0:6;
then ( inf (F2 . n) in REAL & sup (F2 . n) in REAL ) by A83, XXREAL_0:14;
then reconsider iF = inf (F2 . n), sF = sup (F2 . n) as Real ;
A89: ( (inf (F2 . n)) - e1 = iF - (e / (2 |^ (n + 3))) & (sup (F2 . n)) + e1 = sF + (e / (2 |^ (n + 3))) ) by Lm9, XXREAL_3:def 2;
A90: ( iF - (e / (2 |^ (n + 3))) < iF & sF < sF + (e / (2 |^ (n + 3))) ) by A76, A9, XREAL_1:139, XREAL_1:29, XREAL_1:44;
then iF - (e / (2 |^ (n + 3))) < sF by A83, XXREAL_0:2;
then (inf (F2 . n)) - e1 < (sup (F2 . n)) + e1 by A89, A90, XXREAL_0:2;
then diameter (FF . n) = ((sup (F2 . n)) + e1) - ((inf (F2 . n)) - e1) by A82, MEASURE5:5;
then diameter (FF . n) = (sF + (e / (2 |^ (n + 3)))) - (iF - (e / (2 |^ (n + 3)))) by A89, Lm9;
then diameter (FF . n) = (sF - iF) + (2 * (e / (2 |^ ((n + 2) + 1)))) ;
then diameter (FF . n) = (sF - iF) + (2 * (e / ((2 |^ (n + 2)) * 2))) by NEWTON:6;
then diameter (FF . n) = (sF - iF) + (2 * ((e / (2 |^ (n + 2))) / 2)) by XCMPLX_1:78;
then A91: (FF vol) . n = (sF - iF) + (e / (2 |^ (n + 2))) by A73, MEASURE7:def 4;
SS . n = (e / 2) / (2 |^ (n + 1)) by A59;
then SS . n = e / (2 * (2 |^ (n + 1))) by XCMPLX_1:78;
then A92: SS . n = e / (2 |^ ((n + 1) + 1)) by NEWTON:6;
diameter (F2 . n) = sF - iF by A84, Lm9;
then (F2 vol) . n = sF - iF by A73, MEASURE7:def 4;
hence (FF vol) . n = ((F2 vol) . n) + (SS . n) by A92, A91, XXREAL_3:def 2; :: thesis: verum
end;
end;
end;
then A93: SUM (FF vol) = (SUM (F2 vol)) + (SUM SS) by A71, MEASURE8:3;
( SUM (F vol) = vol F & SUM (FF vol) = vol FF ) by MEASURE7:def 6;
then A94: vol FF = x + (e / 2) by A21, A11, A93, A72, FUNCT_2:def 8;
reconsider I1 = I as Subset of R^1 by TOPMETR:17;
A95: I1 is compact by A2, Th24;
reconsider F1 = rng FF as Subset-Family of R^1 by TOPMETR:17;
I1 c= union (rng FF) by MEASURE7:def 2;
then consider F2 being Subset-Family of R^1 such that
A96: ( F2 c= F1 & F2 is Cover of I1 & ( for C being set st C in F2 holds
C meets I1 ) ) by SETFAM_1:def 11, BORSUK_1:22;
for P being Subset of R^1 st P in F1 holds
P is open
proof
let P be Subset of R^1; :: thesis: ( P in F1 implies P is open )
assume P in F1 ; :: thesis: P is open
then consider n being Element of NAT such that
A97: P = FF . n by FUNCT_2:113;
ex p, q being R_eal st P = ].p,q.[ by A97, MEASURE5:def 2;
hence P is open by BORSUK_5:40; :: thesis: verum
end;
then for P being Subset of R^1 st P in F2 holds
P is open by A96;
then consider G1 being Subset-Family of R^1 such that
A98: ( G1 c= F2 & G1 is Cover of I1 & G1 is finite ) by A95, A96, COMPTS_1:def 4, TOPS_2:def 1;
reconsider G1 = G1 as finite set by A98;
now :: thesis: for A being set st A in rng (canFS G1) holds
A in bool REAL
let A be set ; :: thesis: ( A in rng (canFS G1) implies A in bool REAL )
assume A in rng (canFS G1) ; :: thesis: A in bool REAL
then A in F1 by A96, A98;
hence A in bool REAL ; :: thesis: verum
end;
then rng (canFS G1) c= bool REAL ;
then reconsider GG = canFS G1 as FinSequence of bool REAL by FINSEQ_1:def 4;
I c= union G1 by A98, SETFAM_1:def 11;
then I c= Union GG by ZFMISC_1:2, SRINGS_3:2;
then A99: I c= union (rng GG) by CARD_3:def 4;
deffunc H2( Nat) -> Element of ExtREAL = diameter (GG . $1);
consider G2 being FinSequence of ExtREAL such that
A100: ( len G2 = len GG & ( for n being Nat st n in dom G2 holds
G2 . n = H2(n) ) ) from FINSEQ_2:sch 1();
 A101: dom GG = dom G2 by A100, FINSEQ_3:29;
A102: now :: thesis: for n being Nat holds G2 . n = diameter (GG . n)
let n be Nat; :: thesis: G2 . b1 = diameter (GG . b1)
per cases ( n in dom GG or not n in dom GG ) ;
suppose n in dom GG ; :: thesis: G2 . b1 = diameter (GG . b1)
hence G2 . n = diameter (GG . n) by A100, A101; :: thesis: verum
end;
end;
end;
A104: for n being Nat st n in dom GG holds
I meets GG . n
proof
let n be Nat; :: thesis: ( n in dom GG implies I meets GG . n )
assume n in dom GG ; :: thesis: I meets GG . n
then GG . n in rng (canFS G1) by FUNCT_1:3;
hence I meets GG . n by A96, A98; :: thesis: verum
end;
for n being Nat st n in dom GG holds
GG . n is open_interval Subset of REAL
proof
let n be Nat; :: thesis: ( n in dom GG implies GG . n is open_interval Subset of REAL )
assume n in dom GG ; :: thesis: GG . n is open_interval Subset of REAL
then GG . n in rng (canFS G1) by FUNCT_1:3;
then GG . n in G1 ;
then ex k being Element of NAT st GG . n = FF . k by A96, A98, FUNCT_2:113;
hence GG . n is open_interval Subset of REAL ; :: thesis: verum
end;
then A105: DI <= Sum G2 by A1, A99, A100, A101, A104, Th45;
rng (canFS G1) c= rng FF by A96, A98;
then Sum G2 <= x + (e / 2) by A94, A1, A101, A102, Th56;
then A106: DI <= x + (e / 2) by A105, XXREAL_0:2;
reconsider e2 = e / 2 as ExtReal ;
A107: e / 2 in REAL by XREAL_0:def 1;
A108: ((inf (Svc I)) + (e / 2)) + (e / 2) = (inf (Svc I)) + (e2 + e2) by XXREAL_3:29
.= (inf (Svc I)) + ((e / 2) + (e / 2)) by XXREAL_3:def 2 ;
x + (e / 2) < ((inf (Svc I)) + (e / 2)) + (e / 2) by A107, A10, XXREAL_3:43;
then DI < (inf (Svc I)) + ((e / 2) + (e / 2)) by A108, A106, XXREAL_0:2;
then DI < (OS_Meas . I) + e by MEASURE7:def 10;
hence DI <= LI + e by XXREAL_3:def 2; :: thesis: verum
end;
hence diameter I <= OS_Meas . I by XREAL_1:41; :: thesis: verum