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 () st M is_extension_of m holds
M = (sigma_Meas ()) | ()

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 () st M is_extension_of m holds
M = (sigma_Meas ()) | ()

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 () st M is_extension_of m holds
M = (sigma_Meas ()) | () )

A1: F c= sigma F by PROB_1:def 9;
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 () st M is_extension_of m holds
M = (sigma_Meas ()) | () )

then consider M1 being sigma_Measure of () such that
A2: M1 is_extension_of m and
A3: M1 = (sigma_Meas ()) | () 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 () st M is_extension_of m holds
M = (sigma_Meas ()) | ()

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 (); :: thesis: ( M is_extension_of m implies M = (sigma_Meas ()) | () )
reconsider Bseq = Partial_Union Aseq as Set_Sequence of F by Th15;
assume A6: M is_extension_of m ; :: thesis: M = (sigma_Meas ()) | ()
F c= sigma_Field () by Th20;
then A7: sigma F c= sigma_Field () 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: ( 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: for n being Element of NAT holds seq . n in sigma F by A1;
now :: thesis: for y being object st y in rng seq holds
y in sigma F
let y be object ; :: thesis: ( y in rng seq implies y in sigma F )
assume y in rng seq ; :: thesis: y in sigma F
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 ; :: thesis: verum
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 () by FUNCT_2:6;
B c= union (rng seq1) by Def3;
then ( Union seq1 in sigma F & B c= Union seq1 ) by ;
then A15: M . B <= M . (Union seq1) by ;
for n being object st n in NAT holds
(M * Fseq) . n = (vol (m,seq)) . n
proof
let n be object ; :: thesis: ( n in NAT implies (M * Fseq) . n = (vol (m,seq)) . n )
assume A16: n in NAT ; :: thesis: (M * Fseq) . n = (vol (m,seq)) . n
then reconsider n1 = n as Element of NAT ;
n1 in dom Fseq by ;
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: verum
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 ;
then M . (union (rng Fseq)) <= SUM (M * Fseq) by MEASURE2:11;
then M . (Union seq1) <= SUM (vol (m,seq)) by ;
hence M . B <= SUM (vol (m,seq)) by ; :: thesis: verum
end;
for r being ExtReal st r in Svc (m,B) holds
M . B <= r
proof
let r be ExtReal; :: 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 <= () . B by Def8;
then M . B <= (sigma_Meas ()) . B by ;
hence M . B <= M1 . B by ; :: thesis: verum
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: ( 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
A19: B c= Bseq . k ;
A20: M . (Bseq . k) = m . (Bseq . k) by A6;
assume A21: B in sigma F ; :: thesis: M . B = M1 . B
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 ;
then M . ((Bseq . k) \ B) <= M . (Bseq . k) by ;
then A24: M . ((Bseq . k) \ B) < +infty by ;
(M . B) + (M . ((Bseq . k) \ B)) = M . (B \/ ((Bseq . k) \ B)) by ;
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 ;
0 <= M . ((Bseq . k) \ B) by SUPINF_2:51;
then A26: M . B = (M . (Bseq . k)) - (M . ((Bseq . k) \ B)) by ;
A27: M1 . (Bseq . k) = m . (Bseq . k) by A2;
(M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . (B \/ ((Bseq . k) \ B)) by ;
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 ;
M1 . ((Bseq . k) \ B) <= M1 . (Bseq . k) by ;
then A29: M1 . ((Bseq . k) \ B) < +infty by ;
0 <= M1 . ((Bseq . k) \ B) by SUPINF_2:51;
then A30: M1 . B = (M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B)) by ;
M . ((Bseq . k) \ B) <= M1 . ((Bseq . k) \ B) by ;
then A31: (M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B)) <= (M . (Bseq . k)) - (M . ((Bseq . k) \ B)) by ;
M . B9 <= M1 . B9 by ;
hence M . B = M1 . B by ; :: thesis: verum
end;
for B being object st B in sigma F holds
M . B = M1 . B
proof
let B be object ; :: thesis: ( B in sigma F implies M . B = M1 . B )
assume A32: B in sigma F ; :: thesis: M . B = M1 . B
then reconsider B9 = B as Subset of X ;
deffunc H1( object ) -> Element of bool X = B9 /\ (Bseq . \$1);
A33: for n being object st n in NAT holds
H1(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 = H1(n) from 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: ( n <= m implies Cseq . n c= Cseq . m )
A35: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
A36: Bseq is non-descending by PROB_3:11;
assume n <= m ; :: thesis: Cseq . n c= Cseq . m
then Bseq . n c= Bseq . m by ;
then B9 /\ (Bseq . n) c= B9 /\ (Bseq . m) by XBOOLE_1:26;
then Cseq . n c= B9 /\ (Bseq . m) by ;
hence Cseq . n c= Cseq . m by ; :: thesis: verum
end;
then A37: Cseq is non-descending by PROB_1:def 5;
now :: thesis: for y being object st y in rng Cseq holds
y in sigma F
let y be object ; :: thesis: ( y in rng Cseq implies y in sigma F )
assume y in rng Cseq ; :: thesis: y in sigma F
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 ;
hence y in sigma F by ; :: thesis: verum
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: ( n in NAT implies (M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n )
assume A40: n in NAT ; :: thesis: (M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n
then reconsider n1 = n as Nat ;
A41: now :: thesis: for x being set st x in (Partial_Union Cseq) . n1 holds
ex k being Element of NAT st
( k <= n1 & x in Bseq . k )
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:13;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
take k = k; :: thesis: ( k <= n1 & x in Bseq . k )
x in B9 /\ (Bseq . k) by ;
hence ( k <= n1 & x in Bseq . k ) by ; :: thesis: verum
end;
A44: (Partial_Union Cseq) . n1 c= Bseq . n1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Partial_Union Cseq) . n1 or 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
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 ;
hence x in Bseq . n1 by A46; :: thesis: verum
end;
A47: (M1 * (Partial_Union Cseq)) . n = M1 . ((Partial_Union Cseq) . n1) by ;
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 ;
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 ; :: thesis: verum
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 ;
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 ;
then A50: B9 = Union Cseq by XBOOLE_1:28;
then B9 = lim Cseq by ;
then M1 . B = lim (M1 * Cseq) by ;
then M1 . B = lim (M * (Partial_Union Cseq)) by ;
then M1 . B = lim (M * Cseq) by ;
then M1 . B = M . (lim Cseq) by ;
hence M1 . B = M . B by ; :: thesis: verum
end;
hence M = (sigma_Meas ()) | () by ; :: thesis: verum