let X be non empty set ; :: thesis: for F being Field_Subset of X
for m being Measure of F st m is completely-additive & ex Aseq being Set_Sequence of F st
( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) holds
for M being sigma_Measure of (sigma F) st M is_extension_of m holds
M = (sigma_Meas (C_Meas m)) | (sigma F)
let F be Field_Subset of X; :: thesis: for m being Measure of F st m is completely-additive & ex Aseq being Set_Sequence of F st
( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) holds
for M being sigma_Measure of (sigma F) st M is_extension_of m holds
M = (sigma_Meas (C_Meas m)) | (sigma F)
let m be Measure of F; :: thesis: ( m is completely-additive & ex Aseq being Set_Sequence of F st
( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) implies for M being sigma_Measure of (sigma F) st M is_extension_of m holds
M = (sigma_Meas (C_Meas m)) | (sigma F) )
A1: F c= sigma F by PROB_1:def 14;
assume m is completely-additive ; :: thesis: ( for Aseq being Set_Sequence of F holds
( ex n being Nat st not m . (Aseq . n) < +infty or not X = union (rng Aseq) ) or for M being sigma_Measure of (sigma F) st M is_extension_of m holds
M = (sigma_Meas (C_Meas m)) | (sigma F) )
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: for M being sigma_Measure of (sigma F) st M is_extension_of m holds
M = (sigma_Meas (C_Meas m)) | (sigma F)
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: ( M is_extension_of m implies M = (sigma_Meas (C_Meas m)) | (sigma F) )
reconsider Bseq = Partial_Union Aseq as Set_Sequence of F by Th15;
assume A6: M is_extension_of m ; :: thesis: M = (sigma_Meas (C_Meas m)) | (sigma F)
F c= sigma_Field (C_Meas m) by Th20;
then A7: sigma F c= sigma_Field (C_Meas m) by PROB_1:def 14;
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: ( B in sigma F implies M . B <= M1 . B )
assume A9: B in sigma F ; :: thesis: M . B <= M1 . B
A10: for seq being Covering of B,F holds M . B <= SUM (vol m,seq)

proof

let seq be Covering of B,F; :: thesis: M . B <= SUM (vol m,seq)

A11: now

let n be Element of NAT ; :: thesis: seq . n in sigma F
seq . n in F ;
hence seq . n in sigma F by A1; :: thesis: verum

end;

now

let y be set ; :: thesis: ( y in rng seq implies y in sigma F )
assume y in rng seq ; :: thesis: y in sigma F
then consider x being set such that
A12: x in NAT and
A13: seq . x = y by FUNCT_2:17;
thus y in sigma F by A11, A12, A13; :: thesis: verum
reconsider x = x as Element of NAT by A12;

end;

then rng seq c= sigma F by TARSKI:def 3;
then reconsider seq1 = seq as SetSequence of sigma F by RELAT_1:def 19;

now

let y be set ; :: thesis: ( y in rng seq1 implies y in sigma F )
assume y in rng seq1 ; :: thesis: y in sigma F
then consider x being set such that
A14: x in NAT and
A15: seq1 . x = y by FUNCT_2:17;
thus y in sigma F by A11, A14, A15; :: thesis: verum
reconsider x = x as Element of NAT by A14;

end;

then A16: rng seq1 c= sigma F by TARSKI:def 3;
then reconsider Fseq = seq1 as Function of NAT ,(sigma F) by FUNCT_2:8;
B c= union (rng seq1) by Def3;
then ( Union seq1 in sigma F & B c= Union seq1 ) by CARD_3:def 4, PROB_1:46;
then A17: M . B <= M . (Union seq1) by A9, MEASURE1:62;
for n being set st n in NAT holds
(M * Fseq) . n = (vol m,seq) . n

proof

let n be set ; :: thesis: ( n in NAT implies (M * Fseq) . n = (vol m,seq) . n )
assume A18: n in NAT ; :: thesis: (M * Fseq) . n = (vol m,seq) . n
then reconsider n1 = n as Element of NAT ;
n1 in dom Fseq by A18, FUNCT_2:def 1;
then (M * Fseq) . n = M . (Fseq . n1) by FUNCT_1:23
.= m . (seq . n1) by A6, Def12 ;
hence (M * Fseq) . n = (vol m,seq) . n by Def5; :: thesis: verum

end;

then A19: SUM (M * Fseq) = SUM (vol m,seq) by FUNCT_2:18;
rng Fseq is N_Sub_set_fam of X by MEASURE1:52;
then rng Fseq is N_Measure_fam of sigma F by A16, MEASURE2:def 1;
then M . (union (rng Fseq)) <= SUM (M * Fseq) by MEASURE2:13;
then M . (Union seq1) <= SUM (vol m,seq) by A19, CARD_3:def 4;
hence M . B <= SUM (vol m,seq) by A17, XXREAL_0:2; :: thesis: verum

end;

for r being ext-real number st r in Svc m,B holds
M . B <= r

proof

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

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 4;
hence M . B <= M1 . B by A3, A9, FUNCT_1:72; :: thesis: verum

end;

A20: 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: ( ex k being Element of NAT st B c= Bseq . k & B in sigma F implies M . B = M1 . B )
assume ex k being Element of NAT st B c= Bseq . k ; :: thesis: ( not B in sigma F or M . B = M1 . B )
then consider k being Element of NAT such that
A21: B c= Bseq . k ;
A22: M . (Bseq . k) = m . (Bseq . k) by A6, Def12;
assume A23: B in sigma F ; :: thesis: M . B = M1 . B
then reconsider B9 = B as Subset of X ;
A24: ( F c= sigma F & Bseq . k in F ) by PROB_1:def 14;
then A25: (Bseq . k) \ B is Element of sigma F by A23, PROB_1:12;
then M . ((Bseq . k) \ B) <= M . (Bseq . k) by A24, MEASURE1:62, XBOOLE_1:36;
then A26: M . ((Bseq . k) \ B) < +infty by A4, A22, Th34, XXREAL_0:2;
(M . B) + (M . ((Bseq . k) \ B)) = M . (B \/ ((Bseq . k) \ B)) by A23, A25, MEASURE1:61, XBOOLE_1:79;
then (M . B) + (M . ((Bseq . k) \ B)) = M . ((Bseq . k) \/ B) by XBOOLE_1:39;
then A27: (M . B) + (M . ((Bseq . k) \ B)) = M . (Bseq . k) by A21, XBOOLE_1:12;
0 <= M . ((Bseq . k) \ B) by SUPINF_2:70;
then A28: M . B = (M . (Bseq . k)) - (M . ((Bseq . k) \ B)) by A27, A26, XXREAL_3:29;
A29: M1 . (Bseq . k) = m . (Bseq . k) by A2, Def12;
(M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . (B \/ ((Bseq . k) \ B)) by A23, A25, MEASURE1:61, XBOOLE_1:79;
then (M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . ((Bseq . k) \/ B) by XBOOLE_1:39;
then A30: (M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . (Bseq . k) by A21, XBOOLE_1:12;
M1 . ((Bseq . k) \ B) <= M1 . (Bseq . k) by A24, A25, MEASURE1:62, XBOOLE_1:36;
then A31: M1 . ((Bseq . k) \ B) < +infty by A4, A29, Th34, XXREAL_0:2;
0 <= M1 . ((Bseq . k) \ B) by SUPINF_2:70;
then A32: M1 . B = (M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B)) by A30, A31, XXREAL_3:29;
M . ((Bseq . k) \ B) <= M1 . ((Bseq . k) \ B) by A8, A23, A24, PROB_1:12;
then A33: (M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B)) <= (M . (Bseq . k)) - (M . ((Bseq . k) \ B)) by A29, A22, XXREAL_3:39;
M . B9 <= M1 . B9 by A8, A23;
hence M . B = M1 . B by A28, A32, A33, XXREAL_0:1; :: thesis: verum

end;

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

proof

let B be set ; :: thesis: ( B in sigma F implies M . B = M1 . B )
deffunc H₁( set ) -> set = B /\ (Bseq . $1);
assume A34: B in sigma F ; :: thesis: M . B = M1 . B
then reconsider B9 = B as Subset of X ;
A35: for n being set st n in NAT holds
H₁(n) in bool X

proof

let n be set ; :: thesis: ( n in NAT implies H₁(n) in bool X )
assume n in NAT ; :: thesis: H₁(n) in bool X
then Bseq . n in F by Def2;
then (Bseq . n) /\ B c= X /\ X by A34, XBOOLE_1:27;
hence H₁(n) in bool X ; :: thesis: verum

end;

consider Cseq being Function of NAT ,(bool X) such that
A36: for n being set st n in NAT holds
Cseq . n = H₁(n) from FUNCT_2:sch 2(A35);
reconsider Cseq = Cseq as SetSequence of X ;
for n, m being Element of NAT st n <= m holds
Cseq . n c= Cseq . m

proof

let n, m be Element of NAT ; :: thesis: ( n <= m implies Cseq . n c= Cseq . m )
A37: Bseq is non-descending by PROB_3:13;
assume n <= m ; :: thesis: Cseq . n c= Cseq . m
then Bseq . n c= Bseq . m by A37, PROB_1:def 7;
then B /\ (Bseq . n) c= B /\ (Bseq . m) by XBOOLE_1:26;
then Cseq . n c= B /\ (Bseq . m) by A36;
hence Cseq . n c= Cseq . m by A36; :: thesis: verum

end;

then A38: Cseq is non-descending by PROB_1:def 7;

now

let y be set ; :: thesis: ( y in rng Cseq implies y in sigma F )
assume y in rng Cseq ; :: thesis: y in sigma F
then consider x being set such that
A39: x in NAT and
A40: Cseq . x = y by FUNCT_2:17;
reconsider x = x as Element of NAT by A39;
Bseq . x in F ;
then (Bseq . x) /\ B in sigma F by A1, A34, MEASURE1:66;
hence y in sigma F by A36, A40; :: thesis: verum

end;

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

proof

let n be set ; :: thesis: ( n in NAT implies (M1 * (@Partial_Union Cseq)) . n = (M * (@Partial_Union Cseq)) . n )
assume n in NAT ; :: thesis: (M1 * (@Partial_Union Cseq)) . n = (M * (@Partial_Union Cseq)) . n
then reconsider n1 = n as Element of NAT ;

A41: now

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

end;

now

let x be set ; :: thesis: ( x in (@Partial_Union Cseq) . n1 implies x in Bseq . n1 )
assume x in (@Partial_Union Cseq) . n1 ; :: thesis: x in Bseq . n1
then consider k being Element of NAT such that
A44: k <= n1 and
A45: x in Bseq . k by A41;
Bseq is non-descending by PROB_3:13;
then Bseq . k c= Bseq . n1 by A44, PROB_1:def 7;
hence x in Bseq . n1 by A45; :: thesis: verum

end;

then ( (M1 * (@Partial_Union Cseq)) . n = M1 . ((@Partial_Union Cseq) . n1) & (@Partial_Union Cseq) . n1 c= Bseq . n1 ) by FUNCT_2:21, TARSKI:def 3;
then (M1 * (@Partial_Union Cseq)) . n = M . ((@Partial_Union Cseq) . n1) by A20;
hence (M1 * (@Partial_Union Cseq)) . n = (M * (@Partial_Union Cseq)) . n by FUNCT_2:21; :: thesis: verum

end;

then A46: M1 * (@Partial_Union Cseq) = M * (@Partial_Union Cseq) by FUNCT_2:18;
for n being Element of NAT holds Cseq . n = B9 /\ (Bseq . n) by A36;
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:17;
then Union Cseq = B9 /\ X by A5, CARD_3:def 4;
then A47: B9 = Union Cseq by XBOOLE_1:28;
then B9 = lim Cseq by A38, SETLIM_1:63;
then M1 . B = lim (M1 * Cseq) by A38, Th26;
then M1 . B = lim (M * (@Partial_Union Cseq)) by A38, A46, PROB_4:20;
then M1 . B = lim (M * Cseq) by A38, PROB_4:20;
then M1 . B = M . (lim Cseq) by A38, Th26;
hence M1 . B = M . B by A38, A47, SETLIM_1:63; :: thesis: verum

end;

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