let X be set ; :: thesis: for F being Field_Subset of X
for M being Measure of F
for k being 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 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 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[ 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 ;
then reconsider D = NAT --> {} as sequence of (bool X) by FUNCOP_1:45;
reconsider y = D as Element of Funcs (NAT,(bool X)) by FUNCT_2:8;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be 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 object ; :: 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 :: thesis: ( n = (pr1 InvPairFunc) . (k + 1) implies ex y being Element of Funcs (NAT,(bool X)) st S2[n,y] )
reconsider y = Cvr . n as Element of Funcs (NAT,(bool X)) by FUNCT_2:8;
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:7;
hence ex y being Element of Funcs (NAT,(bool X)) st S2[n,y] by A5; :: thesis: verum
end;
consider Cvr0 being sequence of (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:2;
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 12;
A12: now :: thesis: ( n = (pr1 InvPairFunc) . (k + 1) implies FSets0 . s in F )
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 12;
then ( n <> (pr1 InvPairFunc) . (k + 1) implies FSets0 . s = {} ) by A7, A9, A11;
hence FSets0 . s in F by A12, PROB_1:4; :: thesis: verum
end;
then A13: FSets0 is Set_Sequence of F by Def2;
n in NAT by ORDINAL1:def 12;
then D . n = {} by FUNCOP_1:7;
then D . n c= union (rng FSets0) ;
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 :: thesis: ( n <> (pr1 InvPairFunc) . (k + 1) implies ex y being Element of Funcs (NAT,(bool X)) st S3[n,y] )
reconsider y = Cvr . n as Element of Funcs (NAT,(bool X)) by FUNCT_2:8;
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:7;
hence ex y being Element of Funcs (NAT,(bool X)) st S3[n,y] by A15; :: thesis: verum
end;
consider Cvr1 being sequence of (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 sequence of (bool X) by A19, FUNCT_2:2;
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 12;
A21: n in NAT by ORDINAL1:def 12;
A22: now :: thesis: ( n <> (pr1 InvPairFunc) . (k + 1) implies FSets1 . s in F )
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:4; :: thesis: verum
end;
then A23: FSets1 is Set_Sequence of F by Def2;
n in NAT by ORDINAL1:def 12;
then D . n = {} by FUNCOP_1:7;
then D . n c= union (rng FSets1) ;
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:15; :: 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 :: thesis: for s1, s2 being object st s1 in N0 & s2 in N0 & SOS . s1 = SOS . s2 holds
s1 = s2
let s1, s2 be object ; :: 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:119;
( SOS . s1 = (pr2 InvPairFunc) . s1 & SOS . s2 = (pr2 InvPairFunc) . s2 ) by A26, A31;
hence s1 = s2 by A32, A33, A34, FUNCT_2:19, NAGATA_2:2; :: thesis: verum
end;
then A35: SOS is one-to-one by FUNCT_2:19;
(Ser (vol (M,(On Cvr1)))) . (k + 1) = ((Ser (vol (M,(On Cvr1)))) . k) + ((vol (M,(On Cvr1))) . (k + 1)) by SUPINF_2:def 11
.= (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:39;
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;
(Ser (Volume (M,Cvr0))) . ((pr1 InvPairFunc) . (k + 1)) <= (Ser (Volume (M,Cvr0))) . m by A37, SUPINF_2:41;
then A39: 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:11;
then A40: SUM (vol (M,(On Cvr0))) <= (Ser (Volume (M,Cvr0))) . m by A39, XXREAL_0:2;
(Ser (vol (M,(On Cvr0)))) . (k + 1) <= SUM (vol (M,(On Cvr0))) by Th4, MEASURE7:6;
then (Ser (vol (M,(On Cvr0)))) . (k + 1) <= (Ser (Volume (M,Cvr0))) . m by A40, XXREAL_0:2;
then (Partial_Sums (vol (M,(On Cvr0)))) . (k + 1) <= (Ser (Volume (M,Cvr0))) . m by Th1;
then A41: (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 A42: Volume (M,Cvr1) is nonnegative by SUPINF_2:39;
then ( m0 <= m & Partial_Sums (Volume (M,Cvr1)) is non-decreasing ) by MESFUNC9:16, NAT_1:11;
then A43: (Partial_Sums (Volume (M,Cvr1))) . m0 <= (Partial_Sums (Volume (M,Cvr1))) . m by RINFSUP2:7;
A44: 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;
A45: ( (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 A46: (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 A47: (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, A47 ;
then A48: 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, A47 ;
hence (vol (M,(On Cvr))) . n = ((vol (M,(On Cvr0))) . n) + ((vol (M,(On Cvr1))) . n) by A45, A46, A48, XXREAL_3:4; :: thesis: verum
end;
suppose A49: (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, A49 ;
then A50: 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, A49 ;
hence (vol (M,(On Cvr))) . n = ((vol (M,(On Cvr0))) . n) + ((vol (M,(On Cvr1))) . n) by A45, A46, A50, 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 A44, 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 A51: (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 A52: (Partial_Sums (vol (M,(On Cvr1)))) . (k + 1) <= (Partial_Sums (Volume (M,Cvr1))) . m by A36, A43, 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)
A53: now :: thesis: ( n <> (pr1 InvPairFunc) . (k + 1) implies SUM (vol (M,(Cvr . n))) = (SUM (vol (M,(Cvr0 . n)))) + (SUM (vol (M,(Cvr1 . n)))) )
assume A54: 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, A54;
then M . ((Cvr0 . n) . s) = 0 by VALUED_0:def 19;
hence (vol (M,(Cvr0 . n))) . s = 0. by Def5; :: thesis: verum
end;
then A55: 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, A54; :: 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:43;
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 A55, XXREAL_3:4; :: thesis: verum
end;
A56: now :: thesis: ( n = (pr1 InvPairFunc) . (k + 1) implies SUM (vol (M,(Cvr . n))) = (SUM (vol (M,(Cvr0 . n)))) + (SUM (vol (M,(Cvr1 . n)))) )
assume A57: 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, A57;
then M . ((Cvr1 . n) . s) = 0 by VALUED_0:def 19;
hence (vol (M,(Cvr1 . n))) . s = 0 by Def5; :: thesis: verum
end;
then A58: 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, A57 ;
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:43;
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 A58, 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 A56, A53, Def6; :: thesis: verum
end;
then (Ser (Volume (M,Cvr))) . m = ((Ser (Volume (M,Cvr0))) . m) + ((Ser (Volume (M,Cvr1))) . m) by A37, A42, 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 A41, A52, A51, XXREAL_3:36; :: thesis: verum
end;
A59: 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:39;
then (Volume (M,Cvr)) . m <= (Ser (Volume (M,Cvr))) . m by MEASURE7:2;
then A60: (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 A60, XXREAL_0:2; :: thesis: verum
end;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A59, A1); :: thesis: verum