let X be set ; :: thesis: for C being C_Measure of X holds sigma_Field C is SigmaField of X
let C be C_Measure of X; :: thesis: sigma_Field C is SigmaField of X
A1: C is nonnegative by Def1;
A2: for M being N_Sub_set_fam of X st M c= sigma_Field C holds
union M in sigma_Field C
proof
let M be N_Sub_set_fam of X; :: thesis: ( M c= sigma_Field C implies union M in sigma_Field C )
assume A3: M c= sigma_Field C ; :: thesis: union M in sigma_Field C
for W, Z being Subset of X st W c= union M & Z c= X \ (union M) holds
(C . W) + (C . Z) <= C . (W \/ Z)
proof
reconsider S = bool X as SigmaField of X by Th3;
let W, Z be Subset of X; :: thesis: ( W c= union M & Z c= X \ (union M) implies (C . W) + (C . Z) <= C . (W \/ Z) )
assume that
A4: W c= union M and
A5: Z c= X \ (union M) ; :: thesis: (C . W) + (C . Z) <= C . (W \/ Z)
consider F being sequence of (bool X) such that
A6: rng F = M by SUPINF_2:def 8;
consider G being sequence of S such that
A7: G . 0 = F . 0 and
A8: for n being Nat holds G . (n + 1) = (F . (n + 1)) \/ (G . n) by MEASURE2:4;
consider B being sequence of S such that
A9: B . 0 = F . 0 and
A10: for n being Nat holds B . (n + 1) = (F . (n + 1)) \ (G . n) by MEASURE2:8;
A11: union (rng F) = union (rng B) by A7, A8, A9, A10, Th2;
defpred S1[ Nat] means G . $1 in sigma_Field C;
A12: for n being Element of NAT holds F . n in sigma_Field C
proof
let n be Element of NAT ; :: thesis: F . n in sigma_Field C
F . n in M by A6, FUNCT_2:4;
hence F . n in sigma_Field C by A3; :: thesis: verum
end;
A13: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A14: G . k in sigma_Field C ; :: thesis: S1[k + 1]
A15: F . (k + 1) in sigma_Field C by A12;
G . (k + 1) = (F . (k + 1)) \/ (G . k) by A8;
hence S1[k + 1] by A14, A15, Th8; :: thesis: verum
end;
A16: S1[ 0 ] by A12, A7;
A17: for n being Nat holds S1[n] from NAT_1:sch 2(A16, A13);
 consider Q being sequence of S such that
A18: for n being Element of NAT holds Q . n = W /\ (B . n) by Th11;
A19: union (rng Q) = W /\ (union (rng B)) by A18, Th1;
consider QQ being sequence of S such that
A20: QQ . 0 = Q . 0 and
A21: for n being Nat holds QQ . (n + 1) = (Q . (n + 1)) \/ (QQ . n) by MEASURE2:4;
reconsider Q = Q, QQ = QQ, F = F, G = G as sequence of (bool X) ;
A22: F . 0 in sigma_Field C by A12;
defpred S2[ Nat] means C . (Z \/ (QQ . $1)) = (C . Z) + ((Ser (C * Q)) . $1);
A23: C * Q is nonnegative by A1, MEASURE1:25;
A24: for k being Nat st S2[k] holds
S2[k + 1]
proof
defpred S3[ Nat] means QQ . $1 c= G . $1;
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
A25: (F . (k + 1)) \ (G . k) c= F . (k + 1) by XBOOLE_1:36;
A26: QQ . (k + 1) = (QQ . k) \/ (Q . (k + 1)) by A21;
A27: G . k in sigma_Field C by A17;
F . (k + 1) in sigma_Field C by A12;
then A28: (F . (k + 1)) \ (G . k) in sigma_Field C by A27, Th10;
A29: 0. <= (C * Q) . (k + 1) by A23, SUPINF_2:39;
A30: 0. <= (Ser (C * Q)) . k by A23, SUPINF_2:40;
QQ . 0 = W /\ (F . 0) by A9, A18, A20;
then A31: S3[ 0 ] by A7, XBOOLE_1:17;
for n being Nat holds QQ . n misses (F . (n + 1)) \ (G . n)
proof
let n be Nat; :: thesis: QQ . n misses (F . (n + 1)) \ (G . n)
A32: for n being Nat st S3[n] holds
S3[n + 1]
proof
let n be Nat; :: thesis: ( S3[n] implies S3[n + 1] )
assume A33: QQ . n c= G . n ; :: thesis: S3[n + 1]
A34: W /\ (F . (n + 1)) c= F . (n + 1) by XBOOLE_1:17;
W /\ ((F . (n + 1)) \ (G . n)) c= W /\ (F . (n + 1)) by XBOOLE_1:26, XBOOLE_1:36;
then A35: W /\ ((F . (n + 1)) \ (G . n)) c= F . (n + 1) by A34;
QQ . (n + 1) = (Q . (n + 1)) \/ (QQ . n) by A21
.= (W /\ (B . (n + 1))) \/ (QQ . n) by A18
.= (W /\ ((F . (n + 1)) \ (G . n))) \/ (QQ . n) by A10 ;
then QQ . (n + 1) c= (F . (n + 1)) \/ (G . n) by A33, A35, XBOOLE_1:13;
hence S3[n + 1] by A8; :: thesis: verum
end;
A36: for n being Nat holds S3[n] from NAT_1:sch 2(A31, A32);
 G . n misses (F . (n + 1)) \ (G . n) by XBOOLE_1:79;
hence QQ . n misses (F . (n + 1)) \ (G . n) by A36, XBOOLE_1:63; :: thesis: verum
end;
then QQ . k misses (F . (k + 1)) \ (G . k) ;
then A37: (QQ . k) /\ ((F . (k + 1)) \ (G . k)) = {} ;
A38: QQ . k c= X \ ((F . (k + 1)) \ (G . k))
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in QQ . k or z in X \ ((F . (k + 1)) \ (G . k)) )
assume A39: z in QQ . k ; :: thesis: z in X \ ((F . (k + 1)) \ (G . k))
then not z in (F . (k + 1)) \ (G . k) by A37, XBOOLE_0:def 4;
hence z in X \ ((F . (k + 1)) \ (G . k)) by A39, XBOOLE_0:def 5; :: thesis: verum
end;
Q . (k + 1) = W /\ (B . (k + 1)) by A18
.= W /\ ((F . (k + 1)) \ (G . k)) by A10 ;
then A40: Q . (k + 1) c= (F . (k + 1)) \ (G . k) by XBOOLE_1:17;
F . (k + 1) c= union (rng F) by FUNCT_2:4, ZFMISC_1:74;
then (F . (k + 1)) \ (G . k) c= union (rng F) by A25;
then X \ (union (rng F)) c= X \ ((F . (k + 1)) \ (G . k)) by XBOOLE_1:34;
then Z c= X \ ((F . (k + 1)) \ (G . k)) by A5, A6;
then Z \/ (QQ . k) c= X \ ((F . (k + 1)) \ (G . k)) by A38, XBOOLE_1:8;
then A41: (C . (Q . (k + 1))) + (C . (Z \/ (QQ . k))) = C . ((Z \/ (QQ . k)) \/ (Q . (k + 1))) by A40, A28, Th5
.= C . (Z \/ (QQ . (k + 1))) by A26, XBOOLE_1:4 ;
A42: 0. <= C . Z by A1, SUPINF_2:39;
assume C . (Z \/ (QQ . k)) = (C . Z) + ((Ser (C * Q)) . k) ; :: thesis: S2[k + 1]
then C . (Z \/ (QQ . (k + 1))) = ((C . Z) + ((Ser (C * Q)) . k)) + ((C * Q) . (k + 1)) by A41, FUNCT_2:15
.= (C . Z) + (((Ser (C * Q)) . k) + ((C * Q) . (k + 1))) by A42, A30, A29, XXREAL_3:44
.= (C . Z) + ((Ser (C * Q)) . (k + 1)) by SUPINF_2:def 11 ;
hence S2[k + 1] ; :: thesis: verum
end;
QQ . 0 = W /\ (F . 0) by A9, A18, A20;
then A43: QQ . 0 c= F . 0 by XBOOLE_1:17;
A44: (Ser (C * Q)) . 0 = (C * Q) . 0 by SUPINF_2:def 11
.= C . (QQ . 0) by A20, FUNCT_2:15 ;
F . 0 in rng F by FUNCT_2:4;
then X \ (union (rng F)) c= X \ (F . 0) by XBOOLE_1:34, ZFMISC_1:74;
then Z c= X \ (F . 0) by A5, A6;
then A45: S2[ 0 ] by A22, A43, A44, Th5;
A46: for n being Nat holds S2[n] from NAT_1:sch 2(A45, A24);
 defpred S3[ Nat] means QQ . $1 c= W;
A47: for n being Nat st S3[n] holds
S3[n + 1]
proof
let n be Nat; :: thesis: ( S3[n] implies S3[n + 1] )
assume A48: QQ . n c= W ; :: thesis: S3[n + 1]
A49: W /\ (B . (n + 1)) c= W by XBOOLE_1:17;
QQ . (n + 1) = (Q . (n + 1)) \/ (QQ . n) by A21
.= (W /\ (B . (n + 1))) \/ (QQ . n) by A18 ;
then QQ . (n + 1) c= W \/ W by A48, A49, XBOOLE_1:13;
hence S3[n + 1] ; :: thesis: verum
end;
QQ . 0 = W /\ (B . 0) by A18, A20;
then A50: S3[ 0 ] by XBOOLE_1:17;
A51: for n being Nat holds S3[n] from NAT_1:sch 2(A50, A47);
 A52: union (rng Q) = W by A4, A6, A11, A19, XBOOLE_1:28;
A53: ( C . Z is real implies (C . W) + (C . Z) <= C . (W \/ Z) )
proof
defpred S4[ object , object ] means ( ( $1 = 0 implies $2 = (C . (Z \/ W)) - (C . Z) ) & ( $1 <> 0 implies $2 = 0. ) );
A54: for x being object st x in NAT holds
ex y being object st
( y in ExtREAL & S4[x,y] )
proof
let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in ExtREAL & S4[x,y] ) )
assume x in NAT ; :: thesis: ex y being object st
( y in ExtREAL & S4[x,y] )
then reconsider x = x as Element of NAT ;
( x <> 0 implies ex y being set st
( y in ExtREAL & S4[x,y] ) ) ;
hence ex y being object st
( y in ExtREAL & S4[x,y] ) ; :: thesis: verum
end;
consider R being sequence of ExtREAL such that
A55: for x being object st x in NAT holds
S4[x,R . x] from FUNCT_2:sch 1(A54);
 assume A56: C . Z is real ; :: thesis: (C . W) + (C . Z) <= C . (W \/ Z)
for n being Element of NAT holds 0. <= R . n
proof
let n be Element of NAT ; :: thesis: 0. <= R . n
( C . Z in REAL or C . Z in {-infty,+infty} ) by XBOOLE_0:def 3, XXREAL_0:def 4;
then consider y being Element of REAL such that
A57: y = C . Z by A56, TARSKI:def 2;
Z c= Z \/ W by XBOOLE_1:7;
then C . Z <= C . (Z \/ W) by Def1;
then A58: (C . Z) - (C . Z) <= (C . (Z \/ W)) - (C . Z) by XXREAL_3:37;
(C . Z) - (C . Z) = y - y by A57, SUPINF_2:3;
hence 0. <= R . n by A55, A58; :: thesis: verum
end;
then A59: R is nonnegative by SUPINF_2:39;
A60: for n being Element of NAT holds (Ser (C * Q)) . n <= (C . (Z \/ W)) - (C . Z)
proof
let n be Element of NAT ; :: thesis: (Ser (C * Q)) . n <= (C . (Z \/ W)) - (C . Z)
A61: Z \/ (QQ . n) c= Z \/ W by A51, XBOOLE_1:9;
((Ser (C * Q)) . n) + (C . Z) = C . (Z \/ (QQ . n)) by A46;
then ((Ser (C * Q)) . n) + (C . Z) <= C . (Z \/ W) by A61, Def1;
hence (Ser (C * Q)) . n <= (C . (Z \/ W)) - (C . Z) by A56, XXREAL_3:45; :: thesis: verum
end;
A62: for n being Element of NAT holds (Ser (C * Q)) . n <= (Ser R) . n
proof
let n be Element of NAT ; :: thesis: (Ser (C * Q)) . n <= (Ser R) . n
defpred S5[ Nat] means (Ser R) . $1 = (C . (Z \/ W)) - (C . Z);
A63: for k being Nat st S5[k] holds
S5[k + 1]
proof
let k be Nat; :: thesis: ( S5[k] implies S5[k + 1] )
assume A64: (Ser R) . k = (C . (Z \/ W)) - (C . Z) ; :: thesis: S5[k + 1]
set y = (Ser R) . k;
thus (Ser R) . (k + 1) = ((Ser R) . k) + (R . (k + 1)) by SUPINF_2:def 11
.= ((Ser R) . k) + 0. by A55
.= (C . (Z \/ W)) - (C . Z) by A64, XXREAL_3:4 ; :: thesis: verum
end;
(Ser R) . 0 = R . 0 by SUPINF_2:def 11;
then A65: S5[ 0 ] by A55;
for k being Nat holds S5[k] from NAT_1:sch 2(A65, A63);
 then (Ser R) . n = (C . (Z \/ W)) - (C . Z) ;
hence (Ser (C * Q)) . n <= (Ser R) . n by A60; :: thesis: verum
end;
set y = (Ser R) . 0;
(Ser R) . 0 = R . 0 by SUPINF_2:def 11;
then A66: (Ser R) . 0 = (C . (Z \/ W)) - (C . Z) by A55;
A67: C . W <= SUM (C * Q) by A52, Def1;
for k being Element of NAT st 1 <= k holds
R . k = 0. by A55;
then A68: SUM R = (Ser R) . 1 by A59, SUPINF_2:48;
(Ser R) . 1 = ((Ser R) . 0) + (R . (0 + 1)) by SUPINF_2:def 11
.= ((Ser R) . 0) + 0. by A55
.= (C . (Z \/ W)) - (C . Z) by A66, XXREAL_3:4 ;
then SUM (C * Q) <= (C . (Z \/ W)) - (C . Z) by A62, A68, MEASURE3:1;
then C . W <= (C . (Z \/ W)) - (C . Z) by A67, XXREAL_0:2;
hence (C . W) + (C . Z) <= C . (W \/ Z) by A56, XXREAL_3:45; :: thesis: verum
end;
A69: ( C . Z = +infty implies (C . W) + (C . Z) <= C . (W \/ Z) )
proof
A70: Z c= W \/ Z by XBOOLE_1:7;
assume A71: C . Z = +infty ; :: thesis: (C . W) + (C . Z) <= C . (W \/ Z)
0. <= C . W by A1, MEASURE1:def 2;
then (C . W) + (C . Z) = +infty by A71, XXREAL_3:def 2;
hence (C . W) + (C . Z) <= C . (W \/ Z) by A71, A70, Def1; :: thesis: verum
end;
0 <= C . Z by A1, MEASURE1:def 2;
then ( C . Z is Element of REAL or C . Z = +infty ) by XXREAL_0:14;
hence (C . W) + (C . Z) <= C . (W \/ Z) by A69, A53; :: thesis: verum
end;
hence union M in sigma_Field C by Def2; :: thesis: verum
end;
for A being set st A in sigma_Field C holds
X \ A in sigma_Field C by Th7;
then reconsider Y = sigma_Field C as non empty compl-closed sigma-additive Subset-Family of X by A2, MEASURE1:def 1, MEASURE1:def 5;
Y is SigmaField of X ;
hence sigma_Field C is SigmaField of X ; :: thesis: verum