let X be set ; :: thesis: for F being Field_Subset of X
for M being Measure of F
for k being Element of NAT ex m being Nat st
for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds (Partial_Sums (vol M,(On Cvr))) . k <= (Partial_Sums (Volume M,Cvr)) . m
let F be Field_Subset of X; :: thesis: for M being Measure of F
for k being Element of NAT ex m being Nat st
for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds (Partial_Sums (vol M,(On Cvr))) . k <= (Partial_Sums (Volume M,Cvr)) . m
let M be Measure of F; :: thesis: for k being Element of NAT ex m being Nat st
for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds (Partial_Sums (vol M,(On Cvr))) . k <= (Partial_Sums (Volume M,Cvr)) . m
defpred S1[ Element of NAT ] means ex m being Nat st
for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds (Partial_Sums (vol M,(On Cvr))) . $1 <= (Partial_Sums (Volume M,Cvr)) . m;
{} c= X by XBOOLE_1:2;
then reconsider D = NAT --> {} as Function of NAT ,(bool X) by FUNCOP_1:57;
reconsider y = D as Element of Funcs NAT ,(bool X) by FUNCT_2:11;
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
set a = (pr1 InvPairFunc ) . (k + 1);
set b = (pr2 InvPairFunc ) . (k + 1);
set N0 = { s where s is Element of NAT : (pr1 InvPairFunc ) . (k + 1) = (pr1 InvPairFunc ) . s } ;
A2: { s where s is Element of NAT : (pr1 InvPairFunc ) . (k + 1) = (pr1 InvPairFunc ) . s } c= NAT
proof
let s1 be set ; :: according to TARSKI:def 3 :: thesis: ( not s1 in { s where s is Element of NAT : (pr1 InvPairFunc ) . (k + 1) = (pr1 InvPairFunc ) . s } or s1 in NAT )
assume s1 in { s where s is Element of NAT : (pr1 InvPairFunc ) . (k + 1) = (pr1 InvPairFunc ) . s } ; :: thesis: s1 in NAT
then ex s being Element of NAT st
( s = s1 & (pr1 InvPairFunc ) . (k + 1) = (pr1 InvPairFunc ) . s ) ;
hence s1 in NAT ; :: thesis: verum
end;
k + 1 in { s where s is Element of NAT : (pr1 InvPairFunc ) . (k + 1) = (pr1 InvPairFunc ) . s } ;
then reconsider N0 = { s where s is Element of NAT : (pr1 InvPairFunc ) . (k + 1) = (pr1 InvPairFunc ) . s } as non empty Subset of NAT by A2;
given m0 being Nat such that A3: for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds (Partial_Sums (vol M,(On Cvr))) . k <= (Partial_Sums (Volume M,Cvr)) . m0 ; :: thesis: S1[k + 1]
take m = m0 + ((pr1 InvPairFunc ) . (k + 1)); :: thesis: for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds (Partial_Sums (vol M,(On Cvr))) . (k + 1) <= (Partial_Sums (Volume M,Cvr)) . m
let Sets be SetSequence of X; :: thesis: for Cvr being Covering of Sets,F holds (Partial_Sums (vol M,(On Cvr))) . (k + 1) <= (Partial_Sums (Volume M,Cvr)) . m
let Cvr be Covering of Sets,F; :: thesis: (Partial_Sums (vol M,(On Cvr))) . (k + 1) <= (Partial_Sums (Volume M,Cvr)) . m
defpred S2[ Element of NAT , Function] means ( ( $1 = (pr1 InvPairFunc ) . (k + 1) implies for m being Element of NAT holds $2 . m = (Cvr . $1) . m ) & ( $1 <> (pr1 InvPairFunc ) . (k + 1) implies for m being Element of NAT holds $2 . m = {} ) );
defpred S3[ Element of NAT , Function] means ( ( $1 <> (pr1 InvPairFunc ) . (k + 1) implies for m being Element of NAT holds $2 . m = (Cvr . $1) . m ) & ( $1 = (pr1 InvPairFunc ) . (k + 1) implies for m being Element of NAT holds $2 . m = {} ) );
A4: for n being Element of NAT ex y being Element of Funcs NAT ,(bool X) st S2[n,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of Funcs NAT ,(bool X) st S2[n,y]
A5: now
reconsider y = Cvr . n as Element of Funcs NAT ,(bool X) by FUNCT_2:11;
assume A6: n = (pr1 InvPairFunc ) . (k + 1) ; :: thesis: ex y being Element of Funcs NAT ,(bool X) st S2[n,y]
take y = y; :: thesis: S2[n,y]
thus S2[n,y] by A6; :: thesis: verum
end;
( n <> (pr1 InvPairFunc ) . (k + 1) implies S2[n,y] ) by FUNCOP_1:13;
hence ex y being Element of Funcs NAT ,(bool X) st S2[n,y] by A5; :: thesis: verum
end;
consider Cvr0 being Function of NAT ,(Funcs NAT ,(bool X)) such that
A7: for n being Element of NAT holds S2[n,Cvr0 . n] from FUNCT_2:sch 3(A4);
 A8: for n being Nat holds Cvr0 . n is Covering of D . n,F
proof
let n be Nat; :: thesis: Cvr0 . n is Covering of D . n,F
consider FSets0 being Function such that
A9: Cvr0 . n = FSets0 and
A10: ( dom FSets0 = NAT & rng FSets0 c= bool X ) by FUNCT_2:def 2;
reconsider FSets0 = FSets0 as SetSequence of X by A10, FUNCT_2:4;
for s being Nat holds FSets0 . s in F
proof
let s be Nat; :: thesis: FSets0 . s in F
A11: s in NAT by ORDINAL1:def 13;
A12: now
assume n = (pr1 InvPairFunc ) . (k + 1) ; :: thesis: FSets0 . s in F
then FSets0 . s = (Cvr . n) . s by A7, A9, A11;
hence FSets0 . s in F ; :: thesis: verum
end;
n in NAT by ORDINAL1:def 13;
then ( n <> (pr1 InvPairFunc ) . (k + 1) implies FSets0 . s = {} ) by A7, A9, A11;
hence FSets0 . s in F by A12, PROB_1:10; :: thesis: verum
end;
then A13: FSets0 is Set_Sequence of F by Def2;
n in NAT by ORDINAL1:def 13;
then D . n = {} by FUNCOP_1:13;
then D . n c= union (rng FSets0) by XBOOLE_1:2;
hence Cvr0 . n is Covering of D . n,F by A9, A13, Def3; :: thesis: verum
end;
A14: for n being Element of NAT ex y being Element of Funcs NAT ,(bool X) st S3[n,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of Funcs NAT ,(bool X) st S3[n,y]
A15: now
reconsider y = Cvr . n as Element of Funcs NAT ,(bool X) by FUNCT_2:11;
assume A16: n <> (pr1 InvPairFunc ) . (k + 1) ; :: thesis: ex y being Element of Funcs NAT ,(bool X) st S3[n,y]
take y = y; :: thesis: S3[n,y]
thus S3[n,y] by A16; :: thesis: verum
end;
( n = (pr1 InvPairFunc ) . (k + 1) implies S3[n,y] ) by FUNCOP_1:13;
hence ex y being Element of Funcs NAT ,(bool X) st S3[n,y] by A15; :: thesis: verum
end;
consider Cvr1 being Function of NAT ,(Funcs NAT ,(bool X)) such that
A17: for n being Element of NAT holds S3[n,Cvr1 . n] from FUNCT_2:sch 3(A14);
 for n being Nat holds Cvr1 . n is Covering of D . n,F
proof
let n be Nat; :: thesis: Cvr1 . n is Covering of D . n,F
consider FSets1 being Function such that
A18: Cvr1 . n = FSets1 and
A19: ( dom FSets1 = NAT & rng FSets1 c= bool X ) by FUNCT_2:def 2;
reconsider FSets1 = FSets1 as Function of NAT ,(bool X) by A19, FUNCT_2:4;
for s being Nat holds FSets1 . s in F
proof
let s be Nat; :: thesis: FSets1 . s in F
A20: s in NAT by ORDINAL1:def 13;
A21: n in NAT by ORDINAL1:def 13;
A22: now
assume n <> (pr1 InvPairFunc ) . (k + 1) ; :: thesis: FSets1 . s in F
then FSets1 . s = (Cvr . n) . s by A17, A18, A21, A20;
hence FSets1 . s in F ; :: thesis: verum
end;
( n = (pr1 InvPairFunc ) . (k + 1) implies FSets1 . s = {} ) by A17, A18, A20;
hence FSets1 . s in F by A22, PROB_1:10; :: thesis: verum
end;
then A23: FSets1 is Set_Sequence of F by Def2;
n in NAT by ORDINAL1:def 13;
then D . n = {} by FUNCOP_1:13;
then D . n c= union (rng FSets1) by XBOOLE_1:2;
hence Cvr1 . n is Covering of D . n,F by A18, A23, Def3; :: thesis: verum
end;
then reconsider Cvr1 = Cvr1 as Covering of D,F by Def4;
reconsider Cvr0 = Cvr0 as Covering of D,F by A8, Def4;
set PSv1 = Partial_Sums (vol M,(On Cvr1));
(On Cvr1) . (k + 1) = (Cvr1 . ((pr1 InvPairFunc ) . (k + 1))) . ((pr2 InvPairFunc ) . (k + 1)) by Def10
.= {} by A17 ;
then A24: (vol M,(On Cvr1)) . (k + 1) = M . {} by Def5
.= 0 by VALUED_0:def 19 ;
set PSv0 = Partial_Sums (vol M,(On Cvr0));
set PSv = Partial_Sums (vol M,(On Cvr));
defpred S4[ Element of N0, Element of NAT ] means $2 = (pr2 InvPairFunc ) . $1;
A25: for s being Element of N0 ex y being Element of NAT st S4[s,y] ;
consider SOS being Function of N0,NAT such that
A26: for s being Element of N0 holds S4[s,SOS . s] from FUNCT_2:sch 3(A25);
 A27: for s being Element of NAT holds
( ( s in N0 implies (vol M,(On Cvr0)) . s = ((vol M,(Cvr0 . ((pr1 InvPairFunc ) . (k + 1)))) * SOS) . s ) & ( not s in N0 implies (vol M,(On Cvr0)) . s = 0 ) )
proof
let s be Element of NAT ; :: thesis: ( ( s in N0 implies (vol M,(On Cvr0)) . s = ((vol M,(Cvr0 . ((pr1 InvPairFunc ) . (k + 1)))) * SOS) . s ) & ( not s in N0 implies (vol M,(On Cvr0)) . s = 0 ) )
thus ( s in N0 implies (vol M,(On Cvr0)) . s = ((vol M,(Cvr0 . ((pr1 InvPairFunc ) . (k + 1)))) * SOS) . s ) :: thesis: ( not s in N0 implies (vol M,(On Cvr0)) . s = 0 )
proof
A28: (vol M,(On Cvr0)) . s = M . ((On Cvr0) . s) by Def5;
assume A29: s in N0 ; :: thesis: (vol M,(On Cvr0)) . s = ((vol M,(Cvr0 . ((pr1 InvPairFunc ) . (k + 1)))) * SOS) . s
then ( ex s1 being Element of NAT st
( s1 = s & (pr1 InvPairFunc ) . (k + 1) = (pr1 InvPairFunc ) . s1 ) & (pr2 InvPairFunc ) . s = SOS . s ) by A26;
then (vol M,(On Cvr0)) . s = M . ((Cvr0 . ((pr1 InvPairFunc ) . (k + 1))) . (SOS . s)) by A28, Def10;
then (vol M,(On Cvr0)) . s = (vol M,(Cvr0 . ((pr1 InvPairFunc ) . (k + 1)))) . (SOS . s) by Def5;
hence (vol M,(On Cvr0)) . s = ((vol M,(Cvr0 . ((pr1 InvPairFunc ) . (k + 1)))) * SOS) . s by A29, FUNCT_2:21; :: thesis: verum
end;
assume not s in N0 ; :: thesis: (vol M,(On Cvr0)) . s = 0
then A30: not (pr1 InvPairFunc ) . (k + 1) = (pr1 InvPairFunc ) . s ;
(vol M,(On Cvr0)) . s = M . ((On Cvr0) . s) by Def5
.= M . ((Cvr0 . ((pr1 InvPairFunc ) . s)) . ((pr2 InvPairFunc ) . s)) by Def10
.= M . {} by A7, A30 ;
hence (vol M,(On Cvr0)) . s = 0 by VALUED_0:def 19; :: thesis: verum
end;
now
let s1, s2 be set ; :: thesis: ( s1 in N0 & s2 in N0 & SOS . s1 = SOS . s2 implies s1 = s2 )
assume that
A31: ( s1 in N0 & s2 in N0 ) and
A32: SOS . s1 = SOS . s2 ; :: thesis: s1 = s2
A33: ( ex s11 being Element of NAT st
( s11 = s1 & (pr1 InvPairFunc ) . (k + 1) = (pr1 InvPairFunc ) . s11 ) & ex s22 being Element of NAT st
( s22 = s2 & (pr1 InvPairFunc ) . (k + 1) = (pr1 InvPairFunc ) . s22 ) ) by A31;
A34: ( InvPairFunc . s1 = [((pr1 InvPairFunc ) . s1),((pr2 InvPairFunc ) . s1)] & InvPairFunc . s2 = [((pr1 InvPairFunc ) . s2),((pr2 InvPairFunc ) . s2)] ) by A31, FUNCT_2:196;
( SOS . s1 = (pr2 InvPairFunc ) . s1 & SOS . s2 = (pr2 InvPairFunc ) . s2 ) by A26, A31;
hence s1 = s2 by A32, A33, A34, FUNCT_2:25, NAGATA_2:2; :: thesis: verum
end;
then A35: SOS is one-to-one by FUNCT_2:25;
(Ser (vol M,(On Cvr1))) . (k + 1) = ((Ser (vol M,(On Cvr1))) . k) + ((vol M,(On Cvr1)) . (k + 1)) by SUPINF_2:63
.= (Ser (vol M,(On Cvr1))) . k by A24, XXREAL_3:4 ;
then (Partial_Sums (vol M,(On Cvr1))) . (k + 1) = (Ser (vol M,(On Cvr1))) . k by Th1;
then A36: (Partial_Sums (vol M,(On Cvr1))) . (k + 1) = (Partial_Sums (vol M,(On Cvr1))) . k by Th1;
for s being Element of NAT holds 0. <= (Volume M,Cvr0) . s by Th5;
then A37: Volume M,Cvr0 is nonnegative by SUPINF_2:58;
then (Volume M,Cvr0) . ((pr1 InvPairFunc ) . (k + 1)) <= (Ser (Volume M,Cvr0)) . ((pr1 InvPairFunc ) . (k + 1)) by MEASURE7:2;
then A38: SUM (vol M,(Cvr0 . ((pr1 InvPairFunc ) . (k + 1)))) <= (Ser (Volume M,Cvr0)) . ((pr1 InvPairFunc ) . (k + 1)) by Def6;
A39: m0 is Element of NAT by ORDINAL1:def 13;
then (Ser (Volume M,Cvr0)) . ((pr1 InvPairFunc ) . (k + 1)) <= (Ser (Volume M,Cvr0)) . m by A37, SUPINF_2:60;
then A40: SUM (vol M,(Cvr0 . ((pr1 InvPairFunc ) . (k + 1)))) <= (Ser (Volume M,Cvr0)) . m by A38, XXREAL_0:2;
vol M,(Cvr0 . ((pr1 InvPairFunc ) . (k + 1))) is nonnegative by Th4;
then SUM (vol M,(On Cvr0)) <= SUM (vol M,(Cvr0 . ((pr1 InvPairFunc ) . (k + 1)))) by A35, A27, MEASURE7:12;
then A41: SUM (vol M,(On Cvr0)) <= (Ser (Volume M,Cvr0)) . m by A40, XXREAL_0:2;
(Ser (vol M,(On Cvr0))) . (k + 1) <= SUM (vol M,(On Cvr0)) by Th4, MEASURE7:7;
then (Ser (vol M,(On Cvr0))) . (k + 1) <= (Ser (Volume M,Cvr0)) . m by A41, XXREAL_0:2;
then (Partial_Sums (vol M,(On Cvr0))) . (k + 1) <= (Ser (Volume M,Cvr0)) . m by Th1;
then A42: (Partial_Sums (vol M,(On Cvr0))) . (k + 1) <= (Partial_Sums (Volume M,Cvr0)) . m by Th1;
for s being Element of NAT holds 0. <= (Volume M,Cvr1) . s by Th5;
then A43: Volume M,Cvr1 is nonnegative by SUPINF_2:58;
then ( m0 <= m & Partial_Sums (Volume M,Cvr1) is non-decreasing ) by MESFUNC9:16, NAT_1:11;
then A44: (Partial_Sums (Volume M,Cvr1)) . m0 <= (Partial_Sums (Volume M,Cvr1)) . m by A39, RINFSUP2:7;
A45: for n being Element of NAT holds (vol M,(On Cvr)) . n = ((vol M,(On Cvr0)) . n) + ((vol M,(On Cvr1)) . n)
proof
let n be Element of NAT ; :: thesis: (vol M,(On Cvr)) . n = ((vol M,(On Cvr0)) . n) + ((vol M,(On Cvr1)) . n)
set n1 = (pr1 InvPairFunc ) . n;
set n2 = (pr2 InvPairFunc ) . n;
A46: ( (vol M,(On Cvr0)) . n = M . ((On Cvr0) . n) & (vol M,(On Cvr1)) . n = M . ((On Cvr1) . n) ) by Def5;
(vol M,(On Cvr)) . n = M . ((On Cvr) . n) by Def5;
then A47: (vol M,(On Cvr)) . n = M . ((Cvr . ((pr1 InvPairFunc ) . n)) . ((pr2 InvPairFunc ) . n)) by Def10;
per cases ( (pr1 InvPairFunc ) . n = (pr1 InvPairFunc ) . (k + 1) or (pr1 InvPairFunc ) . n <> (pr1 InvPairFunc ) . (k + 1) ) ;
suppose A48: (pr1 InvPairFunc ) . n = (pr1 InvPairFunc ) . (k + 1) ; :: thesis: (vol M,(On Cvr)) . n = ((vol M,(On Cvr0)) . n) + ((vol M,(On Cvr1)) . n)
(On Cvr1) . n = (Cvr1 . ((pr1 InvPairFunc ) . n)) . ((pr2 InvPairFunc ) . n) by Def10
.= {} by A17, A48 ;
then A49: M . ((On Cvr1) . n) = 0 by VALUED_0:def 19;
(On Cvr0) . n = (Cvr0 . ((pr1 InvPairFunc ) . n)) . ((pr2 InvPairFunc ) . n) by Def10
.= (Cvr . ((pr1 InvPairFunc ) . n)) . ((pr2 InvPairFunc ) . n) by A7, A48 ;
hence (vol M,(On Cvr)) . n = ((vol M,(On Cvr0)) . n) + ((vol M,(On Cvr1)) . n) by A46, A47, A49, XXREAL_3:4; :: thesis: verum
end;
suppose A50: (pr1 InvPairFunc ) . n <> (pr1 InvPairFunc ) . (k + 1) ; :: thesis: (vol M,(On Cvr)) . n = ((vol M,(On Cvr0)) . n) + ((vol M,(On Cvr1)) . n)
(On Cvr0) . n = (Cvr0 . ((pr1 InvPairFunc ) . n)) . ((pr2 InvPairFunc ) . n) by Def10
.= {} by A7, A50 ;
then A51: M . ((On Cvr0) . n) = 0 by VALUED_0:def 19;
(On Cvr1) . n = (Cvr1 . ((pr1 InvPairFunc ) . n)) . ((pr2 InvPairFunc ) . n) by Def10
.= (Cvr . ((pr1 InvPairFunc ) . n)) . ((pr2 InvPairFunc ) . n) by A17, A50 ;
hence (vol M,(On Cvr)) . n = ((vol M,(On Cvr0)) . n) + ((vol M,(On Cvr1)) . n) by A46, A47, A51, XXREAL_3:4; :: thesis: verum
end;
end;
end;
( vol M,(On Cvr0) is nonnegative & vol M,(On Cvr1) is nonnegative ) by Th4;
then (Ser (vol M,(On Cvr))) . (k + 1) = ((Ser (vol M,(On Cvr0))) . (k + 1)) + ((Ser (vol M,(On Cvr1))) . (k + 1)) by A45, MEASURE7:3;
then (Partial_Sums (vol M,(On Cvr))) . (k + 1) = ((Ser (vol M,(On Cvr0))) . (k + 1)) + ((Ser (vol M,(On Cvr1))) . (k + 1)) by Th1;
then (Partial_Sums (vol M,(On Cvr))) . (k + 1) = ((Partial_Sums (vol M,(On Cvr0))) . (k + 1)) + ((Ser (vol M,(On Cvr1))) . (k + 1)) by Th1;
then A52: (Partial_Sums (vol M,(On Cvr))) . (k + 1) = ((Partial_Sums (vol M,(On Cvr0))) . (k + 1)) + ((Partial_Sums (vol M,(On Cvr1))) . (k + 1)) by Th1;
(Partial_Sums (vol M,(On Cvr1))) . k <= (Partial_Sums (Volume M,Cvr1)) . m0 by A3;
then A53: (Partial_Sums (vol M,(On Cvr1))) . (k + 1) <= (Partial_Sums (Volume M,Cvr1)) . m by A36, A44, XXREAL_0:2;
for n being Element of NAT holds (Volume M,Cvr) . n = ((Volume M,Cvr0) . n) + ((Volume M,Cvr1) . n)
proof
let n be Element of NAT ; :: thesis: (Volume M,Cvr) . n = ((Volume M,Cvr0) . n) + ((Volume M,Cvr1) . n)
A54: now
assume A55: n <> (pr1 InvPairFunc ) . (k + 1) ; :: thesis: SUM (vol M,(Cvr . n)) = (SUM (vol M,(Cvr0 . n))) + (SUM (vol M,(Cvr1 . n)))
for s being Element of NAT holds (vol M,(Cvr0 . n)) . s = 0.
proof
let s be Element of NAT ; :: thesis: (vol M,(Cvr0 . n)) . s = 0.
(Cvr0 . n) . s = {} by A7, A55;
then M . ((Cvr0 . n) . s) = 0 by VALUED_0:def 19;
hence (vol M,(Cvr0 . n)) . s = 0. by Def5; :: thesis: verum
end;
then A56: SUM (vol M,(Cvr0 . n)) = 0. by MEASURE7:1;
for s being Element of NAT holds
( (vol M,(Cvr1 . n)) . s <= (vol M,(Cvr . n)) . s & (vol M,(Cvr . n)) . s <= (vol M,(Cvr1 . n)) . s )
proof
let s be Element of NAT ; :: thesis: ( (vol M,(Cvr1 . n)) . s <= (vol M,(Cvr . n)) . s & (vol M,(Cvr . n)) . s <= (vol M,(Cvr1 . n)) . s )
( (vol M,(Cvr1 . n)) . s = M . ((Cvr1 . n) . s) & (vol M,(Cvr . n)) . s = M . ((Cvr . n) . s) ) by Def5;
hence ( (vol M,(Cvr1 . n)) . s <= (vol M,(Cvr . n)) . s & (vol M,(Cvr . n)) . s <= (vol M,(Cvr1 . n)) . s ) by A17, A55; :: thesis: verum
end;
then ( SUM (vol M,(Cvr1 . n)) <= SUM (vol M,(Cvr . n)) & SUM (vol M,(Cvr . n)) <= SUM (vol M,(Cvr1 . n)) ) by SUPINF_2:62;
then SUM (vol M,(Cvr . n)) = SUM (vol M,(Cvr1 . n)) by XXREAL_0:1;
hence SUM (vol M,(Cvr . n)) = (SUM (vol M,(Cvr0 . n))) + (SUM (vol M,(Cvr1 . n))) by A56, XXREAL_3:4; :: thesis: verum
end;
A57: now
assume A58: n = (pr1 InvPairFunc ) . (k + 1) ; :: thesis: SUM (vol M,(Cvr . n)) = (SUM (vol M,(Cvr0 . n))) + (SUM (vol M,(Cvr1 . n)))
for s being Element of NAT holds (vol M,(Cvr1 . n)) . s = 0
proof
let s be Element of NAT ; :: thesis: (vol M,(Cvr1 . n)) . s = 0
(Cvr1 . n) . s = {} by A17, A58;
then M . ((Cvr1 . n) . s) = 0 by VALUED_0:def 19;
hence (vol M,(Cvr1 . n)) . s = 0 by Def5; :: thesis: verum
end;
then A59: SUM (vol M,(Cvr1 . n)) = 0 by MEASURE7:1;
for s being Element of NAT holds
( (vol M,(Cvr . n)) . s <= (vol M,(Cvr0 . n)) . s & (vol M,(Cvr0 . n)) . s <= (vol M,(Cvr . n)) . s )
proof
let s be Element of NAT ; :: thesis: ( (vol M,(Cvr . n)) . s <= (vol M,(Cvr0 . n)) . s & (vol M,(Cvr0 . n)) . s <= (vol M,(Cvr . n)) . s )
(vol M,(Cvr0 . n)) . s = M . ((Cvr0 . n) . s) by Def5
.= M . ((Cvr . n) . s) by A7, A58 ;
hence ( (vol M,(Cvr . n)) . s <= (vol M,(Cvr0 . n)) . s & (vol M,(Cvr0 . n)) . s <= (vol M,(Cvr . n)) . s ) by Def5; :: thesis: verum
end;
then ( SUM (vol M,(Cvr . n)) <= SUM (vol M,(Cvr0 . n)) & SUM (vol M,(Cvr0 . n)) <= SUM (vol M,(Cvr . n)) ) by SUPINF_2:62;
then SUM (vol M,(Cvr . n)) = SUM (vol M,(Cvr0 . n)) by XXREAL_0:1;
hence SUM (vol M,(Cvr . n)) = (SUM (vol M,(Cvr0 . n))) + (SUM (vol M,(Cvr1 . n))) by A59, XXREAL_3:4; :: thesis: verum
end;
( (Volume M,Cvr) . n = SUM (vol M,(Cvr . n)) & (Volume M,Cvr0) . n = SUM (vol M,(Cvr0 . n)) ) by Def6;
hence (Volume M,Cvr) . n = ((Volume M,Cvr0) . n) + ((Volume M,Cvr1) . n) by A57, A54, Def6; :: thesis: verum
end;
then (Ser (Volume M,Cvr)) . m = ((Ser (Volume M,Cvr0)) . m) + ((Ser (Volume M,Cvr1)) . m) by A37, A43, MEASURE7:3;
then (Partial_Sums (Volume M,Cvr)) . m = ((Ser (Volume M,Cvr0)) . m) + ((Ser (Volume M,Cvr1)) . m) by Th1
.= ((Partial_Sums (Volume M,Cvr0)) . m) + ((Ser (Volume M,Cvr1)) . m) by Th1
.= ((Partial_Sums (Volume M,Cvr0)) . m) + ((Partial_Sums (Volume M,Cvr1)) . m) by Th1 ;
hence (Partial_Sums (vol M,(On Cvr))) . (k + 1) <= (Partial_Sums (Volume M,Cvr)) . m by A42, A53, A52, XXREAL_3:38; :: thesis: verum
end;
A60: S1[ 0 ]
proof
take m = (pr1 InvPairFunc ) . 0 ; :: thesis: for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds (Partial_Sums (vol M,(On Cvr))) . 0 <= (Partial_Sums (Volume M,Cvr)) . m
let Sets be SetSequence of X; :: thesis: for Cvr being Covering of Sets,F holds (Partial_Sums (vol M,(On Cvr))) . 0 <= (Partial_Sums (Volume M,Cvr)) . m
let Cvr be Covering of Sets,F; :: thesis: (Partial_Sums (vol M,(On Cvr))) . 0 <= (Partial_Sums (Volume M,Cvr)) . m
for n being Element of NAT holds 0 <= (Volume M,Cvr) . n by Th5;
then Volume M,Cvr is nonnegative by SUPINF_2:58;
then (Volume M,Cvr) . m <= (Ser (Volume M,Cvr)) . m by MEASURE7:2;
then A61: (Volume M,Cvr) . m <= (Partial_Sums (Volume M,Cvr)) . m by Th1;
( (vol M,(On Cvr)) . 0 = M . ((On Cvr) . 0 ) & (vol M,(Cvr . ((pr1 InvPairFunc ) . 0 ))) . ((pr2 InvPairFunc ) . 0 ) = M . ((Cvr . ((pr1 InvPairFunc ) . 0 )) . ((pr2 InvPairFunc ) . 0 )) ) by Def5;
then (vol M,(On Cvr)) . 0 <= (vol M,(Cvr . ((pr1 InvPairFunc ) . 0 ))) . ((pr2 InvPairFunc ) . 0 ) by Def10;
then (vol M,(On Cvr)) . 0 <= SUM (vol M,(Cvr . ((pr1 InvPairFunc ) . 0 ))) by Th4, MEASURE6:3;
then ( (Partial_Sums (vol M,(On Cvr))) . 0 = (vol M,(On Cvr)) . 0 & (vol M,(On Cvr)) . 0 <= (Volume M,Cvr) . ((pr1 InvPairFunc ) . 0 ) ) by Def6, MESFUNC9:def 1;
hence (Partial_Sums (vol M,(On Cvr))) . 0 <= (Partial_Sums (Volume M,Cvr)) . m by A61, XXREAL_0:2; :: thesis: verum
end;
thus for k being Element of NAT holds S1[k] from NAT_1:sch 1(A60, A1); :: thesis: verum