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 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 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 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 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 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 Interval_Covering of F holds (Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . m
let G be 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, FUNCOP_1:7; :: 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 Interval_Covering of D . n
proof
let n be Element of NAT ; :: thesis: G1 . n is 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 = {} by FUNCOP_1:7;
then D . n c= union (rng f0) ;
then reconsider f0 = f0 as Interval_Covering of D . n by A13, Def2;
G1 . n = f0 by A11;
hence G1 . n is 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, FUNCOP_1:7; :: 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 = {} by FUNCOP_1:7;
then D . n c= union (rng f0) ;
then reconsider f0 = f0 as Interval_Covering of D . n by A20, Def2;
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 Def3;
set GG0 = On (G0,H);
reconsider G1 = G1 as Interval_Covering of D by A10, Def3;
set GG1 = On (G1,H);
A21: (Ser ((On (G0,H)) vol)) . (k + 1) <= SUM ((On (G0,H)) vol) by Th6, Th12;
(On (G1,H)) . (k + 1) = (G1 . ((pr1 H) . (k + 1))) . ((pr2 H) . (k + 1)) by A2, Def11
.= {} by A9 ;
then A22: ((On (G1,H)) vol) . (k + 1) = 0. by Def4, 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 A23: (Ser ((On (G1,H)) vol)) . (k + 1) = (Ser ((On (G1,H)) vol)) . k by A22, XXREAL_3:4;
for s being Element of NAT holds 0. <= (vol G1) . s by Th13;
then vol G1 is nonnegative by SUPINF_2:39;
then A24: (Ser (vol G1)) . m0 <= (Ser (vol G1)) . m by SUPINF_2:41;
A25: 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)
A26: ( ((On (G0,H)) vol) . n = diameter ((On (G0,H)) . n) & ((On (G1,H)) vol) . n = diameter ((On (G1,H)) . n) ) by Def4;
((On (G,H)) vol) . n = diameter ((On (G,H)) . n) by Def4;
then A27: ((On (G,H)) vol) . n = diameter ((G . ((pr1 H) . n)) . ((pr2 H) . n)) by A2, Def11;
per cases ( (pr1 H) . n = (pr1 H) . (k + 1) or (pr1 H) . n <> (pr1 H) . (k + 1) ) ;
suppose A28: (pr1 H) . n = (pr1 H) . (k + 1) ; :: thesis: ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n)
A29: (On (G1,H)) . n = (G1 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, Def11
.= {} by A9, A28 ;
(On (G0,H)) . n = (G0 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, Def11
.= (G . ((pr1 H) . n)) . ((pr2 H) . n) by A17, A28 ;
hence ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n) by A26, A27, A29, MEASURE5:10, XXREAL_3:4; :: thesis: verum
end;
suppose A30: (pr1 H) . n <> (pr1 H) . (k + 1) ; :: thesis: ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n)
A31: (On (G0,H)) . n = (G0 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, Def11
.= {} by A17, A30 ;
(On (G1,H)) . n = (G1 . ((pr1 H) . n)) . ((pr2 H) . n) by A2, Def11
.= (G . ((pr1 H) . n)) . ((pr2 H) . n) by A9, A30 ;
hence ((On (G,H)) vol) . n = (((On (G0,H)) vol) . n) + (((On (G1,H)) vol) . n) by A26, A27, A31, MEASURE5:10, XXREAL_3:4; :: thesis: verum
end;
end;
end;
( (On (G0,H)) vol is nonnegative & (On (G1,H)) vol is nonnegative ) by Th12;
then A32: (Ser ((On (G,H)) vol)) . (k + 1) = ((Ser ((On (G0,H)) vol)) . (k + 1)) + ((Ser ((On (G1,H)) vol)) . (k + 1)) by A25, Th3;
for s being Element of NAT holds 0. <= (vol G1) . s by Th13;
then A33: vol G1 is nonnegative by SUPINF_2:39;
(Ser ((On (G1,H)) vol)) . k <= (Ser (vol G1)) . m0 by A5;
then A34: (Ser ((On (G1,H)) vol)) . (k + 1) <= (Ser (vol G1)) . m by A23, A24, XXREAL_0:2;
A35: 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
A36: for s being Element of N0 holds S3[s,SOS . s] from FUNCT_2:sch 3(A35);
 A37: 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)
A38: vol (G . n) = (vol (G0 . n)) + (vol (G1 . n))
proof
per cases ( n = (pr1 H) . (k + 1) or n <> (pr1 H) . (k + 1) ) ;
suppose A39: 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 Def4
.= diameter ((G . n) . s) by A17, A39
.= ((G . n) vol) . s by Def4 ;
hence ((G . n) vol) . s <= ((G0 . n) vol) . s ; :: thesis: verum
end;
then A40: 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, A39, MEASURE5:10;
hence ((G1 . n) vol) . s = 0. by Def4; :: thesis: verum
end;
then A41: SUM ((G1 . n) vol) = 0. by Th1;
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 Def4
.= diameter ((G . n) . s) by A17, A39
.= ((G . n) vol) . s by Def4 ;
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 A40, XXREAL_0:1;
hence vol (G . n) = (vol (G0 . n)) + (vol (G1 . n)) by A41, XXREAL_3:4; :: thesis: verum
end;
suppose A42: n <> (pr1 H) . (k + 1) ; :: thesis: vol (G . n) = (vol (G0 . n)) + (vol (G1 . n))
A43: 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 Def4;
hence ((G1 . n) vol) . s = ((G . n) vol) . s by A9, A42; :: thesis: verum
end;
then for s being Element of NAT holds ((G . n) vol) . s <= ((G1 . n) vol) . s ;
then A44: 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, A42, MEASURE5:10;
hence ((G0 . n) vol) . s = 0. by Def4; :: thesis: verum
end;
then A45: SUM ((G0 . n) vol) = 0. by Th1;
for s being Element of NAT holds ((G1 . n) vol) . s <= ((G . n) vol) . s by A43;
then SUM ((G1 . n) vol) <= SUM ((G . n) vol) by SUPINF_2:43;
then SUM ((G . n) vol) = SUM ((G1 . n) vol) by A44, XXREAL_0:1;
hence vol (G . n) = (vol (G0 . n)) + (vol (G1 . n)) by A45, XXREAL_3:4; :: thesis: verum
end;
end;
end;
( (vol G) . n = vol (G . n) & (vol G0) . n = vol (G0 . n) ) by Def7;
hence (vol G) . n = ((vol G0) . n) + ((vol G1) . n) by A38, Def7; :: thesis: verum
end;
for s being Element of NAT holds 0. <= (vol G0) . s by Th13;
then vol G0 is nonnegative by SUPINF_2:39;
then A46: ( (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 Th2, SUPINF_2:41;
A47: 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 A48: s in N0 ; :: thesis: ((On (G0,H)) vol) . s = (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s
then A49: ex s1 being Element of NAT st
( s1 = s & (pr1 H) . (k + 1) = (pr1 H) . s1 ) ;
A50: (pr2 H) . s = SOS . s by A36, A48;
((On (G0,H)) vol) . s = diameter ((On (G0,H)) . s) by Def4
.= diameter ((G0 . ((pr1 H) . (k + 1))) . ((pr2 H) . s)) by A2, A49, Def11
.= ((G0 . ((pr1 H) . (k + 1))) vol) . (SOS . s) by A50, Def4
.= (((G0 . ((pr1 H) . (k + 1))) vol) * SOS) . s by A48, 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 A51: not (pr1 H) . (k + 1) = (pr1 H) . s ;
((On (G0,H)) vol) . s = diameter ((On (G0,H)) . s) by Def4
.= diameter ((G0 . ((pr1 H) . s)) . ((pr2 H) . s)) by A2, Def11
.= 0. by A17, A51, 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
A52: ( s1 in N0 & s2 in N0 ) and
A53: SOS . s1 = SOS . s2 ; :: thesis: s1 = s2
reconsider s1 = s1, s2 = s2 as Element of NAT by A52;
A54: ( 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 A52;
A55: ( 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 A36, A52;
hence s1 = s2 by A1, A53, A54, A55, FUNCT_2:19; :: thesis: verum
end;
then A56: SOS is one-to-one by FUNCT_2:19;
(G0 . ((pr1 H) . (k + 1))) vol is nonnegative by Th12;
then SUM ((On (G0,H)) vol) <= SUM ((G0 . ((pr1 H) . (k + 1))) vol) by A56, A47, Th11;
then A57: (Ser ((On (G0,H)) vol)) . (k + 1) <= SUM ((G0 . ((pr1 H) . (k + 1))) vol) by A21, XXREAL_0:2;
SUM ((G0 . ((pr1 H) . (k + 1))) vol) = vol (G0 . ((pr1 H) . (k + 1)))
.= (vol G0) . ((pr1 H) . (k + 1)) by Def7 ;
then SUM ((G0 . ((pr1 H) . (k + 1))) vol) <= (Ser (vol G0)) . m by A46, 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 Th13;
then vol G0 is nonnegative by SUPINF_2:39;
then (Ser (vol G)) . m = ((Ser (vol G0)) . m) + ((Ser (vol G1)) . m) by A37, A33, Th3;
hence (Ser ((On (G,H)) vol)) . (k + 1) <= (Ser (vol G)) . m by A58, A34, A32, 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 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 Interval_Covering of F holds (Ser ((On (G,H)) vol)) . 0 <= (Ser (vol G)) . m
let G be Interval_Covering of F; :: thesis: (Ser ((On (G,H)) vol)) . 0 <= (Ser (vol G)) . m
reconsider GG = On (G,H) as Interval_Covering of union (rng F) ;
( (GG vol) . 0 = diameter (GG . 0) & ((G . ((pr1 H) . 0)) vol) . ((pr2 H) . 0) = diameter ((G . ((pr1 H) . 0)) . ((pr2 H) . 0)) ) by Def4;
then (GG vol) . 0 <= ((G . ((pr1 H) . 0)) vol) . ((pr2 H) . 0) by A2, Def11;
then (GG vol) . 0 <= vol (G . ((pr1 H) . 0)) by Th12, MEASURE6:3;
then A60: ( (Ser (GG vol)) . 0 = (GG vol) . 0 & (GG vol) . 0 <= (vol G) . ((pr1 H) . 0) ) by Def7, SUPINF_2:def 11;
for n being Element of NAT holds 0. <= (vol G) . n by Th13;
then vol G is nonnegative by SUPINF_2:39;
then (vol G) . m <= (Ser (vol G)) . m by Th2;
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