let X be non empty set ; :: thesis:
let F be Field_Subset of X; :: thesis:
let m be Measure of F; :: thesis:
A1: F c= sigma F by PROB_1:def 9;
assume m is completely-additive ; :: thesis:
then consider M1 being sigma_Measure of (sigma F) such that
A2: M1 is_extension_of m and
A3: M1 = (sigma_Meas (C_Meas m)) | (sigma F) by Th33;
assume ex Aseq being Set_Sequence of F st
( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) ; :: thesis:
then consider Aseq being Set_Sequence of F such that
A4: for n being Nat holds m . (Aseq . n) < +infty and
A5: X = union (rng Aseq) ;
let M be sigma_Measure of (sigma F); :: thesis:
reconsider Bseq = Partial_Union Aseq as Set_Sequence of F by Th15;
assume A6: M is_extension_of m ; :: thesis:
F c= sigma_Field (C_Meas m) by Th20;
then A7: sigma F c= sigma_Field (C_Meas m) by PROB_1:def 9;
A8: for B being Subset of X st B in sigma F holds
M . B <= M1 . B

proof

let B be Subset of X; :: thesis:
assume A9: B in sigma F ; :: thesis:
A10: for seq being Covering of B,F holds M . B <= SUM (vol (m,seq))

proof

let seq be Covering of B,F; :: thesis:
A11: for n being Element of NAT holds seq . n in sigma F by A1;

now :: thesis:

let y be object ; :: thesis:
assume y in rng seq ; :: thesis:
then consider x being object such that
A12: x in NAT and
A13: seq . x = y by FUNCT_2:11;
thus y in sigma F by A11, A12, A13; :: thesis:

end;

then rng seq c= sigma F ;
then reconsider seq1 = seq as SetSequence of sigma F by RELAT_1:def 19;
A14: rng seq1 c= sigma F ;
then reconsider Fseq = seq1 as sequence of (sigma F) by FUNCT_2:6;
B c= union (rng seq1) by Def3;
then ( Union seq1 in sigma F & B c= Union seq1 ) by CARD_3:def 4, PROB_1:17;
then A15: M . B <= M . (Union seq1) by A9, MEASURE1:31;
for n being object st n in NAT holds
(M * Fseq) . n = (vol (m,seq)) . n

proof

let n be object ; :: thesis:
assume A16: n in NAT ; :: thesis:
then reconsider n1 = n as Element of NAT ;
n1 in dom Fseq by A16, FUNCT_2:def 1;
then (M * Fseq) . n = M . (Fseq . n1) by FUNCT_1:13
.= m . (seq . n1) by A6 ;
hence (M * Fseq) . n = (vol (m,seq)) . n by Def5; :: thesis:

end;

then A17: SUM (M * Fseq) = SUM (vol (m,seq)) by FUNCT_2:12;
rng Fseq is N_Sub_set_fam of X by MEASURE1:23;
then rng Fseq is N_Measure_fam of sigma F by A14, MEASURE2:def 1;
then M . (union (rng Fseq)) <= SUM (M * Fseq) by MEASURE2:11;
then M . (Union seq1) <= SUM (vol (m,seq)) by A17, CARD_3:def 4;
hence M . B <= SUM (vol (m,seq)) by A15, XXREAL_0:2; :: thesis:

end;

for r being ExtReal st r in Svc (m,B) holds
M . B <= r

proof

let r be ExtReal; :: thesis:
assume r in Svc (m,B) ; :: thesis:
then ex seq being Covering of B,F st r = SUM (vol (m,seq)) by Def7;
hence M . B <= r by A10; :: thesis:

end;

then M . B is LowerBound of Svc (m,B) by XXREAL_2:def 2;
then M . B <= inf (Svc (m,B)) by XXREAL_2:def 4;
then M . B <= (C_Meas m) . B by Def8;
then M . B <= (sigma_Meas (C_Meas m)) . B by A7, A9, MEASURE4:def 3;
hence M . B <= M1 . B by A3, A9, FUNCT_1:49; :: thesis:

end;

A18: for B being set st ex k being Element of NAT st B c= Bseq . k & B in sigma F holds
M . B = M1 . B

proof

let B be set ; :: thesis:
assume ex k being Element of NAT st B c= Bseq . k ; :: thesis:
then consider k being Element of NAT such that
A19: B c= Bseq . k ;
A20: M . (Bseq . k) = m . (Bseq . k) by A6;
assume A21: B in sigma F ; :: thesis:
then reconsider B9 = B as Subset of X ;
A22: ( F c= sigma F & Bseq . k in F ) by PROB_1:def 9;
then A23: (Bseq . k) \ B is Element of sigma F by A21, PROB_1:6;
then M . ((Bseq . k) \ B) <= M . (Bseq . k) by A22, MEASURE1:31, XBOOLE_1:36;
then A24: M . ((Bseq . k) \ B) < +infty by A4, A20, Th34, XXREAL_0:2;
(M . B) + (M . ((Bseq . k) \ B)) = M . (B \/ ((Bseq . k) \ B)) by A21, A23, MEASURE1:30, XBOOLE_1:79;
then (M . B) + (M . ((Bseq . k) \ B)) = M . ((Bseq . k) \/ B) by XBOOLE_1:39;
then A25: (M . B) + (M . ((Bseq . k) \ B)) = M . (Bseq . k) by A19, XBOOLE_1:12;
0 <= M . ((Bseq . k) \ B) by SUPINF_2:51;
then A26: M . B = (M . (Bseq . k)) - (M . ((Bseq . k) \ B)) by A25, A24, XXREAL_3:28;
A27: M1 . (Bseq . k) = m . (Bseq . k) by A2;
(M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . (B \/ ((Bseq . k) \ B)) by A21, A23, MEASURE1:30, XBOOLE_1:79;
then (M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . ((Bseq . k) \/ B) by XBOOLE_1:39;
then A28: (M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . (Bseq . k) by A19, XBOOLE_1:12;
M1 . ((Bseq . k) \ B) <= M1 . (Bseq . k) by A22, A23, MEASURE1:31, XBOOLE_1:36;
then A29: M1 . ((Bseq . k) \ B) < +infty by A4, A27, Th34, XXREAL_0:2;
0 <= M1 . ((Bseq . k) \ B) by SUPINF_2:51;
then A30: M1 . B = (M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B)) by A28, A29, XXREAL_3:28;
M . ((Bseq . k) \ B) <= M1 . ((Bseq . k) \ B) by A8, A21, A22, PROB_1:6;
then A31: (M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B)) <= (M . (Bseq . k)) - (M . ((Bseq . k) \ B)) by A27, A20, XXREAL_3:37;
M . B9 <= M1 . B9 by A8, A21;
hence M . B = M1 . B by A26, A30, A31, XXREAL_0:1; :: thesis:

end;

for B being object st B in sigma F holds
M . B = M1 . B

proof

let B be object ; :: thesis:
assume A32: B in sigma F ; :: thesis:
then reconsider B9 = B as Subset of X ;
deffunc H₁( object ) -> Element of bool X = B9 /\ (Bseq . $1);
A33: for n being object st n in NAT holds
H₁(n) in bool X ;
consider Cseq being sequence of (bool X) such that
A34: for n being object st n in NAT holds
Cseq . n = H₁(n) from FUNCT_2:sch 2(A33);
reconsider Cseq = Cseq as SetSequence of X ;
for n, m being Nat st n <= m holds
Cseq . n c= Cseq . m

proof

let n, m be Nat; :: thesis:
A35: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
A36: Bseq is non-descending by PROB_3:11;
assume n <= m ; :: thesis:
then Bseq . n c= Bseq . m by A36, PROB_1:def 5;
then B9 /\ (Bseq . n) c= B9 /\ (Bseq . m) by XBOOLE_1:26;
then Cseq . n c= B9 /\ (Bseq . m) by A34, A35;
hence Cseq . n c= Cseq . m by A34, A35; :: thesis:

end;

then A37: Cseq is non-descending by PROB_1:def 5;

now :: thesis:

let y be object ; :: thesis:
assume y in rng Cseq ; :: thesis:
then consider x being object such that
A38: x in NAT and
A39: Cseq . x = y by FUNCT_2:11;
reconsider x = x as Element of NAT by A38;
Bseq . x in F ;
then (Bseq . x) /\ B9 in sigma F by A1, A32, MEASURE1:34;
hence y in sigma F by A34, A39; :: thesis:

end;

then rng Cseq c= sigma F ;
then reconsider Cseq = Cseq as SetSequence of sigma F by RELAT_1:def 19;
for n being object st n in NAT holds
(M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n

proof

let n be object ; :: thesis:
assume A40: n in NAT ; :: thesis:
then reconsider n1 = n as Nat ;

A41: now :: thesis:

let x be set ; :: thesis:
assume x in (Partial_Union Cseq) . n1 ; :: thesis:
then consider k being Nat such that
A42: k <= n1 and
A43: x in Cseq . k by PROB_3:13;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
take k = k; :: thesis:
x in B9 /\ (Bseq . k) by A34, A43;
hence ( k <= n1 & x in Bseq . k ) by A42, XBOOLE_0:def 4; :: thesis:

end;

A44: (Partial_Union Cseq) . n1 c= Bseq . n1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in (Partial_Union Cseq) . n1 ; :: thesis:
then consider k being Element of NAT such that
A45: k <= n1 and
A46: x in Bseq . k by A41;
Bseq is non-descending by PROB_3:11;
then Bseq . k c= Bseq . n1 by A45, PROB_1:def 5;
hence x in Bseq . n1 by A46; :: thesis:

end;

A47: (M1 * (Partial_Union Cseq)) . n = M1 . ((Partial_Union Cseq) . n1) by FUNCT_2:15, A40;
A48: rng (Partial_Union Cseq) c= sigma F by RELAT_1:def 19;
dom (Partial_Union Cseq) = NAT by PARTFUN1:def 2;
then (Partial_Union Cseq) . n1 in rng (Partial_Union Cseq) by FUNCT_1:3, A40;
then (M1 * (Partial_Union Cseq)) . n = M . ((Partial_Union Cseq) . n1) by A47, A18, A44, A48, A40;
hence (M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n by FUNCT_2:15, A40; :: thesis:

end;

then A49: M1 * (Partial_Union Cseq) = M * (Partial_Union Cseq) by FUNCT_2:12;
for n being Nat holds Cseq . n = B9 /\ (Bseq . n) by ORDINAL1:def 12, A34;
then Cseq = B9 (/\) Bseq by SETLIM_2:def 5;
then Union Cseq = B9 /\ (Union Bseq) by SETLIM_2:38;
then Union Cseq = B9 /\ (Union Aseq) by PROB_3:15;
then Union Cseq = B9 /\ X by A5, CARD_3:def 4;
then A50: B9 = Union Cseq by XBOOLE_1:28;
then B9 = lim Cseq by A37, SETLIM_1:63;
then M1 . B = lim (M1 * Cseq) by A37, Th26;
then M1 . B = lim (M * (Partial_Union Cseq)) by A37, A49, PROB_4:19;
then M1 . B = lim (M * Cseq) by A37, PROB_4:19;
then M1 . B = M . (lim Cseq) by A37, Th26;
hence M1 . B = M . B by A37, A50, SETLIM_1:63; :: thesis:

end;

hence M = (sigma_Meas (C_Meas m)) | (sigma F) by A3, FUNCT_2:12; :: thesis: