reconsider y = D as Element of Funcs (NAT,(bool REAL)) by FUNCT_2:8;
let H be sequence of [:NAT,NAT:]; :: thesis: ( H is one-to-one & rng H = [:NAT,NAT:] implies for k being Nat ex m being Element of NAT st
for F being sequence of (bool REAL)
for G being Open_Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m )
assume that
A1: H is one-to-one and
A2: rng H = [:NAT,NAT:] ; :: thesis: for k being Nat ex m being Element of NAT st
for F being sequence of (bool REAL)
for G being Open_Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m
defpred S1[ Nat] means ex m being Element of NAT st
for F being sequence of (bool REAL)
for G being Open_Interval_Covering of F holds (Ser ((On (G,H)) vol)) . $1 <= (Ser (vol G)) . m;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
set N0 = { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } ;
A4: { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } c= NAT
proof
let s1 be object ; :: according to TARSKI:def 3 :: thesis: ( not s1 in { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } or s1 in NAT )
assume s1 in { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } ; :: thesis: s1 in NAT
then ex s being Element of NAT st
( s = s1 & (pr1 H) . (k + 1) = (pr1 H) . s ) ;
hence s1 in NAT ; :: thesis: verum
end;
k + 1 in { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } ;
then reconsider N0 = { s where s is Element of NAT : (pr1 H) . (k + 1) = (pr1 H) . s } as non empty Subset of NAT by A4;
given m0 being Element of NAT such that A5: for F being sequence of (bool REAL)
for G being Open_Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m0 ; :: thesis: S1[k + 1]
take m = m0 + ((pr1 H) . (k + 1)); :: thesis: for F being sequence of (bool REAL)
for G being Open_Interval_Covering of F holds (Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . m
let F be sequence of (bool REAL); :: thesis: for G being Open_Interval_Covering of F holds (Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . m
let G be Open_Interval_Covering of F; :: thesis: (Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . m
defpred S2[ Element of NAT , Function] means ( ( $1 <> (pr1 H) . (k + 1) implies for m being Element of NAT holds $2 . m = (G . $1) . m ) & ( $1 = (pr1 H) . (k + 1) implies for m being Element of NAT holds $2 . m = {} ) );
A6: for n being Element of NAT ex y being Element of Funcs (NAT,(bool REAL)) st S2[n,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S2[n,y]
per cases ( n <> (pr1 H) . (k + 1) or n = (pr1 H) . (k + 1) ) ;
suppose A7: n <> (pr1 H) . (k + 1) ; :: thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S2[n,y]
reconsider y = G . n as Element of Funcs (NAT,(bool REAL)) by FUNCT_2:8;
take y ; :: thesis: S2[n,y]
thus S2[n,y] by A7; :: thesis: verum
end;
suppose A8: n = (pr1 H) . (k + 1) ; :: thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S2[n,y]
take y ; :: thesis: S2[n,y]
thus S2[n,y] by A8; :: thesis: verum
end;
end;
end;
consider G1 being sequence of (Funcs (NAT,(bool REAL))) such that
A9: for n being Element of NAT holds S2[n,G1 . n] from FUNCT_2:sch 3(A6);
 A10: for n being Element of NAT holds G1 . n is Open_Interval_Covering of D . n
proof
let n be Element of NAT ; :: thesis: G1 . n is Open_Interval_Covering of D . n
consider f0 being Function such that
A11: G1 . n = f0 and
A12: ( dom f0 = NAT & rng f0 c= bool REAL ) by FUNCT_2:def 2;
reconsider f0 = f0 as sequence of (bool REAL) by A12, FUNCT_2:2;
A13: for s being Element of NAT holds f0 . s is Interval
proof
let s be Element of NAT ; :: thesis: f0 . s is Interval
per cases ( n <> (pr1 H) . (k + 1) or n = (pr1 H) . (k + 1) ) ;
suppose n <> (pr1 H) . (k + 1) ; :: thesis: f0 . s is Interval
then f0 . s = (G . n) . s by A9, A11;
hence f0 . s is Interval ; :: thesis: verum
end;
suppose n = (pr1 H) . (k + 1) ; :: thesis: f0 . s is Interval
hence f0 . s is Interval by A9, A11; :: thesis: verum
end;
end;
end;
D . n c= union (rng f0) ;
then reconsider f0 = f0 as Interval_Covering of D . n by A13, MEASURE7:def 2;
for m being Element of NAT holds f0 . m is open_interval
proof
let m be Element of NAT ; :: thesis: f0 . m is open_interval
per cases ( n <> (pr1 H) . (k + 1) or n = (pr1 H) . (k + 1) ) ;
suppose n <> (pr1 H) . (k + 1) ; :: thesis: f0 . m is open_interval
then f0 . m = (G . n) . m by A9, A11;
hence f0 . m is open_interval ; :: thesis: verum
end;
suppose n = (pr1 H) . (k + 1) ; :: thesis: f0 . m is open_interval
hence f0 . m is open_interval by A9, A11; :: thesis: verum
end;
end;
end;
then reconsider f0 = f0 as Open_Interval_Covering of D . n by Def5;
G1 . n = f0 by A11;
hence G1 . n is Open_Interval_Covering of D . n ; :: thesis: verum
end;
defpred S3[ Element of N0, Element of NAT ] means $2 = (pr2 H) . $1;
defpred S4[ Element of NAT , Function] means ( ( $1 = (pr1 H) . (k + 1) implies for m being Element of NAT holds $2 . m = (G . $1) . m ) & ( $1 <> (pr1 H) . (k + 1) implies for m being Element of NAT holds $2 . m = {} ) );
A14: for n being Element of NAT ex y being Element of Funcs (NAT,(bool REAL)) st S4[n,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S4[n,y]
per cases ( n = (pr1 H) . (k + 1) or n <> (pr1 H) . (k + 1) ) ;
suppose A15: n = (pr1 H) . (k + 1) ; :: thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S4[n,y]
reconsider y = G . n as Element of Funcs (NAT,(bool REAL)) by FUNCT_2:8;
take y ; :: thesis: S4[n,y]
thus S4[n,y] by A15; :: thesis: verum
end;
suppose A16: n <> (pr1 H) . (k + 1) ; :: thesis: ex y being Element of Funcs (NAT,(bool REAL)) st S4[n,y]
take y ; :: thesis: S4[n,y]
thus S4[n,y] by A16; :: thesis: verum
end;
end;
end;
consider G0 being sequence of (Funcs (NAT,(bool REAL))) such that
A17: for n being Element of NAT holds S4[n,G0 . n] from FUNCT_2:sch 3(A14);
 for n being Element of NAT holds G0 . n is Interval_Covering of D . n
proof
let n be Element of NAT ; :: thesis: G0 . n is Interval_Covering of D . n
consider f0 being Function such that
A18: G0 . n = f0 and
A19: ( dom f0 = NAT & rng f0 c= bool REAL ) by FUNCT_2:def 2;
reconsider f0 = f0 as sequence of (bool REAL) by A19, FUNCT_2:2;
A20: for s being Element of NAT holds f0 . s is Interval
proof
let s be Element of NAT ; :: thesis: f0 . s is Interval
per cases ( n = (pr1 H) . (k + 1) or n <> (pr1 H) . (k + 1) ) ;
suppose n = (pr1 H) . (k + 1) ; :: thesis: f0 . s is Interval
then f0 . s = (G . n) . s by A17, A18;
hence f0 . s is Interval ; :: thesis: verum
end;
suppose n <> (pr1 H) . (k + 1) ; :: thesis: f0 . s is Interval
hence f0 . s is Interval by A17, A18; :: thesis: verum
end;
end;
end;
D . n c= union (rng f0) ;
then reconsider f0 = f0 as Interval_Covering of D . n by A20, MEASURE7:def 2;
for s being Element of NAT holds f0 . s is open_interval
proof
let s be Element of NAT ; :: thesis: f0 . s is open_interval
per cases ( n = (pr1 H) . (k + 1) or n <> (pr1 H) . (k + 1) ) ;
suppose n = (pr1 H) . (k + 1) ; :: thesis: f0 . s is open_interval
then f0 . s = (G . n) . s by A17, A18;
hence f0 . s is open_interval ; :: thesis: verum
end;
suppose n <> (pr1 H) . (k + 1) ; :: thesis: f0 . s is open_interval
hence f0 . s is open_interval by A17, A18; :: thesis: verum
end;
end;
end;
then reconsider f0 = f0 as Open_Interval_Covering of D . n by Def5;
G0 . n = f0 by A18;
hence G0 . n is Interval_Covering of D . n ; :: thesis: verum
end;
then reconsider G0 = G0 as Interval_Covering of D by MEASURE7:def 3;
for n being Element of NAT holds G0 . n is Open_Interval_Covering of D . n
proof
let n be Element of NAT ; :: thesis: G0 . n is Open_Interval_Covering of D . n
per cases ( n = (pr1 H) . (k + 1) or n <> (pr1 H) . (k + 1) ) ;
suppose A21: n = (pr1 H) . (k + 1) ; :: thesis: G0 . n is Open_Interval_Covering of D . n
for m being Element of NAT holds (G0 . n) . m is open_interval
proof
let m be Element of NAT ; :: thesis: (G0 . n) . m is open_interval
(G0 . n) . m = (G . n) . m by A21, A17;
hence (G0 . n) . m is open_interval ; :: thesis: verum
end;
hence G0 . n is Open_Interval_Covering of D . n by Def5; :: thesis: verum
end;
suppose n <> (pr1 H) . (k + 1) ; :: thesis: G0 . n is Open_Interval_Covering of D . n
then for m being Element of NAT holds (G0 . n) . m is open_interval by A17;
hence G0 . n is Open_Interval_Covering of D . n by Def5; :: thesis: verum
end;
end;
end;
then reconsider G0 = G0 as Open_Interval_Covering of D by Def6;
set GG0 = On (G0,H);
reconsider G1 = G1 as Open_Interval_Covering of D by A10, Th33;
set GG1 = On (G1,H);
A22: (Ser ((On (G0,H)) vol)) . (k + 1) <= SUM ((On (G0,H)) vol) by MEASURE7:6, MEASURE7:12;
(On (G1,H)) . (k + 1) = (G1 . ((pr1 H) . (k + 1))) . ((pr2 H) . (k + 1)) by A2, MEASURE7:def 11
.= {} by A9 ;
then A23: ((On (G1,H)) vol) . (k + 1) = 0. by MEASURE7:def 4, MEASURE5:10;
(Ser ((On (G1,H)) vol)) . (k + 1) = ((Ser ((On (G1,H)) vol)) . k) + (((On (G1,H)) vol) . (k + 1)) by SUPINF_2:def 11;
then A24: (Ser ((On (G1,H)) vol)) . (k + 1) = (Ser ((On (G1,H)) vol)) . k by A23, XXREAL_3:4;
for s being Element of NAT holds 0. <= (vol G1) . s by MEASURE7:13;
then vol G1 is nonnegative by SUPINF_2:39;
then A25: (Ser (vol G1)) . m0 <= (Ser (vol G1)) . m by SUPINF_2:41;
A26: for n being Element of NAT holds ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n)
proof
let n be Element of NAT ; :: thesis: ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n)
A27: ( ((On (G0,H)) vol) . n = diameter ((On (G0,H)) . n) & ((On (G1,H)) vol) . n = diameter ((On (G1,H)) . n) ) by MEASURE7:def 4;
((On (G,H)) vol) . n = diameter ((On (G,H)) . n) by MEASURE7:def 4;
then A28: ((On (G,H)) vol) . n = diameter ((G . ((pr1 H) . n)) . ((pr2 H) . n)) by A2, MEASURE7:def 11;
per cases ( (pr1 H) . n = (pr1 H) . (k + 1) or (pr1 H) . n <> (pr1 H) . (k + 1) ) ;
suppose A29: (pr1 H) . n = (pr1 H) . (k + 1) ; :: thesis: ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n)
A30: (On (G1,H)) . n = (G1 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, MEASURE7:def 11
.= {} by A9, A29 ;
(On (G0,H)) . n = (G0 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, MEASURE7:def 11
.= (G . ((pr1 H) . n)) . ((pr2 H) . n) by A17, A29 ;
hence ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n) by A27, A28, A30, MEASURE5:10, XXREAL_3:4; :: thesis: verum
end;
suppose A31: (pr1 H) . n <> (pr1 H) . (k + 1) ; :: thesis: ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n)
A32: (On (G0,H)) . n = (G0 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, MEASURE7:def 11
.= {} by A17, A31 ;
(On (G1,H)) . n = (G1 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, MEASURE7:def 11
.= (G . ((pr1 H) . n)) . ((pr2 H) . n) by A9, A31 ;
hence ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n) by A27, A28, A32, MEASURE5:10, XXREAL_3:4; :: thesis: verum
end;
end;
end;
( (On (G0,H)) vol is nonnegative & (On (G1,H)) vol is nonnegative ) by MEASURE7:12;
then A33: (Ser ((On (G,H)) vol)) . (k + 1) = ((Ser ((On (G0,H)) vol)) . (k + 1)) + ((Ser ((On (G1,H)) vol)) . (k + 1)) by A26, MEASURE7:3;
for s being Element of NAT holds 0. <= (vol G1) . s by MEASURE7:13;
then A34: vol G1 is nonnegative by SUPINF_2:39;
(Ser ((On (G1,H)) vol)) . k <= (Ser (vol G1)) . m0 by A5;
then A35: (Ser ((On (G1,H)) vol)) . (k + 1) <= (Ser (vol G1)) . m by A24, A25, XXREAL_0:2;
A36: for s being Element of N0 ex y being Element of NAT st S3[s,y] ;
consider SOS being Function of N0,NAT such that
A37: for s being Element of N0 holds S3[s,SOS . s] from FUNCT_2:sch 3(A36);
 A38: for n being Element of NAT holds (vol G) . n = ((vol G0) . n) + ((vol G1) . n)
proof
let n be Element of NAT ; :: thesis: (vol G) . n = ((vol G0) . n) + ((vol G1) . n)
A39: vol (G . n) = (vol (G0 . n)) + (vol (G1 . n))
proof
per cases ( n = (pr1 H) . (k + 1) or n <> (pr1 H) . (k + 1) ) ;
suppose A40: n = (pr1 H) . (k + 1) ; :: thesis: vol (G . n) = (vol (G0 . n)) + (vol (G1 . n))
for s being Element of NAT holds ((G . n) vol) . s <= ((G0 . n) vol) . s
proof
let s be Element of NAT ; :: thesis: ((G . n) vol) . s <= ((G0 . n) vol) . s
((G0 . n) vol) . s = diameter ((G0 . n) . s) by MEASURE7:def 4
.= diameter ((G . n) . s) by A17, A40
.= ((G . n) vol) . s by MEASURE7:def 4 ;
hence ((G . n) vol) . s <= ((G0 . n) vol) . s ; :: thesis: verum
end;
then A41: SUM ((G . n) vol) <= SUM ((G0 . n) vol) by SUPINF_2:43;
for s being Element of NAT holds ((G1 . n) vol) . s = 0.
proof
let s be Element of NAT ; :: thesis: ((G1 . n) vol) . s = 0.
diameter ((G1 . n) . s) = 0. by A9, A40, MEASURE5:10;
hence ((G1 . n) vol) . s = 0. by MEASURE7:def 4; :: thesis: verum
end;
then A42: SUM ((G1 . n) vol) = 0. by MEASURE7:1;
for s being Element of NAT holds ((G0 . n) vol) . s <= ((G . n) vol) . s
proof
let s be Element of NAT ; :: thesis: ((G0 . n) vol) . s <= ((G . n) vol) . s
((G0 . n) vol) . s = diameter ((G0 . n) . s) by MEASURE7:def 4
.= diameter ((G . n) . s) by A17, A40
.= ((G . n) vol) . s by MEASURE7:def 4 ;
hence ((G0 . n) vol) . s <= ((G . n) vol) . s ; :: thesis: verum
end;
then SUM ((G0 . n) vol) <= SUM ((G . n) vol) by SUPINF_2:43;
then SUM ((G . n) vol) = SUM ((G0 . n) vol) by A41, XXREAL_0:1;
then vol (G . n) = SUM ((G0 . n) vol) by MEASURE7:def 6;
then vol (G . n) = vol (G0 . n) by MEASURE7:def 6;
then vol (G . n) = (vol (G0 . n)) + (SUM ((G1 . n) vol)) by A42, XXREAL_3:4;
hence vol (G . n) = (vol (G0 . n)) + (vol (G1 . n)) by MEASURE7:def 6; :: thesis: verum
end;
suppose A43: n <> (pr1 H) . (k + 1) ; :: thesis: vol (G . n) = (vol (G0 . n)) + (vol (G1 . n))
A44: for s being Element of NAT holds ((G1 . n) vol) . s = ((G . n) vol) . s
proof
let s be Element of NAT ; :: thesis: ((G1 . n) vol) . s = ((G . n) vol) . s
( ((G1 . n) vol) . s = diameter ((G1 . n) . s) & ((G . n) vol) . s = diameter ((G . n) . s) ) by MEASURE7:def 4;
hence ((G1 . n) vol) . s = ((G . n) vol) . s by A9, A43; :: thesis: verum
end;
then for s being Element of NAT holds ((G . n) vol) . s <= ((G1 . n) vol) . s ;
then A45: SUM ((G . n) vol) <= SUM ((G1 . n) vol) by SUPINF_2:43;
for s being Element of NAT holds ((G0 . n) vol) . s = 0.
proof
let s be Element of NAT ; :: thesis: ((G0 . n) vol) . s = 0.
diameter ((G0 . n) . s) = 0. by A17, A43, MEASURE5:10;
hence ((G0 . n) vol) . s = 0. by MEASURE7:def 4; :: thesis: verum
end;
then A46: SUM ((G0 . n) vol) = 0. by MEASURE7:1;
for s being Element of NAT holds ((G1 . n) vol) . s <= ((G . n) vol) . s by A44;
then SUM ((G1 . n) vol) <= SUM ((G . n) vol) by SUPINF_2:43;
then SUM ((G . n) vol) = SUM ((G1 . n) vol) by A45, XXREAL_0:1;
then vol (G . n) = SUM ((G1 . n) vol) by MEASURE7:def 6;
then vol (G . n) = vol (G1 . n) by MEASURE7:def 6;
then vol (G . n) = (SUM ((G0 . n) vol)) + (vol (G1 . n)) by A46, XXREAL_3:4;
hence vol (G . n) = (vol (G0 . n)) + (vol (G1 . n)) by MEASURE7:def 6; :: thesis: verum
end;
end;
end;
( (vol G) . n = vol (G . n) & (vol G0) . n = vol (G0 . n) ) by MEASURE7:def 7;
hence (vol G) . n = ((vol G0) . n) + ((vol G1) . n) by A39, MEASURE7:def 7; :: thesis: verum
end;
for s being Element of NAT holds 0. <= (vol G0) . s by MEASURE7:13;
then vol G0 is nonnegative by SUPINF_2:39;
then A47: ( (vol G0) . ((pr1 H) . (k + 1)) <= (Ser (vol G0)) . ((pr1 H) . (k + 1)) & (Ser (vol G0)) . ((pr1 H) . (k + 1)) <= (Ser (vol G0)) . m ) by MEASURE7:2, SUPINF_2:41;
A48: for s being Element of NAT holds
( ( s in N0 implies ((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s ) & ( not s in N0 implies ((On (G0,H)) vol) . s = 0. ) )
proof
let s be Element of NAT ; :: thesis: ( ( s in N0 implies ((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s ) & ( not s in N0 implies ((On (G0,H)) vol) . s = 0. ) )
thus ( s in N0 implies ((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s ) :: thesis: ( not s in N0 implies ((On (G0,H)) vol) . s = 0. )
proof
assume A49: s in N0 ; :: thesis: ((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s
then A50: ex s1 being Element of NAT st
( s1 = s & (pr1 H) . (k + 1) = (pr1 H) . s1 ) ;
A51: (pr2 H) . s = SOS . s by A37, A49;
((On (G0,H)) vol) . s = diameter ((On (G0,H)) . s) by MEASURE7:def 4
.= diameter ((G0 . ((pr1 H) . (k + 1))) . ((pr2 H) . s)) by A2, A50, MEASURE7:def 11
.= ((G0 . ((pr1 H) . (k + 1))) vol) . (SOS . s) by A51, MEASURE7:def 4
.= (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s by A49, FUNCT_2:15 ;
hence ((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s ; :: thesis: verum
end;
assume not s in N0 ; :: thesis: ((On (G0,H)) vol) . s = 0.
then A52: not (pr1 H) . (k + 1) = (pr1 H) . s ;
((On (G0,H)) vol) . s = diameter ((On (G0,H)) . s) by MEASURE7:def 4
.= diameter ((G0 . ((pr1 H) . s)) . ((pr2 H) . s)) by A2, MEASURE7:def 11
.= 0. by A17, A52, MEASURE5:10 ;
hence ((On (G0,H)) vol) . s = 0. ; :: thesis: verum
end;
for s1, s2 being object st s1 in N0 & s2 in N0 & SOS . s1 = SOS . s2 holds
s1 = s2
proof
let s1, s2 be object ; :: thesis: ( s1 in N0 & s2 in N0 & SOS . s1 = SOS . s2 implies s1 = s2 )
assume that
A53: ( s1 in N0 & s2 in N0 ) and
A54: SOS . s1 = SOS . s2 ; :: thesis: s1 = s2
reconsider s1 = s1, s2 = s2 as Element of NAT by A53;
A55: ( ex s11 being Element of NAT st
( s11 = s1 & (pr1 H) . (k + 1) = (pr1 H) . s11 ) & ex s22 being Element of NAT st
( s22 = s2 & (pr1 H) . (k + 1) = (pr1 H) . s22 ) ) by A53;
A56: ( H . s1 = [((pr1 H) . s1),((pr2 H) . s1)] & H . s2 = [((pr1 H) . s2),((pr2 H) . s2)] ) by FUNCT_2:119;
( SOS . s1 = (pr2 H) . s1 & SOS . s2 = (pr2 H) . s2 ) by A37, A53;
hence s1 = s2 by A1, A54, A55, A56, FUNCT_2:19; :: thesis: verum
end;
then SOS is one-to-one by FUNCT_2:19;
then SUM ((On (G0,H)) vol) <= SUM ((G0 . ((pr1 H) . (k + 1))) vol) by A48, MEASURE7:11, MEASURE7:12;
then A57: (Ser ((On (G0,H)) vol)) . (k + 1) <= SUM ((G0 . ((pr1 H) . (k + 1))) vol) by A22, XXREAL_0:2;
SUM ((G0 . ((pr1 H) . (k + 1))) vol) = vol (G0 . ((pr1 H) . (k + 1))) by MEASURE7:def 6
.= (vol G0) . ((pr1 H) . (k + 1)) by MEASURE7:def 7 ;
then SUM ((G0 . ((pr1 H) . (k + 1))) vol) <= (Ser (vol G0)) . m by A47, XXREAL_0:2;
then A58: (Ser ((On (G0,H)) vol)) . (k + 1) <= (Ser (vol G0)) . m by A57, XXREAL_0:2;
for s being Element of NAT holds 0. <= (vol G0) . s by MEASURE7:13;
then vol G0 is nonnegative by SUPINF_2:39;
then (Ser (vol G)) . m = ((Ser (vol G0)) . m) + ((Ser (vol G1)) . m) by A38, A34, MEASURE7:3;
hence (Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . m by A58, A35, A33, XXREAL_3:36; :: thesis: verum
end;
A59: S1[ 0 ]
proof
take m = (pr1 H) . 0; :: thesis: for F being sequence of (bool REAL)
for G being Open_Interval_Covering of F holds (Ser ((On (G,H)) vol)) . 0 <= (Ser (vol G)) . m
let F be sequence of (bool REAL); :: thesis: for G being Open_Interval_Covering of F holds (Ser ((On (G,H)) vol)) . 0 <= (Ser (vol G)) . m
let G be Open_Interval_Covering of F; :: thesis: (Ser ((On (G,H)) vol)) . 0 <= (Ser (vol G)) . m
reconsider GG = On (G,H) as Open_Interval_Covering of union (rng F) by A2, Th31;
( (GG vol) . 0 = diameter (GG . 0) & ((G . ((pr1 H) . 0)) vol) . ((pr2 H) . 0) = diameter ((G . ((pr1 H) . 0)) . ((pr2 H) . 0)) ) by MEASURE7:def 4;
then (GG vol) . 0 <= ((G . ((pr1 H) . 0)) vol) . ((pr2 H) . 0) by A2, MEASURE7:def 11;
then (GG vol) . 0 <= SUM ((G . ((pr1 H) . 0)) vol) by MEASURE7:12, MEASURE6:3;
then (GG vol) . 0 <= vol (G . ((pr1 H) . 0)) by MEASURE7:def 6;
then A60: ( (Ser (GG vol)) . 0 = (GG vol) . 0 & (GG vol) . 0 <= (vol G) . ((pr1 H) . 0) ) by MEASURE7:def 7, SUPINF_2:def 11;
for n being Element of NAT holds 0. <= (vol G) . n by MEASURE7:13;
then vol G is nonnegative by SUPINF_2:39;
then (vol G) . m <= (Ser (vol G)) . m by MEASURE7:2;
hence (Ser ((On (G,H)) vol)) . 0 <= (Ser (vol G)) . m by A60, XXREAL_0:2; :: thesis: verum
end;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A59, A3); :: thesis: verum