let A be Element of Family_of_Intervals ; :: thesis: ( A is open_interval implies ex F being Open_Interval_Covering of A st
( F . 0 = A & ( for n being Nat st n <> 0 holds
F . n = {} ) & union (rng F) = A & SUM (F vol) = diameter A ) )
assume A1: A is open_interval ; :: thesis: ex F being Open_Interval_Covering of A st
( F . 0 = A & ( for n being Nat st n <> 0 holds
F . n = {} ) & union (rng F) = A & SUM (F vol) = diameter A )
defpred S1[ Nat, set ] means ( ( $1 = 0 implies $2 = A ) & ( $1 <> 0 implies $2 = {} REAL ) );
A2: for n being Element of NAT ex E being Element of bool REAL st S1[n,E]
proof
let n be Element of NAT ; :: thesis: ex E being Element of bool REAL st S1[n,E]
per cases ( n = 0 or n <> 0 ) ;
suppose A3: n = 0 ; :: thesis: ex E being Element of bool REAL st S1[n,E]
take E = A; :: thesis: S1[n,E]
thus S1[n,E] by A3; :: thesis: verum
end;
suppose A4: n <> 0 ; :: thesis: ex E being Element of bool REAL st S1[n,E]
take E = {} REAL; :: thesis: S1[n,E]
thus S1[n,E] by A4; :: thesis: verum
end;
end;
end;
consider F being Function of NAT,(bool REAL) such that
A5: for n being Element of NAT holds S1[n,F . n] from FUNCT_2:sch 3(A2);
 reconsider F = F as sequence of (bool REAL) ;
0 in NAT ;
then ( 0 in dom F & F . 0 = A ) by A5, FUNCT_2:def 1;
then A in rng F by FUNCT_1:def 3;
then A6: A c= union (rng F) by ZFMISC_1:74;
now :: thesis: for z being object st z in union (rng F) holds
z in A
let z be object ; :: thesis: ( z in union (rng F) implies z in A )
assume z in union (rng F) ; :: thesis: z in A
then consider Y being set such that
A7: ( z in Y & Y in rng F ) by TARSKI:def 4;
ex n being object st
( n in dom F & Y = F . n ) by A7, FUNCT_1:def 3;
hence z in A by A7, A5; :: thesis: verum
end;
then A8: union (rng F) c= A ;
A9: for n being Element of NAT holds F . n is open_interval by A1, A5;
reconsider F = F as Open_Interval_Covering of A by A6, A9, Th32;
take F ; :: thesis: ( F . 0 = A & ( for n being Nat st n <> 0 holds
F . n = {} ) & union (rng F) = A & SUM (F vol) = diameter A )
thus F . 0 = A by A5; :: thesis: ( ( for n being Nat st n <> 0 holds
F . n = {} ) & union (rng F) = A & SUM (F vol) = diameter A )
thus for n being Nat st n <> 0 holds
F . n = {} :: thesis: ( union (rng F) = A & SUM (F vol) = diameter A )
proof
let n be Nat; :: thesis: ( n <> 0 implies F . n = {} )
assume A10: n <> 0 ; :: thesis: F . n = {}
n is Element of NAT by ORDINAL1:def 12;
hence F . n = {} by A5, A10; :: thesis: verum
end;
thus union (rng F) = A by A8, A6, XBOOLE_0:def 10; :: thesis: SUM (F vol) = diameter A
for n being object holds 0 <= (F vol) . n
proof
let n be object ; :: thesis: 0 <= (F vol) . n
per cases ( n in NAT or not n in NAT ) ;
suppose n in NAT ; :: thesis: 0 <= (F vol) . n
then reconsider n1 = n as Element of NAT ;
(F vol) . n = diameter (F . n1) by MEASURE7:def 4;
hence 0 <= (F vol) . n by MEASURE5:13; :: thesis: verum
end;
end;
end;
then A11: F vol is nonnegative by SUPINF_2:51;
defpred S2[ Nat] means (Partial_Sums (F vol)) . $1 = diameter A;
(Partial_Sums (F vol)) . 0 = (F vol) . 0 by MESFUNC9:def 1;
then (Partial_Sums (F vol)) . 0 = diameter (F . 0) by MEASURE7:def 4;
then A12: S2[ 0 ] by A5;
A13: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A14: S2[n] ; :: thesis: S2[n + 1]
A15: (Partial_Sums (F vol)) . (n + 1) = ((Partial_Sums (F vol)) . n) + ((F vol) . (n + 1)) by MESFUNC9:def 1;
(F vol) . (n + 1) = diameter (F . (n + 1)) by MEASURE7:def 4;
then (F vol) . (n + 1) = diameter {} by A5;
hence S2[n + 1] by A14, A15, XXREAL_3:4, MEASURE5:10; :: thesis: verum
end;
A16: for n being Nat holds S2[n] from NAT_1:sch 2(A12, A13);
 thus SUM (F vol) = diameter A :: thesis: verum
proof
SUM (F vol) = Sum (F vol) by A11, MEASURE8:2;
then A17: SUM (F vol) = lim (Partial_Sums (F vol)) by MESFUNC9:def 3;
per cases ( diameter A = +infty or diameter A <> +infty ) ;
end;
end;