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) )
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
A1: ( M1 is_extension_of m & M1 = (sigma_Meas (C_Meas m)) | (sigma F) ) by Th91b;
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
A2: ( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) ;
reconsider Bseq = Partial_Union Aseq as Set_Sequence of F by Lem06;
let M be sigma_Measure of (sigma F); :: thesis: ( M is_extension_of m implies M = (sigma_Meas (C_Meas m)) | (sigma F) )
assume A3: M is_extension_of m ; :: thesis: M = (sigma_Meas (C_Meas m)) | (sigma F)
F c= sigma_Field (C_Meas m) by Th52;
then PP2: ( F c= sigma F & sigma F c= sigma_Field (C_Meas m) ) by PROB_1:def 14;
P1: 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 PP0: B in sigma F ; :: thesis: M . B <= M1 . B
PP4: 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)

PP7: now

let n be Element of NAT ; :: thesis: seq . n in sigma F
seq . n in F ;
hence seq . n in sigma F by PP2; :: 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
PPX: ( x in NAT & seq . x = y ) by FUNCT_2:17;
reconsider x = x as Element of NAT by PPX;
thus y in sigma F by PP7, PPX; :: thesis: verum

end;

then rng seq c= sigma F by TARSKI:def 3;
then reconsider seq1 = seq as SetSequence of by RELAT_1:def 19;
PP5: Union seq1 in sigma F by PROB_1:46;
B c= union (rng seq1) by Def2;
then B c= Union seq1 by CARD_3:def 4;
then PQ3: M . B <= M . (Union seq1) by PP0, PP5, MEASURE1:62;

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
PP6: ( x in NAT & seq1 . x = y ) by FUNCT_2:17;
reconsider x = x as Element of NAT by PP6;
thus y in sigma F by PP6, PP7; :: thesis: verum

end;

then PP8: rng seq1 c= sigma F by TARSKI:def 3;
then reconsider Fseq = seq1 as Function of NAT ,(sigma F) by FUNCT_2:8;
rng Fseq is N_Sub_set_fam of X by MEASURE1:52;
then rng Fseq is N_Measure_fam of sigma F by PP8, MEASURE2:def 1;
then PQ2: M . (union (rng Fseq)) <= SUM (M * Fseq) by MEASURE2:13;
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 PQ0: n in NAT ; :: thesis: (M * Fseq) . n = (vol m,seq) . n
then reconsider n1 = n as Element of NAT ;
n1 in dom Fseq by PQ0, FUNCT_2:def 1;
then (M * Fseq) . n = M . (Fseq . n1) by FUNCT_1:23
.= m . (seq . n1) by A3, DDef2 ;
hence (M * Fseq) . n = (vol m,seq) . n by Def4; :: thesis: verum

end;

then SUM (M * Fseq) = SUM (vol m,seq) by FUNCT_2:18;
then M . (Union seq1) <= SUM (vol m,seq) by PQ2, CARD_3:def 4;
hence M . B <= SUM (vol m,seq) by PQ3, 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 Def8;
hence M . B <= r by PP4; :: 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 Def10;
then M . B <= (sigma_Meas (C_Meas m)) . B by PP0, PP2, MEASURE4:def 4;
hence M . B <= M1 . B by A1, PP0, FUNCT_1:72; :: thesis: verum

end;

P2: 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
PP1: B c= Bseq . k ;
assume PP2: B in sigma F ; :: thesis: M . B = M1 . B
then reconsider B' = B as Subset of X ;
X in sigma F by PROB_1:43;
then PP3: ( M . B' <= M1 . B' & M . (X \ B') <= M1 . (X \ B') ) by PP2, P1, PROB_1:44;
PP4: F c= sigma F by PROB_1:def 14;
PP8: Bseq . k in F ;
PP5: ( M1 . (Bseq . k) = m . (Bseq . k) & M . (Bseq . k) = m . (Bseq . k) ) by A1, A3, DDef2;
PQ2: (Bseq . k) \ B is Element of sigma F by PP8, PP4, PP2, PROB_1:12;
then ( (M . B) + (M . ((Bseq . k) \ B)) = M . (B \/ ((Bseq . k) \ B)) & (M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . (B \/ ((Bseq . k) \ B)) ) by PP2, MEASURE1:61, XBOOLE_1:79;
then ( (M . B) + (M . ((Bseq . k) \ B)) = M . ((Bseq . k) \/ B) & (M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . ((Bseq . k) \/ B) ) by XBOOLE_1:39;
then PQ6: ( (M . B) + (M . ((Bseq . k) \ B)) = M . (Bseq . k) & (M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . (Bseq . k) ) by PP1, XBOOLE_1:12;
PQ4: ( M . ((Bseq . k) \ B) <= M . (Bseq . k) & M1 . ((Bseq . k) \ B) <= M1 . (Bseq . k) ) by PP8, PP4, PQ2, XBOOLE_1:36, MEASURE1:62;
X: ( M . ((Bseq . k) \ B) < +infty & M1 . ((Bseq . k) \ B) < +infty ) by PQ4, PP5, A2, Lem10, XXREAL_0:2;
( 0 <= M . ((Bseq . k) \ B) & 0 <= M1 . ((Bseq . k) \ B) ) by SUPINF_2:70;
then PQ7: ( M . B = (M . (Bseq . k)) - (M . ((Bseq . k) \ B)) & M1 . B = (M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B)) ) by PQ6, XXREAL_3:29, X;
M . ((Bseq . k) \ B) <= M1 . ((Bseq . k) \ B) by PP8, PP4, P1, PP2, PROB_1:12;
then (M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B)) <= (M . (Bseq . k)) - (M . ((Bseq . k) \ B)) by PP5, XXREAL_3:39;
hence M . B = M1 . B by PP3, PQ7, 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 )
assume D1: B in sigma F ; :: thesis: M . B = M1 . B
then reconsider B' = B as Subset of X ;
deffunc H₁( set ) -> set = B /\ (Bseq . $1);
D5: 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 DDef4;
then (Bseq . n) /\ B c= X /\ X by D1, XBOOLE_1:27;
hence H₁(n) in bool X ; :: thesis: verum

end;

consider Cseq being Function of NAT ,(bool X) such that
D6: for n being set st n in NAT holds
Cseq . n = H₁(n) from FUNCT_2:sch 2(D5);
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 )
assume E11: n <= m ; :: thesis: Cseq . n c= Cseq . m
Bseq is non-descending by PROB_3:13;
then Bseq . n c= Bseq . m by E11, PROB_1:def 7;
then B /\ (Bseq . n) c= B /\ (Bseq . m) by XBOOLE_1:26;
then Cseq . n c= B /\ (Bseq . m) by D6;
hence Cseq . n c= Cseq . m by D6; :: thesis: verum

end;

then L1: 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
L2: ( x in NAT & Cseq . x = y ) by FUNCT_2:17;
reconsider x = x as Element of NAT by L2;
Bseq . x in F ;
then (Bseq . x) /\ B in sigma F by D1, PP2, MEASURE1:66;
hence y in sigma F by D6, L2; :: thesis: verum

end;

then rng Cseq c= sigma F by TARSKI:def 3;
then reconsider Cseq = Cseq as SetSequence of by RELAT_1:def 19;
for n being Element of NAT holds Cseq . n = B' /\ (Bseq . n) by D6;
then Cseq = B' (/\) Bseq by SETLIM_2:def 5;
then Union Cseq = B' /\ (Union Bseq) by SETLIM_2:38;
then Union Cseq = B' /\ (Union Aseq) by PROB_3:17;
then Union Cseq = B' /\ X by A2, CARD_3:def 4;
then F3: B' = Union Cseq by XBOOLE_1:28;
then B' = lim Cseq by L1, SETLIM_1:63;
then F2: M1 . B = lim (M1 * Cseq) by L1, Th62a;
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 ;
K1: (M1 * (@Partial_Union Cseq)) . n = M1 . ((@Partial_Union Cseq) . n1) by FUNCT_2:21;

K5: 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
K4: ( k <= n1 & 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 K4, D6;
hence ( k <= n1 & x in Bseq . k ) by K4, 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
K6: ( k <= n1 & x in Bseq . k ) by K5;
Bseq is non-descending by PROB_3:13;
then Bseq . k c= Bseq . n1 by K6, PROB_1:def 7;
hence x in Bseq . n1 by K6; :: thesis: verum

end;

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

end;

then M1 * (@Partial_Union Cseq) = M * (@Partial_Union Cseq) by FUNCT_2:18;
then M1 . B = lim (M * (@Partial_Union Cseq)) by F2, L1, PROB_4:20;
then M1 . B = lim (M * Cseq) by L1, PROB_4:20;
then M1 . B = M . (lim Cseq) by L1, Th62a;
hence M1 . B = M . B by F3, L1, SETLIM_1:63; :: thesis: verum

end;

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