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 S_{1}[ 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 S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A59, A1); :: thesis: verum

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 S

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 S

S

proof

A59:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[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

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: S_{1}[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 S_{2}[ 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 S_{3}[ 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 S_{2}[n,y]

A7: for n being Element of NAT holds S_{2}[n,Cvr0 . n]
from FUNCT_2:sch 3(A4);

A8: for n being Nat holds Cvr0 . n is Covering of D . n,F_{3}[n,y]

A17: for n being Element of NAT holds S_{3}[n,Cvr1 . n]
from FUNCT_2:sch 3(A14);

for n being Nat holds Cvr1 . n is Covering of D . n,F

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 S_{4}[ 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 S_{4}[s,y]
;

consider SOS being Function of N0,NAT such that

A26: for s being Element of N0 holds S_{4}[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 ) )

(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)

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)

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;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

k + 1 in { s where s is Element of NAT : (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s }
;
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;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

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: S

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 S

defpred S

A4: for n being Element of NAT ex y being Element of Funcs (NAT,(bool X)) st S

proof

consider Cvr0 being sequence of (Funcs (NAT,(bool X))) such that
let n be Element of NAT ; :: thesis: ex y being Element of Funcs (NAT,(bool X)) st S_{2}[n,y]

_{2}[n,y] )
by FUNCOP_1:7;

hence ex y being Element of Funcs (NAT,(bool X)) st S_{2}[n,y]
by A5; :: thesis: verum

end;A5: now :: thesis: ( n = (pr1 InvPairFunc) . (k + 1) implies ex y being Element of Funcs (NAT,(bool X)) st S_{2}[n,y] )

( n <> (pr1 InvPairFunc) . (k + 1) implies Sreconsider 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 S_{2}[n,y]

take y = y; :: thesis: S_{2}[n,y]

thus S_{2}[n,y]
by A6; :: thesis: verum

end;assume A6: n = (pr1 InvPairFunc) . (k + 1) ; :: thesis: ex y being Element of Funcs (NAT,(bool X)) st S

take y = y; :: thesis: S

thus S

hence ex y being Element of Funcs (NAT,(bool X)) st S

A7: for n being Element of NAT holds S

A8: for n being Nat holds Cvr0 . n is Covering of D . n,F

proof

A14:
for n being Element of NAT ex y being Element of Funcs (NAT,(bool X)) st S
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

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;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

then A13:
FSets0 is Set_Sequence of F
by Def2;
let s be Nat; :: thesis: FSets0 . s in F

A11: s 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;A11: s in NAT by ORDINAL1:def 12;

A12: now :: thesis: ( n = (pr1 InvPairFunc) . (k + 1) implies FSets0 . s in F )

n in NAT
by ORDINAL1:def 12;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;then FSets0 . s = (Cvr . n) . s by A7, A9, A11;

hence FSets0 . s in F ; :: thesis: verum

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

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

proof

consider Cvr1 being sequence of (Funcs (NAT,(bool X))) such that
let n be Element of NAT ; :: thesis: ex y being Element of Funcs (NAT,(bool X)) st S_{3}[n,y]

_{3}[n,y] )
by FUNCOP_1:7;

hence ex y being Element of Funcs (NAT,(bool X)) st S_{3}[n,y]
by A15; :: thesis: verum

end;A15: now :: thesis: ( n <> (pr1 InvPairFunc) . (k + 1) implies ex y being Element of Funcs (NAT,(bool X)) st S_{3}[n,y] )

( n = (pr1 InvPairFunc) . (k + 1) implies Sreconsider 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 S_{3}[n,y]

take y = y; :: thesis: S_{3}[n,y]

thus S_{3}[n,y]
by A16; :: thesis: verum

end;assume A16: n <> (pr1 InvPairFunc) . (k + 1) ; :: thesis: ex y being Element of Funcs (NAT,(bool X)) st S

take y = y; :: thesis: S

thus S

hence ex y being Element of Funcs (NAT,(bool X)) st S

A17: for n being Element of NAT holds S

for n being Nat holds Cvr1 . n is Covering of D . n,F

proof

then reconsider Cvr1 = Cvr1 as Covering of D,F by Def4;
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

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;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

then A23:
FSets1 is Set_Sequence of F
by Def2;
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;

hence FSets1 . s in F by A22, PROB_1:4; :: thesis: verum

end;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 )

( n = (pr1 InvPairFunc) . (k + 1) implies FSets1 . s = {} )
by A17, A18, A20;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;then FSets1 . s = (Cvr . n) . s by A17, A18, A21, A20;

hence FSets1 . s in F ; :: thesis: verum

hence FSets1 . s in F by A22, PROB_1:4; :: thesis: verum

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

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 S

A25: for s being Element of N0 ex y being Element of NAT st S

consider SOS being Function of N0,NAT such that

A26: for s being Element of N0 holds S

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 )

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;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

assume
not s in N0
; :: thesis: (vol (M,(On Cvr0))) . s = 0
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 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

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

now :: thesis: for s1, s2 being object st s1 in N0 & s2 in N0 & SOS . s1 = SOS . s2 holds

s1 = s2

then A35:
SOS is one-to-one
by FUNCT_2:19;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;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

(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

( vol (M,(On Cvr0)) is nonnegative & vol (M,(On Cvr1)) is nonnegative )
by Th4;
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;

end;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) )
;

end;

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;.= {} 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

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;.= {} 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

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

then
(Ser (Volume (M,Cvr))) . m = ((Ser (Volume (M,Cvr0))) . m) + ((Ser (Volume (M,Cvr1))) . m)
by A37, A42, MEASURE7:3;
let n be Element of NAT ; :: thesis: (Volume (M,Cvr)) . n = ((Volume (M,Cvr0)) . n) + ((Volume (M,Cvr1)) . n)

hence (Volume (M,Cvr)) . n = ((Volume (M,Cvr0)) . n) + ((Volume (M,Cvr1)) . n) by A56, A53, Def6; :: thesis: verum

end;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.

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 )

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;for s being Element of NAT holds (vol (M,(Cvr0 . n))) . s = 0.

proof

then A55:
SUM (vol (M,(Cvr0 . n))) = 0.
by MEASURE7:1;
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;(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

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

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;
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;( (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

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

A56: now :: thesis: ( n = (pr1 InvPairFunc) . (k + 1) implies SUM (vol (M,(Cvr . n))) = (SUM (vol (M,(Cvr0 . n)))) + (SUM (vol (M,(Cvr1 . n)))) )

( (Volume (M,Cvr)) . n = SUM (vol (M,(Cvr . n))) & (Volume (M,Cvr0)) . n = SUM (vol (M,(Cvr0 . n))) )
by Def6;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

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 )

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;for s being Element of NAT holds (vol (M,(Cvr1 . n))) . s = 0

proof

then A58:
SUM (vol (M,(Cvr1 . n))) = 0
by MEASURE7:1;
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;(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

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

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;
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;(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

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

hence (Volume (M,Cvr)) . n = ((Volume (M,Cvr0)) . n) + ((Volume (M,Cvr1)) . n) by A56, A53, Def6; :: thesis: verum

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

proof

thus
for k being Nat holds S
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;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