let A be Element of Family_of_Intervals ; ( 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
; 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]
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;
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
; ( 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; ( ( 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 = {}
( union (rng F) = A & SUM (F vol) = diameter A )
thus
union (rng F) = A
by A8, A6, XBOOLE_0:def 10; SUM (F vol) = diameter A
for n being object holds 0 <= (F vol) . n
then A11:
F vol is V115()
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]
A16:
for n being Nat holds S2[n]
from NAT_1:sch 2(A12, A13);
thus
SUM (F vol) = diameter A
verum