:: MEASURE4 semantic presentation

begin


theorem Th1: :: MEASURE4:1
for X being set
for S being non empty Subset-Family of X
for F, G being Function of NAT,S
for A being Element of S st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds
union (rng G) = A /\ (union (rng F))
proof
let X be set ; ::_thesis: for S being non empty Subset-Family of X
for F, G being Function of NAT,S
for A being Element of S st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds
union (rng G) = A /\ (union (rng F))
let S be non empty Subset-Family of X; ::_thesis: for F, G being Function of NAT,S
for A being Element of S st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds
union (rng G) = A /\ (union (rng F))
let F, G be Function of NAT,S; ::_thesis: for A being Element of S st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds
union (rng G) = A /\ (union (rng F))
let A be Element of S; ::_thesis: ( ( for n being Element of NAT holds G . n = A /\ (F . n) ) implies union (rng G) = A /\ (union (rng F)) )
assume A1: for n being Element of NAT holds G . n = A /\ (F . n) ; ::_thesis: union (rng G) = A /\ (union (rng F))
thus  union (rng G) c= A /\ (union (rng F)) :: according to XBOOLE_0:def_10 ::_thesis: A /\ (union (rng F)) c= union (rng G)
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in union (rng G) or r in A /\ (union (rng F)) )
assume  r in union (rng G) ; ::_thesis: r in A /\ (union (rng F))
then consider E being set  such that
A2: r in E and
A3: E in rng G by TARSKI:def_4;
consider s being set  such that
A4: s in dom G and
A5: E = G . s by A3, FUNCT_1:def_3;
reconsider s = s as Element of NAT by A4;
A6: r in A /\ (F . s) by A1, A2, A5;
then A7: r in A by XBOOLE_0:def_4;
A8: F . s in rng F by FUNCT_2:4;
 r in F . s by A6, XBOOLE_0:def_4;
then  r in union (rng F) by A8, TARSKI:def_4;
hence  r in A /\ (union (rng F)) by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in A /\ (union (rng F)) or r in union (rng G) )
assume A9: r in A /\ (union (rng F)) ; ::_thesis: r in union (rng G)
then A10: r in A by XBOOLE_0:def_4;
 r in union (rng F) by A9, XBOOLE_0:def_4;
then consider E being set  such that
A11: r in E and
A12: E in rng F by TARSKI:def_4;
consider s being set  such that
A13: s in dom F and
A14: E = F . s by A12, FUNCT_1:def_3;
reconsider s = s as Element of NAT by A13;
A15: G . s in rng G by FUNCT_2:4;
 A /\ E = G . s by A1, A14;
then  r in G . s by A10, A11, XBOOLE_0:def_4;
hence  r in union (rng G) by A15, TARSKI:def_4; ::_thesis: verum
end;

theorem Th2: :: MEASURE4:2
for X being set
for S being non empty Subset-Family of X
for F, G being Function of NAT,S st G . 0 = F . 0 & ( for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ) holds
for H being Function of NAT,S st H . 0 = F . 0 & ( for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) ) holds
union (rng F) = union (rng H)
proof
let X be set ; ::_thesis: for S being non empty Subset-Family of X
for F, G being Function of NAT,S st G . 0 = F . 0 & ( for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ) holds
for H being Function of NAT,S st H . 0 = F . 0 & ( for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) ) holds
union (rng F) = union (rng H)
let S be non empty Subset-Family of X; ::_thesis: for F, G being Function of NAT,S st G . 0 = F . 0 & ( for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ) holds
for H being Function of NAT,S st H . 0 = F . 0 & ( for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) ) holds
union (rng F) = union (rng H)
let F, G be Function of NAT,S; ::_thesis: ( G . 0 = F . 0 & ( for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ) implies for H being Function of NAT,S st H . 0 = F . 0 & ( for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) ) holds
union (rng F) = union (rng H) )
assume that
A1: G . 0 = F . 0 and
A2: for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ; ::_thesis: for H being Function of NAT,S st H . 0 = F . 0 & ( for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) ) holds
union (rng F) = union (rng H)
let H be Function of NAT,S; ::_thesis: ( H . 0 = F . 0 & ( for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) ) implies union (rng F) = union (rng H) )
assume that
A3: H . 0 = F . 0 and
A4: for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) ; ::_thesis: union (rng F) = union (rng H)
thus  union (rng F) c= union (rng H) :: according to XBOOLE_0:def_10 ::_thesis: union (rng H) c= union (rng F)
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in union (rng F) or r in union (rng H) )
assume  r in union (rng F) ; ::_thesis: r in union (rng H)
then consider E being set  such that
A5: r in E and
A6: E in rng F by TARSKI:def_4;
A7: ex s being set st
( s in dom F & E = F . s ) by A6, FUNCT_1:def_3;
 ex s1 being Element of NAT st r in H . s1
proof
defpred S1[ Nat] means r in F . $1;
A8: ex k being Nat st S1[k] by A5, A7;
 ex k being Nat st
( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from NAT_1:sch_5(A8);
then consider k being Nat such that
A9: r in F . k and
A10: for n being Nat st r in F . n holds
k <= n ;
A11: ( ex l being Nat st k = l + 1 implies ex s1 being Element of NAT st r in H . s1 )
proof
given l being Nat such that A12: k = l + 1 ; ::_thesis: ex s1 being Element of NAT st r in H . s1
take  k ; ::_thesis: ( k is Element of REAL & k is Element of NAT & r in H . k )
reconsider l = l as Element of NAT by ORDINAL1:def_12;
A13: not r in G . l
proof
assume  r in G . l ; ::_thesis: contradiction
then consider i being Element of NAT  such that
A14: i <= l and
A15: r in F . i by A1, A2, MEASURE2:5;
 k <= i by A10, A15;
hence  contradiction by A12, A14, NAT_1:13; ::_thesis: verum
end;
 H . (l + 1) = (F . (l + 1)) \ (G . l) by A4;
hence  ( k is Element of REAL & k is Element of NAT & r in H . k ) by A9, A12, A13, XBOOLE_0:def_5; ::_thesis: verum
end;
 ( k = 0 implies ex s1 being Element of NAT st r in H . s1 ) by A3, A9;
hence  ex s1 being Element of NAT st r in H . s1 by A11, NAT_1:6; ::_thesis: verum
end;
then consider s1 being Element of NAT  such that
A16: r in H . s1 ;
 H . s1 in rng H by FUNCT_2:4;
hence  r in union (rng H) by A16, TARSKI:def_4; ::_thesis: verum
end;
A17: for n being Element of NAT holds H . n c= F . n
proof
let n be Element of NAT ; ::_thesis: H . n c= F . n
A18: ( ex k being Nat st n = k + 1 implies H . n c= F . n )
proof
given k being Nat such that A19: n = k + 1 ; ::_thesis: H . n c= F . n
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 H . n = (F . n) \ (G . k) by A4, A19;
hence  H . n c= F . n ; ::_thesis: verum
end;
 ( n = 0 implies H . n c= F . n ) by A3;
hence  H . n c= F . n by A18, NAT_1:6; ::_thesis: verum
end;
 union (rng H) c= union (rng F)
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in union (rng H) or r in union (rng F) )
assume  r in union (rng H) ; ::_thesis: r in union (rng F)
then consider E being set  such that
A20: r in E and
A21: E in rng H by TARSKI:def_4;
consider s being set  such that
A22: s in dom H and
A23: E = H . s by A21, FUNCT_1:def_3;
reconsider s = s as Element of NAT by A22;
A24: F . s in rng F by FUNCT_2:4;
 E c= F . s by A17, A23;
hence  r in union (rng F) by A20, A24, TARSKI:def_4; ::_thesis: verum
end;
hence  union (rng H) c= union (rng F) ; ::_thesis: verum
end;

theorem Th3: :: MEASURE4:3
for X being set holds bool X is SigmaField of X
proof
let X be set ; ::_thesis: bool X is SigmaField of X
A1: for M being N_Sub_set_fam of X st M c= bool X holds
union M in bool X ;
reconsider Y = bool X as Subset-Family of X ;
 for A being set st A in bool X holds
X \ A in bool X ;
then reconsider Y = Y as non empty compl-closed sigma-additive Subset-Family of X by A1, MEASURE1:def_1, MEASURE1:def_5;
 Y is SigmaField of X ;
hence  bool X is SigmaField of X ; ::_thesis: verum
end;

definition
let X be set ;
mode C_Measure of X ->  Function of (bool X),ExtREAL means :Def1: :: MEASURE4:def 1
( it is V87() & it is zeroed & ( for A, B being Subset of X st A c= B holds
( it . A <= it . B & ( for F being Function of NAT,(bool X) holds it . (union (rng F)) <= SUM (it * F) ) ) ) );
existence
 ex b1 being Function of (bool X),ExtREAL st
( b1 is V87() & b1 is zeroed & ( for A, B being Subset of X st A c= B holds
( b1 . A <= b1 . B & ( for F being Function of NAT,(bool X) holds b1 . (union (rng F)) <= SUM (b1 * F) ) ) ) )
proof
set M = (bool X) --> 0.;
take  (bool X) --> 0. ; ::_thesis: ( (bool X) --> 0. is V87() & (bool X) --> 0. is zeroed & ( for A, B being Subset of X st A c= B holds
( ((bool X) --> 0.) . A <= ((bool X) --> 0.) . B & ( for F being Function of NAT,(bool X) holds ((bool X) --> 0.) . (union (rng F)) <= SUM (((bool X) --> 0.) * F) ) ) ) )
A1: for A being Subset of X holds 0. <= ((bool X) --> 0.) . A ;
then A2: (bool X) --> 0. is V87() by MEASURE1:def_2;
A3: for F being Function of NAT,(bool X) holds ((bool X) --> 0.) . (union (rng F)) <= SUM (((bool X) --> 0.) * F)
proof
let F be Function of NAT,(bool X); ::_thesis: ((bool X) --> 0.) . (union (rng F)) <= SUM (((bool X) --> 0.) * F)
A4: ((bool X) --> 0.) . (union (rng F)) = 0. by FUNCOP_1:7;
A5: for r being Element of NAT st 0 <= r holds
(((bool X) --> 0.) * F) . r = 0.
proof
let r be Element of NAT ; ::_thesis: ( 0 <= r implies (((bool X) --> 0.) * F) . r = 0. )
 dom (((bool X) --> 0.) * F) = NAT by FUNCT_2:def_1;
then  (((bool X) --> 0.) * F) . r = ((bool X) --> 0.) . (F . r) by FUNCT_1:12;
hence  ( 0 <= r implies (((bool X) --> 0.) * F) . r = 0. ) by FUNCOP_1:7; ::_thesis: verum
end;
A6: (Ser (((bool X) --> 0.) * F)) . 0 = (((bool X) --> 0.) * F) . 0 by SUPINF_2:44;
 ((bool X) --> 0.) * F is V87() by A2, MEASURE1:25;
hence  ((bool X) --> 0.) . (union (rng F)) <= SUM (((bool X) --> 0.) * F) by A4, A5, A6, SUPINF_2:48; ::_thesis: verum
end;
 {} c= X by XBOOLE_1:2;
then  ((bool X) --> 0.) . {} = 0. by FUNCOP_1:7;
hence  ( (bool X) --> 0. is V87() & (bool X) --> 0. is zeroed & ( for A, B being Subset of X st A c= B holds
( ((bool X) --> 0.) . A <= ((bool X) --> 0.) . B & ( for F being Function of NAT,(bool X) holds ((bool X) --> 0.) . (union (rng F)) <= SUM (((bool X) --> 0.) * F) ) ) ) ) by A1, A3, FUNCOP_1:7, MEASURE1:def_2, VALUED_0:def_19; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines C_Measure MEASURE4:def_1_:_
 for X being set
for b2 being Function of (bool X),ExtREAL holds
( b2 is C_Measure of X iff ( b2 is V87() & b2 is zeroed & ( for A, B being Subset of X st A c= B holds
( b2 . A <= b2 . B & ( for F being Function of NAT,(bool X) holds b2 . (union (rng F)) <= SUM (b2 * F) ) ) ) ) );

definition
let X be set ;
let C be C_Measure of X;
func sigma_Field C ->  non empty Subset-Family of X means :Def2: :: MEASURE4:def 2
 for A being Subset of X holds
( A in it iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) );
existence
 ex b1 being non empty Subset-Family of X st
for A being Subset of X holds
( A in b1 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) )
proof
reconsider A = {} as Subset of X by XBOOLE_1:2;
defpred S1[ set ] means  for A being set st A = $1 holds
for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z);
consider D being set  such that
A1: for y being set holds
( y in D iff ( y in bool X & S1[y] ) ) from XBOOLE_0:sch_1();
A2: for A being set holds
( A in D iff ( A in bool X & ( for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ) )
proof
let A be set ; ::_thesis: ( A in D iff ( A in bool X & ( for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ) )
 ( S1[A] iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ;
hence  ( A in D iff ( A in bool X & ( for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ) ) by A1; ::_thesis: verum
end;
then A3: for A being set st A in D holds
A in bool X ;
now__::_thesis:_for_W,_Z_being_Subset_of_X_st_W_c=_A_&_Z_c=_X_\_A_holds_
(C_._W)_+_(C_._Z)_<=_C_._(W_\/_Z)
let W, Z be Subset of X; ::_thesis: ( W c= A & Z c= X \ A implies (C . W) + (C . Z) <= C . (W \/ Z) )
assume that
A4: W c= A and
 Z c= X \ A ; ::_thesis: (C . W) + (C . Z) <= C . (W \/ Z)
A5: W = {} by A4;
 C is zeroed by Def1;
then  C . W = 0 by A5, VALUED_0:def_19;
hence  (C . W) + (C . Z) <= C . (W \/ Z) by A5, XXREAL_3:4; ::_thesis: verum
end;
then reconsider D = D as non empty Subset-Family of X by A2, A3, TARSKI:def_3;
take  D ; ::_thesis: for A being Subset of X holds
( A in D iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) )
thus  for A being Subset of X holds
( A in D iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty Subset-Family of X st ( for A being Subset of X holds
( A in b1 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ) & ( for A being Subset of X holds
( A in b2 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ) holds
b1 = b2
proof
let D1, D2 be non empty Subset-Family of X; ::_thesis: ( ( for A being Subset of X holds
( A in D1 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ) & ( for A being Subset of X holds
( A in D2 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ) implies D1 = D2 )
assume that
A6: for A being Subset of X holds
( A in D1 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) and
A7: for A being Subset of X holds
( A in D2 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ; ::_thesis: D1 = D2
 for A being set holds
( A in D1 iff A in D2 )
proof
let A be set ; ::_thesis: ( A in D1 iff A in D2 )
hereby  ::_thesis: ( A in D2 implies A in D1 )
assume A8: A in D1 ; ::_thesis: A in D2
then reconsider A9 = A as Subset of X ;
 for W, Z being Subset of X st W c= A & Z c= X \ A9 holds
(C . W) + (C . Z) <= C . (W \/ Z) by A6, A8;
hence  A in D2 by A7; ::_thesis: verum
end;
assume A9: A in D2 ; ::_thesis: A in D1
then reconsider A = A as Subset of X ;
 for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) by A7, A9;
hence  A in D1 by A6; ::_thesis: verum
end;
hence  D1 = D2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines sigma_Field MEASURE4:def_2_:_
 for X being set
for C being C_Measure of X
for b3 being non empty Subset-Family of X holds
( b3 = sigma_Field C iff for A being Subset of X holds
( A in b3 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) );

theorem Th4: :: MEASURE4:4
for X being set
for C being C_Measure of X
for W, Z being Subset of X holds C . (W \/ Z) <= (C . W) + (C . Z)
proof
let X be set ; ::_thesis: for C being C_Measure of X
for W, Z being Subset of X holds C . (W \/ Z) <= (C . W) + (C . Z)
let C be C_Measure of X; ::_thesis: for W, Z being Subset of X holds C . (W \/ Z) <= (C . W) + (C . Z)
let W, Z be Subset of X; ::_thesis: C . (W \/ Z) <= (C . W) + (C . Z)
reconsider P = {} as Subset of X by XBOOLE_1:2;
consider F being Function of NAT,(bool X) such that
A1: rng F = {W,Z,P} and
A2: F . 0 = W and
A3: F . 1 = Z and
A4: for n being Element of NAT st 1 < n holds
F . n = P by MEASURE1:17;
A5: (C * F) . 1 = C . Z by A3, FUNCT_2:15;
set G = C * F;
A6: union {W,Z,P} = W \/ Z
proof
thus  union {W,Z,P} c= W \/ Z :: according to XBOOLE_0:def_10 ::_thesis: W \/ Z c= union {W,Z,P}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union {W,Z,P} or x in W \/ Z )
assume  x in union {W,Z,P} ; ::_thesis: x in W \/ Z
then  ex Y being set st
( x in Y & Y in {W,Z,P} ) by TARSKI:def_4;
then  ( x in W or x in Z or x in P ) by ENUMSET1:def_1;
hence  x in W \/ Z by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W \/ Z or x in union {W,Z,P} )
assume A7: x in W \/ Z ; ::_thesis: x in union {W,Z,P}
now__::_thesis:_ex_Y_being_Subset_of_X_st_
(_x_in_Y_&_Y_in_{W,Z,P}_)
percases ( x in W or x in Z ) by A7, XBOOLE_0:def_3;
supposeA8: x in W ; ::_thesis: ex Y being Subset of X st
( x in Y & Y in {W,Z,P} )
take Y = W; ::_thesis: ( x in Y & Y in {W,Z,P} )
thus  ( x in Y & Y in {W,Z,P} ) by A8, ENUMSET1:def_1; ::_thesis: verum
end;
supposeA9: x in Z ; ::_thesis: ex Y being Subset of X st
( x in Y & Y in {W,Z,P} )
take Y = Z; ::_thesis: ( x in Y & Y in {W,Z,P} )
thus  ( x in Y & Y in {W,Z,P} ) by A9, ENUMSET1:def_1; ::_thesis: verum
end;
end;
end;
hence  x in union {W,Z,P} by TARSKI:def_4; ::_thesis: verum
end;
A10: C is zeroed by Def1;
A11: for r being Element of NAT st 2 <= r holds
(C * F) . r = 0.
proof
let r be Element of NAT ; ::_thesis: ( 2 <= r implies (C * F) . r = 0. )
assume  2 <= r ; ::_thesis: (C * F) . r = 0.
then  1 + 1 <= r ;
then  1 < r by NAT_1:13;
then A12: F . r = {} by A4;
 C is zeroed by Def1;
then  C . (F . r) = 0. by A12, VALUED_0:def_19;
hence  (C * F) . r = 0. by FUNCT_2:15; ::_thesis: verum
end;
 C is V87() by Def1;
then A13: C * F is V87() by MEASURE1:25;
 F . 2 = P by A4;
then A14: (C * F) . 2 = C . P by FUNCT_2:15;
A15: (C * F) . 0 = C . W by A2, FUNCT_2:15;
consider y1, y2 being R_eal such that
A16: y1 = (Ser (C * F)) . 1 and
A17: y2 = (Ser (C * F)) . 0 ;
(Ser (C * F)) . 2 = y1 + ((C * F) . (1 + 1)) by A16, SUPINF_2:44
.= ((Ser (C * F)) . 1) + 0. by A14, A16, A10, VALUED_0:def_19
.= (Ser (C * F)) . 1 by XXREAL_3:4
.= y2 + ((C * F) . (0 + 1)) by A17, SUPINF_2:44
.= (C . W) + (C . Z) by A5, A15, A17, SUPINF_2:44 ;
then  SUM (C * F) = (C . W) + (C . Z) by A13, A11, SUPINF_2:48;
hence  C . (W \/ Z) <= (C . W) + (C . Z) by A1, A6, Def1; ::_thesis: verum
end;

theorem Th5: :: MEASURE4:5
for X being set
for C being C_Measure of X
for A being Subset of X holds
( A in sigma_Field C iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) = C . (W \/ Z) )
proof
let X be set ; ::_thesis: for C being C_Measure of X
for A being Subset of X holds
( A in sigma_Field C iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) = C . (W \/ Z) )
let C be C_Measure of X; ::_thesis: for A being Subset of X holds
( A in sigma_Field C iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) = C . (W \/ Z) )
let A be Subset of X; ::_thesis: ( A in sigma_Field C iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) = C . (W \/ Z) )
hereby  ::_thesis: ( ( for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) = C . (W \/ Z) ) implies A in sigma_Field C )
assume A1: A in sigma_Field C ; ::_thesis: for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) = C . (W \/ Z)
let W, Z be Subset of X; ::_thesis: ( W c= A & Z c= X \ A implies (C . W) + (C . Z) = C . (W \/ Z) )
assume that
A2: W c= A and
A3: Z c= X \ A ; ::_thesis: (C . W) + (C . Z) = C . (W \/ Z)
A4: C . (W \/ Z) <= (C . W) + (C . Z) by Th4;
 (C . W) + (C . Z) <= C . (W \/ Z) by A1, A2, A3, Def2;
hence  (C . W) + (C . Z) = C . (W \/ Z) by A4, XXREAL_0:1; ::_thesis: verum
end;
assume  for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) = C . (W \/ Z) ; ::_thesis: A in sigma_Field C
then  for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ;
hence  A in sigma_Field C by Def2; ::_thesis: verum
end;

theorem Th6: :: MEASURE4:6
for X being set
for C being C_Measure of X
for W, Z being Subset of X st W in sigma_Field C & Z misses W holds
C . (W \/ Z) = (C . W) + (C . Z)
proof
let X be set ; ::_thesis: for C being C_Measure of X
for W, Z being Subset of X st W in sigma_Field C & Z misses W holds
C . (W \/ Z) = (C . W) + (C . Z)
let C be C_Measure of X; ::_thesis: for W, Z being Subset of X st W in sigma_Field C & Z misses W holds
C . (W \/ Z) = (C . W) + (C . Z)
let W, Z be Subset of X; ::_thesis: ( W in sigma_Field C & Z misses W implies C . (W \/ Z) = (C . W) + (C . Z) )
assume that
A1: W in sigma_Field C and
A2: Z misses W ; ::_thesis: C . (W \/ Z) = (C . W) + (C . Z)
 Z \ W c= X \ W by XBOOLE_1:33;
then  Z c= X \ W by A2, XBOOLE_1:83;
hence  C . (W \/ Z) = (C . W) + (C . Z) by A1, Th5; ::_thesis: verum
end;

theorem Th7: :: MEASURE4:7
for A, X being set
for C being C_Measure of X st A in sigma_Field C holds
X \ A in sigma_Field C
proof
let A, X be set ; ::_thesis: for C being C_Measure of X st A in sigma_Field C holds
X \ A in sigma_Field C
let C be C_Measure of X; ::_thesis: ( A in sigma_Field C implies X \ A in sigma_Field C )
assume A1: A in sigma_Field C ; ::_thesis: X \ A in sigma_Field C
 for W, Z being Subset of X st W c= X \ A & Z c= X \ (X \ A) holds
(C . W) + (C . Z) <= C . (W \/ Z)
proof
let W, Z be Subset of X; ::_thesis: ( W c= X \ A & Z c= X \ (X \ A) implies (C . W) + (C . Z) <= C . (W \/ Z) )
assume that
A2: W c= X \ A and
A3: Z c= X \ (X \ A) ; ::_thesis: (C . W) + (C . Z) <= C . (W \/ Z)
 X \ (X \ A) = X /\ A by XBOOLE_1:48;
then  Z c= A by A1, A3, XBOOLE_1:28;
hence  (C . W) + (C . Z) <= C . (W \/ Z) by A1, A2, Def2; ::_thesis: verum
end;
hence  X \ A in sigma_Field C by Def2; ::_thesis: verum
end;

theorem Th8: :: MEASURE4:8
for X, A, B being set
for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds
A \/ B in sigma_Field C
proof
let X, A, B be set ; ::_thesis: for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds
A \/ B in sigma_Field C
let C be C_Measure of X; ::_thesis: ( A in sigma_Field C & B in sigma_Field C implies A \/ B in sigma_Field C )
assume that
A1: A in sigma_Field C and
A2: B in sigma_Field C ; ::_thesis: A \/ B in sigma_Field C
reconsider A = A, B = B as Subset of X by A1, A2;
set D = A \/ B;
 for W, Z being Subset of X st W c= A \/ B & Z c= X \ (A \/ B) holds
(C . W) + (C . Z) = C . (W \/ Z)
proof
let W, Z be Subset of X; ::_thesis: ( W c= A \/ B & Z c= X \ (A \/ B) implies (C . W) + (C . Z) = C . (W \/ Z) )
assume that
A3: W c= A \/ B and
A4: Z c= X \ (A \/ B) ; ::_thesis: (C . W) + (C . Z) = C . (W \/ Z)
set W2 = W \ A;
set Z1 = (W \ A) \/ Z;
A5: (X \ A) /\ (X \ B) c= X \ B by XBOOLE_1:17;
set W1 = W /\ A;
A6: W /\ A c= A by XBOOLE_1:17;
 (X \ A) /\ (X \ B) c= X \ A by XBOOLE_1:17;
then A7: X \ (A \/ B) c= X \ A by XBOOLE_1:53;
 Z c= (X \ A) /\ (X \ B) by A4, XBOOLE_1:53;
then A8: Z c= X \ B by A5, XBOOLE_1:1;
 W = (W /\ A) \/ (W \ A) by XBOOLE_1:51;
then  C . W <= (C . (W /\ A)) + (C . (W \ A)) by Th4;
then A9: (C . W) + (C . Z) <= ((C . (W /\ A)) + (C . (W \ A))) + (C . Z) by XXREAL_3:36;
 W \ A c= (B \/ A) \ A by A3, XBOOLE_1:33;
then A10: W \ A c= B \ A by XBOOLE_1:40;
 B \ A c= B by XBOOLE_1:36;
then  W \ A c= B by A10, XBOOLE_1:1;
then A11: (C . (W \ A)) + (C . Z) <= C . ((W \ A) \/ Z) by A2, A8, Def2;
 C is V87() by Def1;
then A12: 0. <= C . (W /\ A) by MEASURE1:def_2;
 W \ A c= X \ A by XBOOLE_1:33;
then  (W \ A) \/ Z c= (X \ A) \/ Z by XBOOLE_1:9;
then A13: (W \ A) \/ Z c= X \ A by A4, A7, XBOOLE_1:1, XBOOLE_1:12;
C . (W \/ Z) = C . (((W /\ A) \/ (W \ A)) \/ Z) by XBOOLE_1:51
.= C . ((W /\ A) \/ ((W \ A) \/ Z)) by XBOOLE_1:4
.= (C . (W /\ A)) + (C . ((W \ A) \/ Z)) by A1, A6, A13, Th5 ;
then A14: (C . (W /\ A)) + ((C . (W \ A)) + (C . Z)) <= C . (W \/ Z) by A11, XXREAL_3:36;
A15: C is V87() by Def1;
then A16: 0. <= C . Z by MEASURE1:def_2;
 0. <= C . (W \ A) by A15, MEASURE1:def_2;
then  ((C . (W /\ A)) + (C . (W \ A))) + (C . Z) <= C . (W \/ Z) by A16, A12, A14, XXREAL_3:44;
then A17: (C . W) + (C . Z) <= C . (W \/ Z) by A9, XXREAL_0:2;
 C . (W \/ Z) <= (C . W) + (C . Z) by Th4;
hence  (C . W) + (C . Z) = C . (W \/ Z) by A17, XXREAL_0:1; ::_thesis: verum
end;
hence  A \/ B in sigma_Field C by Th5; ::_thesis: verum
end;

theorem Th9: :: MEASURE4:9
for X, A, B being set
for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds
A /\ B in sigma_Field C
proof
let X, A, B be set ; ::_thesis: for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds
A /\ B in sigma_Field C
let C be C_Measure of X; ::_thesis: ( A in sigma_Field C & B in sigma_Field C implies A /\ B in sigma_Field C )
assume that
A1: A in sigma_Field C and
A2: B in sigma_Field C ; ::_thesis: A /\ B in sigma_Field C
A3: X \ B in sigma_Field C by A2, Th7;
 A /\ B c= X /\ X by A1, A2, XBOOLE_1:27;
then A4: A /\ B = X /\ (A /\ B) by XBOOLE_1:28
.= X \ (X \ (A /\ B)) by XBOOLE_1:48
.= X \ ((X \ A) \/ (X \ B)) by XBOOLE_1:54 ;
 X \ A in sigma_Field C by A1, Th7;
then  (X \ A) \/ (X \ B) in sigma_Field C by A3, Th8;
hence  A /\ B in sigma_Field C by A4, Th7; ::_thesis: verum
end;

theorem Th10: :: MEASURE4:10
for X, A, B being set
for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds
A \ B in sigma_Field C
proof
let X, A, B be set ; ::_thesis: for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds
A \ B in sigma_Field C
let C be C_Measure of X; ::_thesis: ( A in sigma_Field C & B in sigma_Field C implies A \ B in sigma_Field C )
assume that
A1: A in sigma_Field C and
A2: B in sigma_Field C ; ::_thesis: A \ B in sigma_Field C
 for x being set holds
( x in A \ B iff x in A /\ (X \ B) )
proof
let x be set ; ::_thesis: ( x in A \ B iff x in A /\ (X \ B) )
hereby  ::_thesis: ( x in A /\ (X \ B) implies x in A \ B )
assume A3: x in A \ B ; ::_thesis: x in A /\ (X \ B)
then A4: not x in B by XBOOLE_0:def_5;
 x in A by A3;
then  x in X \ B by A1, A4, XBOOLE_0:def_5;
hence  x in A /\ (X \ B) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A5: x in A /\ (X \ B) ; ::_thesis: x in A \ B
then  x in X \ B by XBOOLE_0:def_4;
then A6: not x in B by XBOOLE_0:def_5;
 x in A by A5, XBOOLE_0:def_4;
hence  x in A \ B by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
then A7: A \ B = A /\ (X \ B) by TARSKI:1;
 X \ B in sigma_Field C by A2, Th7;
hence  A \ B in sigma_Field C by A1, A7, Th9; ::_thesis: verum
end;

theorem Th11: :: MEASURE4:11
for X being set
for S being SigmaField of X
for N being Function of NAT,S
for A being Element of S ex F being Function of NAT,S st
for n being Element of NAT holds F . n = A /\ (N . n)
proof
let X be set ; ::_thesis: for S being SigmaField of X
for N being Function of NAT,S
for A being Element of S ex F being Function of NAT,S st
for n being Element of NAT holds F . n = A /\ (N . n)
let S be SigmaField of X; ::_thesis: for N being Function of NAT,S
for A being Element of S ex F being Function of NAT,S st
for n being Element of NAT holds F . n = A /\ (N . n)
let N be Function of NAT,S; ::_thesis: for A being Element of S ex F being Function of NAT,S st
for n being Element of NAT holds F . n = A /\ (N . n)
let A be Element of S; ::_thesis: ex F being Function of NAT,S st
for n being Element of NAT holds F . n = A /\ (N . n)
defpred S1[ set , set ] means ( $1 in NAT implies $2 = A /\ (N . $1) );
A1: for x being set st x in NAT holds
ex y being set st
( y in S & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in S & S1[x,y] ) )
assume  x in NAT ; ::_thesis: ex y being set st
( y in S & S1[x,y] )
then reconsider x = x as Element of NAT ;
consider y being set  such that
A2: y = A /\ (N . x) ;
take  y ; ::_thesis: ( y in S & S1[x,y] )
thus  ( y in S & S1[x,y] ) by A2; ::_thesis: verum
end;
 ex F being Function of NAT,S st
for x being set st x in NAT holds
S1[x,F . x] from FUNCT_2:sch_1(A1);
then consider F being Function of NAT,S such that
A3: for x being set st x in NAT holds
S1[x,F . x] ;
take  F ; ::_thesis: for n being Element of NAT holds F . n = A /\ (N . n)
thus  for n being Element of NAT holds F . n = A /\ (N . n) by A3; ::_thesis: verum
end;

theorem Th12: :: MEASURE4:12
for X being set
for C being C_Measure of X holds sigma_Field C is SigmaField of X
proof
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 V87() 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 Function of NAT,(bool X) such that
A6: rng F = M by SUPINF_2:def_8;
consider G being Function of NAT,S such that
A7: G . 0 = F . 0 and
A8: for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) by MEASURE2:4;
consider B being Function of NAT,S such that
A9: B . 0 = F . 0 and
A10: for n being Element of 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[ Element of 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 Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of 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 Element of NAT holds S1[n] from NAT_1:sch_1(A16, A13);
consider Q being Function of NAT,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 Function of NAT,S such that
A20: QQ . 0 = Q . 0 and
A21: for n being Element of NAT holds QQ . (n + 1) = (Q . (n + 1)) \/ (QQ . n) by MEASURE2:4;
reconsider Q = Q, QQ = QQ, F = F, G = G as Function of NAT,(bool X) ;
A22: F . 0 in sigma_Field C by A12;
defpred S2[ Element of NAT ] means C . (Z \/ (QQ . $1)) = (C . Z) + ((Ser (C * Q)) . $1);
A23: C * Q is V87() by A1, MEASURE1:25;
A24: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
defpred S3[ Element of NAT ] means QQ . $1 c= G . $1;
let k be Element of 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 Element of NAT holds QQ . n misses (F . (n + 1)) \ (G . n)
proof
let n be Element of NAT ; ::_thesis: QQ . n misses (F . (n + 1)) \ (G . n)
A32: for n being Element of NAT st S3[n] holds
S3[n + 1]
proof
let n be Element of 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, XBOOLE_1:1;
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 Element of NAT holds S3[n] from NAT_1:sch_1(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)) = {} by XBOOLE_0:def_7;
A38: QQ . k c= X \ ((F . (k + 1)) \ (G . k))
proof
let z be set ; :: 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, XBOOLE_1:1;
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, XBOOLE_1:1;
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:44 ;
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:44
.= 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, XBOOLE_1:1;
then A45: S2[ 0 ] by A22, A43, A44, Th5;
A46: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A45, A24);
defpred S3[ Element of NAT ] means QQ . $1 c= W;
A47: for n being Element of NAT st S3[n] holds
S3[n + 1]
proof
let n be Element of 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 Element of NAT holds S3[n] from NAT_1:sch_1(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[ set , set ] means ( ( $1 = 0 implies $2 = (C . (Z \/ W)) - (C . Z) ) & ( $1 <> 0 implies $2 = 0. ) );
A54: for x being set st x in NAT holds
ex y being set st
( y in ExtREAL & S4[x,y] )
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in ExtREAL & S4[x,y] ) )
assume  x in NAT ; ::_thesis: ex y being set 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 set st
( y in ExtREAL & S4[x,y] ) ; ::_thesis: verum
end;
consider R being Function of NAT,ExtREAL such that
A55: for x being set 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 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 V87() 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[ Element of NAT ] means (Ser R) . $1 = (C . (Z \/ W)) - (C . Z);
A63: for k being Element of NAT st S5[k] holds
S5[k + 1]
proof
let k be Element of 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:44
.= ((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:44;
then A65: S5[ 0 ] by A55;
 for k being Element of NAT holds S5[k] from NAT_1:sch_1(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:44;
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:44
.= ((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
end;

registration
let X be set ;
let C be C_Measure of X;
cluster sigma_Field C ->  non empty compl-closed sigma-additive ;
coherence
 ( sigma_Field C is sigma-additive & sigma_Field C is compl-closed & not sigma_Field C is empty ) by Th12;
end;

definition
let X be set ;
let S be SigmaField of X;
let A be N_Sub_fam of S;
:: original: union
redefine func union A ->  Element of S;
coherence
 union A is Element of S
proof
 A c= S by MEASURE2:def_1;
hence  union A is Element of S by MEASURE1:def_5; ::_thesis: verum
end;
end;

definition
let X be set ;
let C be C_Measure of X;
func sigma_Meas C ->  Function of (sigma_Field C),ExtREAL means :Def3: :: MEASURE4:def 3
 for A being Subset of X st A in sigma_Field C holds
it . A = C . A;
existence
 ex b1 being Function of (sigma_Field C),ExtREAL st
for A being Subset of X st A in sigma_Field C holds
b1 . A = C . A
proof
 ex D being Function of (sigma_Field C),ExtREAL st
for A being Subset of X st A in sigma_Field C holds
D . A = C . A
proof
deffunc H1( set ) ->  Element of ExtREAL = C . $1;
A1: for S being set st S in sigma_Field C holds
H1(S) in ExtREAL ;
consider D being Function of (sigma_Field C),ExtREAL such that
A2: for S being set st S in sigma_Field C holds
D . S = H1(S) from FUNCT_2:sch_2(A1);
take  D ; ::_thesis: for A being Subset of X st A in sigma_Field C holds
D . A = C . A
thus  for A being Subset of X st A in sigma_Field C holds
D . A = C . A by A2; ::_thesis: verum
end;
then consider D being Function of (sigma_Field C),ExtREAL such that
A3: for A being Subset of X st A in sigma_Field C holds
D . A = C . A ;
take  D ; ::_thesis: for A being Subset of X st A in sigma_Field C holds
D . A = C . A
thus  for A being Subset of X st A in sigma_Field C holds
D . A = C . A by A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (sigma_Field C),ExtREAL st ( for A being Subset of X st A in sigma_Field C holds
b1 . A = C . A ) & ( for A being Subset of X st A in sigma_Field C holds
b2 . A = C . A ) holds
b1 = b2
proof
let D1, D2 be Function of (sigma_Field C),ExtREAL; ::_thesis: ( ( for A being Subset of X st A in sigma_Field C holds
D1 . A = C . A ) & ( for A being Subset of X st A in sigma_Field C holds
D2 . A = C . A ) implies D1 = D2 )
assume that
A4: for A being Subset of X st A in sigma_Field C holds
D1 . A = C . A and
A5: for A being Subset of X st A in sigma_Field C holds
D2 . A = C . A ; ::_thesis: D1 = D2
A6: for A being set st A in sigma_Field C holds
D1 . A = D2 . A
proof
let A be set ; ::_thesis: ( A in sigma_Field C implies D1 . A = D2 . A )
assume A7: A in sigma_Field C ; ::_thesis: D1 . A = D2 . A
then reconsider A = A as Subset of X ;
D1 . A = C . A by A4, A7
.= D2 . A by A5, A7 ;
hence  D1 . A = D2 . A ; ::_thesis: verum
end;
A8: sigma_Field C = dom D2 by FUNCT_2:def_1;
 sigma_Field C = dom D1 by FUNCT_2:def_1;
hence  D1 = D2 by A8, A6, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines sigma_Meas MEASURE4:def_3_:_
 for X being set
for C being C_Measure of X
for b3 being Function of (sigma_Field C),ExtREAL holds
( b3 = sigma_Meas C iff for A being Subset of X st A in sigma_Field C holds
b3 . A = C . A );

theorem Th13: :: MEASURE4:13
for X being set
for C being C_Measure of X holds sigma_Meas C is Measure of (sigma_Field C)
proof
let X be set ; ::_thesis: for C being C_Measure of X holds sigma_Meas C is Measure of (sigma_Field C)
let C be C_Measure of X; ::_thesis: sigma_Meas C is Measure of (sigma_Field C)
A1: now__::_thesis:_for_A_being_Element_of_sigma_Field_C_holds_0._<=_(sigma_Meas_C)_._A
let A be Element of sigma_Field C; ::_thesis: 0. <= (sigma_Meas C) . A
reconsider A9 = A as Subset of X ;
A2: C is V87() by Def1;
 (sigma_Meas C) . A9 = C . A9 by Def3;
hence  0. <= (sigma_Meas C) . A by A2, MEASURE1:def_2; ::_thesis: verum
end;
 {} in sigma_Field C by PROB_1:4;
then A3: (sigma_Meas C) . {} = C . {} by Def3;
A4: now__::_thesis:_for_A,_B_being_Element_of_sigma_Field_C_st_A_misses_B_holds_
(sigma_Meas_C)_._(A_\/_B)_=_((sigma_Meas_C)_._A)_+_((sigma_Meas_C)_._B)
let A, B be Element of sigma_Field C; ::_thesis: ( A misses B implies (sigma_Meas C) . (A \/ B) = ((sigma_Meas C) . A) + ((sigma_Meas C) . B) )
reconsider A9 = A, B9 = B as Subset of X ;
A5: (sigma_Meas C) . B9 = C . B9 by Def3;
assume  A misses B ; ::_thesis: (sigma_Meas C) . (A \/ B) = ((sigma_Meas C) . A) + ((sigma_Meas C) . B)
then A6: C . (A9 \/ B9) = (C . A9) + (C . B9) by Th6;
 (sigma_Meas C) . A9 = C . A9 by Def3;
hence  (sigma_Meas C) . (A \/ B) = ((sigma_Meas C) . A) + ((sigma_Meas C) . B) by A5, A6, Def3; ::_thesis: verum
end;
 C is zeroed by Def1;
then  (sigma_Meas C) . {} = 0. by A3, VALUED_0:def_19;
hence  sigma_Meas C is Measure of (sigma_Field C) by A1, A4, MEASURE1:def_2, MEASURE1:def_3, VALUED_0:def_19; ::_thesis: verum
end;

theorem Th14: :: MEASURE4:14
for X being set
for C being C_Measure of X holds sigma_Meas C is sigma_Measure of (sigma_Field C)
proof
let X be set ; ::_thesis: for C being C_Measure of X holds sigma_Meas C is sigma_Measure of (sigma_Field C)
let C be C_Measure of X; ::_thesis: sigma_Meas C is sigma_Measure of (sigma_Field C)
reconsider M = sigma_Meas C as Measure of (sigma_Field C) by Th13;
 for F being Sep_Sequence of (sigma_Field C) holds M . (union (rng F)) <= SUM (M * F)
proof
let F be Sep_Sequence of (sigma_Field C); ::_thesis: M . (union (rng F)) <= SUM (M * F)
consider A being Subset of X such that
A1: A = union (rng F) ;
A2: for k being set st k in NAT holds
(M * F) . k = (C * F) . k
proof
let k be set ; ::_thesis: ( k in NAT implies (M * F) . k = (C * F) . k )
assume A3: k in NAT ; ::_thesis: (M * F) . k = (C * F) . k
then A4: (M * F) . k = M . (F . k) by FUNCT_2:15;
A5: F . k in sigma_Field C by A3, FUNCT_2:5;
reconsider F = F as Function of NAT,(bool X) by FUNCT_2:7;
 (C * F) . k = C . (F . k) by A3, FUNCT_2:15;
hence  (M * F) . k = (C * F) . k by A4, A5, Def3; ::_thesis: verum
end;
reconsider F9 = F as Function of NAT,(bool X) by FUNCT_2:7;
consider a, b being R_eal such that
 a = M . A and
A6: b = C . A ;
 C * F9 is Function of NAT,ExtREAL ;
then A7: M * F = C * F by A2, FUNCT_2:12;
reconsider F = F as Function of NAT,(bool X) by FUNCT_2:7;
 b <= SUM (C * F) by A1, A6, Def1;
hence  M . (union (rng F)) <= SUM (M * F) by A1, A6, A7, Def3; ::_thesis: verum
end;
hence  sigma_Meas C is sigma_Measure of (sigma_Field C) by MEASURE3:14; ::_thesis: verum
end;

registration
let X be set ;
let C be C_Measure of X;
cluster sigma_Meas C ->  zeroed V87() sigma-additive ;
coherence
 ( sigma_Meas C is nonnegative & sigma_Meas C is sigma-additive & sigma_Meas C is zeroed ) by Th14;
end;

theorem Th15: :: MEASURE4:15
for X being set
for C being C_Measure of X
for A being Subset of X st C . A = 0. holds
A in sigma_Field C
proof
let X be set ; ::_thesis: for C being C_Measure of X
for A being Subset of X st C . A = 0. holds
A in sigma_Field C
let C be C_Measure of X; ::_thesis: for A being Subset of X st C . A = 0. holds
A in sigma_Field C
let A be Subset of X; ::_thesis: ( C . A = 0. implies A in sigma_Field C )
assume A1: C . A = 0. ; ::_thesis: A in sigma_Field C
now__::_thesis:_for_W,_Z_being_Subset_of_X_st_W_c=_A_&_Z_c=_X_\_A_holds_
(C_._W)_+_(C_._Z)_<=_C_._(W_\/_Z)
let W, Z be Subset of X; ::_thesis: ( W c= A & Z c= X \ A implies (C . W) + (C . Z) <= C . (W \/ Z) )
assume that
A2: W c= A and
 Z c= X \ A ; ::_thesis: (C . W) + (C . Z) <= C . (W \/ Z)
 Z c= W \/ Z by XBOOLE_1:7;
then A3: C . Z <= C . (W \/ Z) by Def1;
 C is V87() by Def1;
then  0. <= C . W by MEASURE1:def_2;
then  C . W = 0. by A1, A2, Def1;
hence  (C . W) + (C . Z) <= C . (W \/ Z) by A3, XXREAL_3:4; ::_thesis: verum
end;
hence  A in sigma_Field C by Def2; ::_thesis: verum
end;

theorem :: MEASURE4:16
for X being set
for C being C_Measure of X holds sigma_Meas C is_complete sigma_Field C
proof
let X be set ; ::_thesis: for C being C_Measure of X holds sigma_Meas C is_complete sigma_Field C
let C be C_Measure of X; ::_thesis: sigma_Meas C is_complete sigma_Field C
let A be Subset of X; :: according to MEASURE3:def_1 ::_thesis: for b1 being set holds
( not b1 in sigma_Field C or not A c= b1 or not (sigma_Meas C) . b1 = 0. or A in sigma_Field C )
let B be set ; ::_thesis: ( not B in sigma_Field C or not A c= B or not (sigma_Meas C) . B = 0. or A in sigma_Field C )
assume that
A1: B in sigma_Field C and
A2: A c= B and
A3: (sigma_Meas C) . B = 0. ; ::_thesis: A in sigma_Field C
reconsider B = B as Subset of X by A1;
 C is V87() by Def1;
then A4: 0. <= C . A by MEASURE1:def_2;
 C . B = 0. by A1, A3, Def3;
then  C . A = 0. by A2, A4, Def1;
hence  A in sigma_Field C by Th15; ::_thesis: verum
end;