:: MEASURE1 semantic presentation

begin

theorem Th1: :: MEASURE1:1
for X, Y being set holds union {X,Y,{}} = union {X,Y}
proof
let X, Y be set ; ::_thesis: union {X,Y,{}} = union {X,Y}
thus  union {X,Y,{}} = union ({X,Y} \/ {{}}) by ENUMSET1:3
.= (union {X,Y}) \/ (union {{}}) by ZFMISC_1:78
.= (union {X,Y}) \/ {} by ZFMISC_1:25
.= union {X,Y} ; ::_thesis: verum
end;

theorem :: MEASURE1:2
for X being set
for A, B being Subset of X holds {A,B} is Subset-Family of X
proof
let X be set ; ::_thesis: for A, B being Subset of X holds {A,B} is Subset-Family of X
let A, B be Subset of X; ::_thesis: {A,B} is Subset-Family of X
set C = {A,B};
 {A,B} c= bool X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {A,B} or x in bool X )
assume  x in {A,B} ; ::_thesis: x in bool X
then  ( x = A or x = B ) by TARSKI:def_2;
hence  x in bool X ; ::_thesis: verum
end;
hence  {A,B} is Subset-Family of X ; ::_thesis: verum
end;

theorem :: MEASURE1:3
for X being set
for A, B, C being Subset of X holds {A,B,C} is Subset-Family of X
proof
let X be set ; ::_thesis: for A, B, C being Subset of X holds {A,B,C} is Subset-Family of X
let A, B, C be Subset of X; ::_thesis: {A,B,C} is Subset-Family of X
set D = {A,B,C};
 {A,B,C} c= bool X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {A,B,C} or x in bool X )
assume  x in {A,B,C} ; ::_thesis: x in bool X
then  ( x = A or x = B or x = C ) by ENUMSET1:def_1;
hence  x in bool X ; ::_thesis: verum
end;
hence  {A,B,C} is Subset-Family of X ; ::_thesis: verum
end;

scheme :: MEASURE1:sch 1
DomsetFamEx{ F1() ->  set , P1[ set ] } :
 ex F being non empty Subset-Family of F1() st
for B being set holds
( B in F iff ( B c= F1() & P1[B] ) )
provided
A1: ex B being set st
( B c= F1() & P1[B] )
proof
defpred S1[ set ] means  ex Z being set st
( $1 = Z & P1[Z] );
consider X being set  such that
A2: for x being set holds
( x in X iff ( x in bool F1() & S1[x] ) ) from XBOOLE_0:sch_1();
 X c= bool F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in bool F1() )
assume  x in X ; ::_thesis: x in bool F1()
hence  x in bool F1() by A2; ::_thesis: verum
end;
then reconsider X = X as non empty Subset-Family of F1() by A1, A2;
take  X ; ::_thesis: for B being set holds
( B in X iff ( B c= F1() & P1[B] ) )
 for B being set holds
( B in X iff ( B c= F1() & P1[B] ) )
proof
let B be set ; ::_thesis: ( B in X iff ( B c= F1() & P1[B] ) )
thus  ( B in X implies ( B c= F1() & P1[B] ) ) ::_thesis: ( B c= F1() & P1[B] implies B in X )
proof
assume A3: B in X ; ::_thesis: ( B c= F1() & P1[B] )
then  ex Z being set st
( B = Z & P1[Z] ) by A2;
hence  ( B c= F1() & P1[B] ) by A3; ::_thesis: verum
end;
assume  ( B c= F1() & P1[B] ) ; ::_thesis: B in X
hence  B in X by A2; ::_thesis: verum
end;
hence  for B being set holds
( B in X iff ( B c= F1() & P1[B] ) ) ; ::_thesis: verum
end;

notation
let X be set ;
let S be non empty Subset-Family of X;
synonym X \ S for  COMPLEMENT S;
end;

registration
let X be set ;
let S be non empty Subset-Family of X;
clusterX \ S ->  non empty ;
coherence
 not X \ S is empty
proof
consider x being Subset of X such that
A1: x in S by SUBSET_1:4;
 (x `) ` in S by A1;
hence  not X \ S is empty by SETFAM_1:def_7; ::_thesis: verum
end;
end;

theorem Th4: :: MEASURE1:4
for X being set
for S being non empty Subset-Family of X holds
( meet S = X \ (union (X \ S)) & union S = X \ (meet (X \ S)) )
proof
let X be set ; ::_thesis: for S being non empty Subset-Family of X holds
( meet S = X \ (union (X \ S)) & union S = X \ (meet (X \ S)) )
let S be non empty Subset-Family of X; ::_thesis: ( meet S = X \ (union (X \ S)) & union S = X \ (meet (X \ S)) )
A1: X \ (union (X \ S)) c= meet S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \ (union (X \ S)) or x in meet S )
assume A2: x in X \ (union (X \ S)) ; ::_thesis: x in meet S
then A3: not x in union (X \ S) by XBOOLE_0:def_5;
 for Y being set st Y in S holds
x in Y
proof
let Y be set ; ::_thesis: ( Y in S implies x in Y )
assume that
A4: Y in S and
A5: not x in Y ; ::_thesis: contradiction
reconsider Y = Y as Subset of X by A4;
 (Y `) ` in S by A4;
then A6: Y ` in X \ S by SETFAM_1:def_7;
 x in Y ` by A2, A5, SUBSET_1:29;
hence  contradiction by A3, A6, TARSKI:def_4; ::_thesis: verum
end;
hence  x in meet S by SETFAM_1:def_1; ::_thesis: verum
end;
 meet S c= X \ (union (X \ S))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet S or x in X \ (union (X \ S)) )
assume A7: x in meet S ; ::_thesis: x in X \ (union (X \ S))
 not x in union (X \ S)
proof
assume  x in union (X \ S) ; ::_thesis: contradiction
then consider Z being set  such that
A8: x in Z and
A9: Z in X \ S by TARSKI:def_4;
reconsider Z = Z as Subset of X by A9;
 ( Z ` in S & not x in Z ` ) by A8, A9, SETFAM_1:def_7, XBOOLE_0:def_5;
hence  contradiction by A7, SETFAM_1:def_1; ::_thesis: verum
end;
hence  x in X \ (union (X \ S)) by A7, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  meet S = X \ (union (X \ S)) by A1, XBOOLE_0:def_10; ::_thesis: union S = X \ (meet (X \ S))
thus  union S c= X \ (meet (X \ S)) :: according to XBOOLE_0:def_10 ::_thesis: X \ (meet (X \ S)) c= union S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union S or x in X \ (meet (X \ S)) )
assume  x in union S ; ::_thesis: x in X \ (meet (X \ S))
then consider Y being set  such that
A10: x in Y and
A11: Y in S by TARSKI:def_4;
reconsider Y = Y as Subset of X by A11;
 not x in meet (X \ S)
proof
 (Y `) ` in S by A11;
then A12: Y ` in X \ S by SETFAM_1:def_7;
assume A13: x in meet (X \ S) ; ::_thesis: contradiction
 not x in Y ` by A10, XBOOLE_0:def_5;
hence  contradiction by A13, A12, SETFAM_1:def_1; ::_thesis: verum
end;
hence  x in X \ (meet (X \ S)) by A10, A11, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \ (meet (X \ S)) or x in union S )
assume A14: x in X \ (meet (X \ S)) ; ::_thesis: x in union S
then  not x in meet (X \ S) by XBOOLE_0:def_5;
then consider Z being set  such that
A15: Z in X \ S and
A16: not x in Z by SETFAM_1:def_1;
reconsider Z = Z as Subset of X by A15;
A17: Z ` in S by A15, SETFAM_1:def_7;
 x in Z ` by A14, A16, SUBSET_1:29;
hence  x in union S by A17, TARSKI:def_4; ::_thesis: verum
end;

definition
let X be set ;
let IT be Subset-Family of X;
redefine attr IT is compl-closed  means :Def1: :: MEASURE1:def 1
 for A being set st A in IT holds
X \ A in IT;
compatibility
 ( IT is compl-closed iff for A being set st A in IT holds
X \ A in IT )
proof
hereby  ::_thesis: ( ( for A being set st A in IT holds
X \ A in IT ) implies IT is compl-closed )
assume A1: IT is compl-closed ; ::_thesis: for A being set st A in IT holds
X \ A in IT
let A be set ; ::_thesis: ( A in IT implies X \ A in IT )
assume A2: A in IT ; ::_thesis: X \ A in IT
then reconsider A9 = A as Subset of X ;
 A9 ` in IT by A1, A2, PROB_1:def_1;
hence  X \ A in IT ; ::_thesis: verum
end;
assume A3: for A being set st A in IT holds
X \ A in IT ; ::_thesis: IT is compl-closed
let A be Subset of X; :: according to PROB_1:def_1 ::_thesis: ( not A in IT or A ` in IT )
assume  A in IT ; ::_thesis: A ` in IT
hence  A ` in IT by A3; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines compl-closed MEASURE1:def_1_:_
 for X being set
for IT being Subset-Family of X holds
( IT is compl-closed iff for A being set st A in IT holds
X \ A in IT );

registration
let X be set ;
cluster cup-closed compl-closed  ->  cap-closed for Element of bool (bool X);
coherence
 for b1 being Subset-Family of X st b1 is cup-closed & b1 is compl-closed holds
b1 is cap-closed
proof
let S be Subset-Family of X; ::_thesis: ( S is cup-closed & S is compl-closed implies S is cap-closed )
assume A1: ( S is cup-closed & S is compl-closed ) ; ::_thesis: S is cap-closed
let A, B be set ; :: according to FINSUB_1:def_2 ::_thesis: ( not A in S or not B in S or A /\ B in S )
assume that
A2: A in S and
A3: B in S ; ::_thesis: A /\ B in S
 ( X \ A in S & X \ B in S ) by A1, A2, A3, Def1;
then A4: (X \ A) \/ (X \ B) in S by A1, FINSUB_1:def_1;
 A /\ B c= A by XBOOLE_1:17;
then A /\ B = X /\ (A /\ B) by A2, XBOOLE_1:1, XBOOLE_1:28
.= X \ (X \ (A /\ B)) by XBOOLE_1:48
.= X \ ((X \ A) \/ (X \ B)) by XBOOLE_1:54 ;
hence  A /\ B in S by A1, A4, Def1; ::_thesis: verum
end;
cluster cap-closed compl-closed  ->  cup-closed for Element of bool (bool X);
coherence
 for b1 being Subset-Family of X st b1 is cap-closed & b1 is compl-closed holds
b1 is cup-closed
proof
let S be Subset-Family of X; ::_thesis: ( S is cap-closed & S is compl-closed implies S is cup-closed )
assume A5: ( S is cap-closed & S is compl-closed ) ; ::_thesis: S is cup-closed
let A, B be set ; :: according to FINSUB_1:def_1 ::_thesis: ( not A in S or not B in S or A \/ B in S )
assume A6: ( A in S & B in S ) ; ::_thesis: A \/ B in S
then  ( X \ A in S & X \ B in S ) by A5, Def1;
then A7: (X \ A) /\ (X \ B) in S by A5, FINSUB_1:def_2;
A \/ B = X /\ (A \/ B) by A6, XBOOLE_1:8, XBOOLE_1:28
.= X \ (X \ (A \/ B)) by XBOOLE_1:48
.= X \ ((X \ A) /\ (X \ B)) by XBOOLE_1:53 ;
hence  A \/ B in S by A5, A7, Def1; ::_thesis: verum
end;
end;

theorem :: MEASURE1:5
for X being set
for S being Field_Subset of X holds S = X \ S
proof
let X be set ; ::_thesis: for S being Field_Subset of X holds S = X \ S
let S be Field_Subset of X; ::_thesis: S = X \ S
 for A being set holds
( A in S iff A in X \ S )
proof
let A be set ; ::_thesis: ( A in S iff A in X \ S )
hereby  ::_thesis: ( A in X \ S implies A in S )
assume A1: A in S ; ::_thesis: A in X \ S
then reconsider B = A as Subset of X ;
 B ` in S by A1, PROB_1:def_1;
hence  A in X \ S by SETFAM_1:def_7; ::_thesis: verum
end;
assume A2: A in X \ S ; ::_thesis: A in S
then reconsider B = A as Subset of X ;
 B ` in S by A2, SETFAM_1:def_7;
then  (B `) ` in S by PROB_1:def_1;
hence  A in S ; ::_thesis: verum
end;
hence  S = X \ S by TARSKI:1; ::_thesis: verum
end;

registration
let X be set ;
cluster cap-closed compl-closed  ->  diff-closed for Element of bool (bool X);
coherence
 for b1 being Subset-Family of X st b1 is compl-closed & b1 is cap-closed holds
b1 is diff-closed
proof
let S be Subset-Family of X; ::_thesis: ( S is compl-closed & S is cap-closed implies S is diff-closed )
assume that
A1: S is compl-closed and
A2: S is cap-closed ; ::_thesis: S is diff-closed
let A, B be set ; :: according to FINSUB_1:def_3 ::_thesis: ( not A in S or not B in S or A \ B in S )
assume that
A3: A in S and
A4: B in S ; ::_thesis: A \ B in S
A5: A /\ (X \ B) = (A /\ X) \ B by XBOOLE_1:49
.= A \ B by A3, XBOOLE_1:28 ;
 X \ B in S by A4, A1, Def1;
hence  A \ B in S by A3, A5, A2, FINSUB_1:def_2; ::_thesis: verum
end;
end;

theorem :: MEASURE1:6
for X being set
for S being Field_Subset of X
for A, B being set st A in S & B in S holds
A \ B in S by FINSUB_1:def_3;

theorem :: MEASURE1:7
for X being set
for S being Field_Subset of X holds
( {} in S & X in S ) by PROB_1:4, PROB_1:5;

definition
let X be non empty set ;
let F be Function of X,ExtREAL;
:: original: nonnegative
redefine attrF is nonnegative  means :Def2: :: MEASURE1:def 2
 for A being Element of X holds 0. <= F . A;
compatibility
 ( F is nonnegative iff for A being Element of X holds 0. <= F . A ) by SUPINF_2:39;
end;

:: deftheorem Def2 defines nonnegative MEASURE1:def_2_:_
 for X being non empty set
for F being Function of X,ExtREAL holds
( F is nonnegative iff for A being Element of X holds 0. <= F . A );

definition
let X be set ;
let S be Field_Subset of X;
let F be Function of S,ExtREAL;
attrF is additive  means :Def3: :: MEASURE1:def 3
 for A, B being Element of S st A misses B holds
F . (A \/ B) = (F . A) + (F . B);
end;

:: deftheorem Def3 defines additive MEASURE1:def_3_:_
 for X being set
for S being Field_Subset of X
for F being Function of S,ExtREAL holds
( F is additive iff for A, B being Element of S st A misses B holds
F . (A \/ B) = (F . A) + (F . B) );

registration
let X be set ;
let S be Field_Subset of X;
cluster Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed V89() additive for Element of bool [:S,ExtREAL:];
existence
 ex b1 being Function of S,ExtREAL st
( b1 is V89() & b1 is additive & b1 is zeroed )
proof
reconsider M = S --> 0. as Function of S,ExtREAL ;
A1: for A, B being Element of S st A misses B holds
M . (A \/ B) = (M . A) + (M . B)
proof
let A, B be Element of S; ::_thesis: ( A misses B implies M . (A \/ B) = (M . A) + (M . B) )
assume  A misses B ; ::_thesis: M . (A \/ B) = (M . A) + (M . B)
A2: ( M . A = 0. & M . B = 0. ) by FUNCOP_1:7;
reconsider A = A, B = B as set ;
reconsider A = A, B = B as Element of S ;
 0. = (M . A) + (M . B) by A2, XXREAL_3:4;
hence  M . (A \/ B) = (M . A) + (M . B) by FUNCOP_1:7; ::_thesis: verum
end;
take  M ; ::_thesis: ( M is V89() & M is additive & M is zeroed )
 ( ( for x being Element of S holds 0. <= M . x ) & M . {} = 0. ) by FUNCOP_1:7, PROB_1:4;
hence  ( M is V89() & M is additive & M is zeroed ) by A1, Def2, Def3, VALUED_0:def_19; ::_thesis: verum
end;
end;

definition
let X be set ;
let S be Field_Subset of X;
mode Measure of S is zeroed V89() additive Function of S,ExtREAL;
end;

theorem Th8: :: MEASURE1:8
for X being set
for S being Field_Subset of X
for M being Measure of S
for A, B being Element of S st A c= B holds
M . A <= M . B
proof
let X be set ; ::_thesis: for S being Field_Subset of X
for M being Measure of S
for A, B being Element of S st A c= B holds
M . A <= M . B
let S be Field_Subset of X; ::_thesis: for M being Measure of S
for A, B being Element of S st A c= B holds
M . A <= M . B
let M be Measure of S; ::_thesis: for A, B being Element of S st A c= B holds
M . A <= M . B
let A, B be Element of S; ::_thesis: ( A c= B implies M . A <= M . B )
reconsider C = B \ A as Element of S ;
A1: 0. <= M . C by Def2;
 A misses C by XBOOLE_1:79;
then A2: M . (A \/ C) = (M . A) + (M . C) by Def3;
assume  A c= B ; ::_thesis: M . A <= M . B
then  M . B = (M . A) + (M . C) by A2, XBOOLE_1:45;
hence  M . A <= M . B by A1, XXREAL_3:39; ::_thesis: verum
end;

theorem Th9: :: MEASURE1:9
for X being set
for S being Field_Subset of X
for M being Measure of S
for A, B being Element of S st A c= B & M . A < +infty holds
M . (B \ A) = (M . B) - (M . A)
proof
let X be set ; ::_thesis: for S being Field_Subset of X
for M being Measure of S
for A, B being Element of S st A c= B & M . A < +infty holds
M . (B \ A) = (M . B) - (M . A)
let S be Field_Subset of X; ::_thesis: for M being Measure of S
for A, B being Element of S st A c= B & M . A < +infty holds
M . (B \ A) = (M . B) - (M . A)
let M be Measure of S; ::_thesis: for A, B being Element of S st A c= B & M . A < +infty holds
M . (B \ A) = (M . B) - (M . A)
let A, B be Element of S; ::_thesis: ( A c= B & M . A < +infty implies M . (B \ A) = (M . B) - (M . A) )
set C = B \ A;
assume that
A1: A c= B and
A2: M . A < +infty ; ::_thesis: M . (B \ A) = (M . B) - (M . A)
A3: 0. <= M . A by Def2;
 A misses B \ A by XBOOLE_1:79;
then  M . (A \/ (B \ A)) = (M . A) + (M . (B \ A)) by Def3;
then  M . B = (M . A) + (M . (B \ A)) by A1, XBOOLE_1:45;
hence  M . (B \ A) = (M . B) - (M . A) by A2, A3, XXREAL_3:28; ::_thesis: verum
end;

registration
let X be set ;
cluster non empty cap-closed compl-closed for Element of bool (bool X);
existence
 ex b1 being Subset-Family of X st
( not b1 is empty & b1 is compl-closed & b1 is cap-closed )
proof
take  the non empty cap-closed compl-closed Subset-Family of X ; ::_thesis: ( not the non empty cap-closed compl-closed Subset-Family of X is empty & the non empty cap-closed compl-closed Subset-Family of X is compl-closed & the non empty cap-closed compl-closed Subset-Family of X is cap-closed )
thus  ( not the non empty cap-closed compl-closed Subset-Family of X is empty & the non empty cap-closed compl-closed Subset-Family of X is compl-closed & the non empty cap-closed compl-closed Subset-Family of X is cap-closed ) ; ::_thesis: verum
end;
end;

definition
let X be set ;
let S be non empty cup-closed Subset-Family of X;
let A, B be Element of S;
:: original: \/
redefine funcA \/ B ->  Element of S;
coherence
 A \/ B is Element of S by FINSUB_1:def_1;
end;

definition
let X be set ;
let S be Field_Subset of X;
let A, B be Element of S;
:: original: /\
redefine funcA /\ B ->  Element of S;
coherence
 A /\ B is Element of S by FINSUB_1:def_2;
:: original: \
redefine funcA \ B ->  Element of S;
coherence
 A \ B is Element of S by FINSUB_1:def_3;
end;

theorem Th10: :: MEASURE1:10
for X being set
for S being Field_Subset of X
for M being Measure of S
for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)
proof
let X be set ; ::_thesis: for S being Field_Subset of X
for M being Measure of S
for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)
let S be Field_Subset of X; ::_thesis: for M being Measure of S
for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)
let M be Measure of S; ::_thesis: for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)
let A, B be Element of S; ::_thesis: M . (A \/ B) <= (M . A) + (M . B)
set C = B \ A;
A1: A misses B \ A by XBOOLE_1:79;
A2: M . (B \ A) <= M . B by Th8, XBOOLE_1:36;
M . (A \/ B) = M . (A \/ (B \ A)) by XBOOLE_1:39
.= (M . A) + (M . (B \ A)) by A1, Def3 ;
hence  M . (A \/ B) <= (M . A) + (M . B) by A2, XXREAL_3:36; ::_thesis: verum
end;

theorem :: MEASURE1:11
for X being set
for S being Field_Subset of X
for M being Measure of S holds
( {} in S & X in S & ( for A, B being set st A in S & B in S holds
( X \ A in S & A \/ B in S & A /\ B in S ) ) ) by Def1, FINSUB_1:def_1, FINSUB_1:def_2, PROB_1:4, PROB_1:5;

definition
let X be set ;
let S be Field_Subset of X;
let M be Measure of S;
mode measure_zero of M ->  Element of S means :Def4: :: MEASURE1:def 4
M . it = 0. ;
existence
 ex b1 being Element of S st M . b1 = 0.
proof
reconsider A = {} as Element of S by PROB_1:4;
take  A ; ::_thesis: M . A = 0.
thus  M . A = 0. by VALUED_0:def_19; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines measure_zero MEASURE1:def_4_:_
 for X being set
for S being Field_Subset of X
for M being Measure of S
for b4 being Element of S holds
( b4 is measure_zero of M iff M . b4 = 0. );

theorem :: MEASURE1:12
for X being set
for S being Field_Subset of X
for M being Measure of S
for A being Element of S
for B being measure_zero of M st A c= B holds
A is measure_zero of M
proof
let X be set ; ::_thesis: for S being Field_Subset of X
for M being Measure of S
for A being Element of S
for B being measure_zero of M st A c= B holds
A is measure_zero of M
let S be Field_Subset of X; ::_thesis: for M being Measure of S
for A being Element of S
for B being measure_zero of M st A c= B holds
A is measure_zero of M
let M be Measure of S; ::_thesis: for A being Element of S
for B being measure_zero of M st A c= B holds
A is measure_zero of M
let A be Element of S; ::_thesis: for B being measure_zero of M st A c= B holds
A is measure_zero of M
let B be measure_zero of M; ::_thesis: ( A c= B implies A is measure_zero of M )
assume  A c= B ; ::_thesis: A is measure_zero of M
then  M . A <= M . B by Th8;
then A1: M . A <= 0. by Def4;
 0. <= M . A by Def2;
then  M . A = 0. by A1, XXREAL_0:1;
hence  A is measure_zero of M by Def4; ::_thesis: verum
end;

theorem :: MEASURE1:13
for X being set
for S being Field_Subset of X
for M being Measure of S
for A, B being measure_zero of M holds
( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )
proof
let X be set ; ::_thesis: for S being Field_Subset of X
for M being Measure of S
for A, B being measure_zero of M holds
( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )
let S be Field_Subset of X; ::_thesis: for M being Measure of S
for A, B being measure_zero of M holds
( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )
let M be Measure of S; ::_thesis: for A, B being measure_zero of M holds
( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )
let A, B be measure_zero of M; ::_thesis: ( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )
A1: 0. <= M . (A /\ B) by Def2;
A2: 0. <= M . (A \ B) by Def2;
A3: M . A = 0. by Def4;
then  M . (A \ B) <= 0. by Th8, XBOOLE_1:36;
then A4: M . (A \ B) = 0. by A2, XXREAL_0:1;
 M . B = 0. by Def4;
then  M . (A \/ B) <= 0. + 0. by A3, Th10;
then A5: M . (A \/ B) <= 0. by XXREAL_3:4;
 0. <= M . (A \/ B) by Def2;
then A6: M . (A \/ B) = 0. by A5, XXREAL_0:1;
 M . (A /\ B) <= 0. by A3, Th8, XBOOLE_1:17;
then  M . (A /\ B) = 0. by A1, XXREAL_0:1;
hence  ( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M ) by A6, A4, Def4; ::_thesis: verum
end;

theorem :: MEASURE1:14
for X being set
for S being Field_Subset of X
for M being Measure of S
for A being Element of S
for B being measure_zero of M holds
( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )
proof
let X be set ; ::_thesis: for S being Field_Subset of X
for M being Measure of S
for A being Element of S
for B being measure_zero of M holds
( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )
let S be Field_Subset of X; ::_thesis: for M being Measure of S
for A being Element of S
for B being measure_zero of M holds
( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )
let M be Measure of S; ::_thesis: for A being Element of S
for B being measure_zero of M holds
( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )
let A be Element of S; ::_thesis: for B being measure_zero of M holds
( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )
let B be measure_zero of M; ::_thesis: ( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )
A1: M . A = M . ((A /\ B) \/ (A \ B)) by XBOOLE_1:51;
A2: M . B = 0. by Def4;
then A3: M . (A /\ B) <= 0. by Th8, XBOOLE_1:17;
A4: 0. <= M . (A /\ B) by Def2;
then  M . (A /\ B) = 0. by A3, XXREAL_0:1;
then  M . A <= 0. + (M . (A \ B)) by A1, Th10;
then A5: M . A <= M . (A \ B) by XXREAL_3:4;
 M . (A \/ B) <= (M . A) + 0. by A2, Th10;
then A6: M . (A \/ B) <= M . A by XXREAL_3:4;
 ( M . A <= M . (A \/ B) & M . (A \ B) <= M . A ) by Th8, XBOOLE_1:7, XBOOLE_1:36;
hence  ( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A ) by A4, A6, A3, A5, XXREAL_0:1; ::_thesis: verum
end;

theorem Th15: :: MEASURE1:15
for X being set
for A being Subset of X ex F being Function of NAT,(bool X) st rng F = {A}
proof
let X be set ; ::_thesis: for A being Subset of X ex F being Function of NAT,(bool X) st rng F = {A}
let A be Subset of X; ::_thesis: ex F being Function of NAT,(bool X) st rng F = {A}
take  NAT --> A ; ::_thesis: rng (NAT --> A) = {A}
thus  rng (NAT --> A) = {A} by FUNCOP_1:8; ::_thesis: verum
end;

theorem Th16: :: MEASURE1:16
for A being set ex F being Function of NAT,{A} st
for n being Element of NAT holds F . n = A
proof
let A be set ; ::_thesis: ex F being Function of NAT,{A} st
for n being Element of NAT holds F . n = A
take  NAT --> A ; ::_thesis: for n being Element of NAT holds (NAT --> A) . n = A
thus  for n being Element of NAT holds (NAT --> A) . n = A by TARSKI:def_1; ::_thesis: verum
end;

registration
let X be set ;
cluster non empty V53() for Element of bool (bool X);
existence
 ex b1 being Subset-Family of X st
( not b1 is empty & b1 is V53() )
proof
reconsider S = {{}} as Subset-Family of X by SETFAM_1:46;
take  S ; ::_thesis: ( not S is empty & S is V53() )
thus  not S is empty ; ::_thesis: S is V53()
 {} X is Subset of X ;
hence  ( S is empty or ex F being Function of NAT,(bool X) st S = rng F ) by Th15; :: according to SUPINF_2:def_8 ::_thesis: verum
end;
end;

definition
let X be set ;
mode N_Sub_set_fam of X is non empty V53() Subset-Family of X;
end;

theorem Th17: :: MEASURE1:17
for X being set
for A, B, C being Subset of X ex F being Function of NAT,(bool X) st
( rng F = {A,B,C} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = C ) )
proof
let X be set ; ::_thesis: for A, B, C being Subset of X ex F being Function of NAT,(bool X) st
( rng F = {A,B,C} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = C ) )
let A, B, C be Subset of X; ::_thesis: ex F being Function of NAT,(bool X) st
( rng F = {A,B,C} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = C ) )
take  (A,B) followed_by C ; ::_thesis: ( rng ((A,B) followed_by C) = {A,B,C} & ((A,B) followed_by C) . 0 = A & ((A,B) followed_by C) . 1 = B & ( for n being Element of NAT st 1 < n holds
((A,B) followed_by C) . n = C ) )
thus  ( rng ((A,B) followed_by C) = {A,B,C} & ((A,B) followed_by C) . 0 = A & ((A,B) followed_by C) . 1 = B & ( for n being Element of NAT st 1 < n holds
((A,B) followed_by C) . n = C ) ) by FUNCT_7:122, FUNCT_7:123, FUNCT_7:124, FUNCT_7:127; ::_thesis: verum
end;

theorem :: MEASURE1:18
for X being set
for A, B being Subset of X holds {A,B,{}} is N_Sub_set_fam of X
proof
let X be set ; ::_thesis: for A, B being Subset of X holds {A,B,{}} is N_Sub_set_fam of X
let A, B be Subset of X; ::_thesis: {A,B,{}} is N_Sub_set_fam of X
 ex F being Function of NAT,(bool X) st
( rng F = {A,B,({} X)} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = {} X ) ) by Th17;
hence  {A,B,{}} is N_Sub_set_fam of X by SUPINF_2:def_8; ::_thesis: verum
end;

theorem Th19: :: MEASURE1:19
for X being set
for A, B being Subset of X ex F being Function of NAT,(bool X) st
( rng F = {A,B} & F . 0 = A & ( for n being Element of NAT st 0 < n holds
F . n = B ) )
proof
let X be set ; ::_thesis: for A, B being Subset of X ex F being Function of NAT,(bool X) st
( rng F = {A,B} & F . 0 = A & ( for n being Element of NAT st 0 < n holds
F . n = B ) )
let A, B be Subset of X; ::_thesis: ex F being Function of NAT,(bool X) st
( rng F = {A,B} & F . 0 = A & ( for n being Element of NAT st 0 < n holds
F . n = B ) )
take  A followed_by B ; ::_thesis: ( rng (A followed_by B) = {A,B} & (A followed_by B) . 0 = A & ( for n being Element of NAT st 0 < n holds
(A followed_by B) . n = B ) )
thus  ( rng (A followed_by B) = {A,B} & (A followed_by B) . 0 = A & ( for n being Element of NAT st 0 < n holds
(A followed_by B) . n = B ) ) by FUNCT_7:119, FUNCT_7:120, FUNCT_7:126; ::_thesis: verum
end;

theorem :: MEASURE1:20
for X being set
for A, B being Subset of X holds {A,B} is N_Sub_set_fam of X
proof
let X be set ; ::_thesis: for A, B being Subset of X holds {A,B} is N_Sub_set_fam of X
let A, B be Subset of X; ::_thesis: {A,B} is N_Sub_set_fam of X
 ex F being Function of NAT,(bool X) st
( rng F = {A,B} & F . 0 = A & ( for n being Element of NAT st 0 < n holds
F . n = B ) ) by Th19;
hence  {A,B} is N_Sub_set_fam of X by SUPINF_2:def_8; ::_thesis: verum
end;

theorem Th21: :: MEASURE1:21
for X being set
for S being N_Sub_set_fam of X holds X \ S is N_Sub_set_fam of X
proof
let X be set ; ::_thesis: for S being N_Sub_set_fam of X holds X \ S is N_Sub_set_fam of X
let S be N_Sub_set_fam of X; ::_thesis: X \ S is N_Sub_set_fam of X
consider F being Function of NAT,(bool X) such that
A1: S = rng F by SUPINF_2:def_8;
defpred S1[ set , set ] means  ex V being Subset of X st
( V = F . $1 & $2 = V ` );
A2: for n being set st n in NAT holds
ex y being set st
( y in X \ S & S1[n,y] )
proof
let n be set ; ::_thesis: ( n in NAT implies ex y being set st
( y in X \ S & S1[n,y] ) )
assume  n in NAT ; ::_thesis: ex y being set st
( y in X \ S & S1[n,y] )
then consider V being set  such that
A3: V in S and
A4: V = F . n by A1, FUNCT_2:4;
reconsider V = V as Subset of X by A3;
take  V ` ; ::_thesis: ( V ` in X \ S & S1[n,V ` ] )
 (V `) ` in S by A3;
hence  ( V ` in X \ S & S1[n,V ` ] ) by A4, SETFAM_1:def_7; ::_thesis: verum
end;
A5: ex G being Function of NAT,(X \ S) st
for n being set st n in NAT holds
S1[n,G . n] from FUNCT_2:sch_1(A2);
A6: NAT = dom F by FUNCT_2:def_1;
 ex G being Function of NAT,(bool X) st X \ S = rng G
proof
consider G being Function of NAT,(X \ S) such that
A7: for n being set st n in NAT holds
ex V being Subset of X st
( V = F . n & G . n = V ` ) by A5;
A8: dom G = NAT by FUNCT_2:def_1;
A9: X \ S c= rng G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \ S or x in rng G )
assume A10: x in X \ S ; ::_thesis: x in rng G
then reconsider B = x as Subset of X ;
 B ` in S by A10, SETFAM_1:def_7;
then consider n being set  such that
A11: n in NAT and
A12: F . n = B ` by A1, A6, FUNCT_1:def_3;
 ex V being Subset of X st
( V = F . n & G . n = V ` ) by A7, A11;
hence  x in rng G by A8, A11, A12, FUNCT_1:def_3; ::_thesis: verum
end;
reconsider G = G as Function of NAT,(bool X) by FUNCT_2:7;
take  G ; ::_thesis: X \ S = rng G
thus  X \ S = rng G by A9, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  X \ S is N_Sub_set_fam of X by SUPINF_2:def_8; ::_thesis: verum
end;

definition
let X be set ;
let IT be Subset-Family of X;
attrIT is sigma-additive  means :Def5: :: MEASURE1:def 5
 for M being N_Sub_set_fam of X st M c= IT holds
union M in IT;
end;

:: deftheorem Def5 defines sigma-additive MEASURE1:def_5_:_
 for X being set
for IT being Subset-Family of X holds
( IT is sigma-additive iff for M being N_Sub_set_fam of X st M c= IT holds
union M in IT );

registration
let X be set ;
cluster non empty compl-closed sigma-additive for Element of bool (bool X);
existence
 ex b1 being Subset-Family of X st
( not b1 is empty & b1 is compl-closed & b1 is sigma-additive )
proof
reconsider S = {{},X} as non empty Subset-Family of X by PROB_1:8;
take  S ; ::_thesis: ( not S is empty & S is compl-closed & S is sigma-additive )
thus  not S is empty ; ::_thesis: ( S is compl-closed & S is sigma-additive )
thus  for A being set st A in S holds
X \ A in S :: according to MEASURE1:def_1 ::_thesis: S is sigma-additive
proof
let A be set ; ::_thesis: ( A in S implies X \ A in S )
A1: ( A = {} implies X \ A in S ) by TARSKI:def_2;
A2: ( A = X implies X \ A in S )
proof
assume  A = X ; ::_thesis: X \ A in S
then  X \ A = {} by XBOOLE_1:37;
hence  X \ A in S by TARSKI:def_2; ::_thesis: verum
end;
assume  A in S ; ::_thesis: X \ A in S
hence  X \ A in S by A1, A2, TARSKI:def_2; ::_thesis: verum
end;
let M be N_Sub_set_fam of X; :: according to MEASURE1:def_5 ::_thesis: ( M c= S implies union M in S )
assume A3: M c= S ; ::_thesis: union M in S
A4: ( not X in M implies union M in S )
proof
assume  not X in M ; ::_thesis: union M in S
then  for A being set st A in M holds
A c= {} by A3, TARSKI:def_2;
then  union M c= {} by ZFMISC_1:76;
then  union M = {} ;
hence  union M in S by TARSKI:def_2; ::_thesis: verum
end;
 ( X in M implies union M in S )
proof
assume  X in M ; ::_thesis: union M in S
then  X c= union M by ZFMISC_1:74;
then  X = union M by XBOOLE_0:def_10;
hence  union M in S by TARSKI:def_2; ::_thesis: verum
end;
hence  union M in S by A4; ::_thesis: verum
end;
end;

registration
let X be set ;
cluster compl-closed sigma-multiplicative  ->  sigma-additive for Element of bool (bool X);
coherence
 for b1 being Subset-Family of X st b1 is compl-closed & b1 is sigma-multiplicative holds
b1 is sigma-additive
proof
let F be Subset-Family of X; ::_thesis: ( F is compl-closed & F is sigma-multiplicative implies F is sigma-additive )
assume that
A1: F is compl-closed and
A2: F is sigma-multiplicative ; ::_thesis: F is sigma-additive
let M be non empty V53() Subset-Family of X; :: according to MEASURE1:def_5 ::_thesis: ( M c= F implies union M in F )
assume A3: M c= F ; ::_thesis: union M in F
consider f being SetSequence of X such that
A4: M = rng f by SUPINF_2:def_8;
 for n being Nat holds (Complement f) . n in F
proof
let n be Nat; ::_thesis: (Complement f) . n in F
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 ( f . n in M & (Complement f) . n = (f . n) ` ) by A4, FUNCT_2:4, PROB_1:def_2;
hence  (Complement f) . n in F by A1, A3, PROB_1:def_1; ::_thesis: verum
end;
then  rng (Complement f) c= F by NAT_1:52;
then A5: Intersection (Complement f) in F by A2, PROB_1:def_6;
 (Intersection (Complement f)) ` = union M by A4, CARD_3:def_4;
hence  union M in F by A1, A5, PROB_1:def_1; ::_thesis: verum
end;
cluster compl-closed sigma-additive  ->  sigma-multiplicative for Element of bool (bool X);
coherence
 for b1 being Subset-Family of X st b1 is compl-closed & b1 is sigma-additive holds
b1 is sigma-multiplicative
proof
let F be Subset-Family of X; ::_thesis: ( F is compl-closed & F is sigma-additive implies F is sigma-multiplicative )
assume that
A6: F is compl-closed and
A7: F is sigma-additive ; ::_thesis: F is sigma-multiplicative
let f be SetSequence of X; :: according to PROB_1:def_6 ::_thesis: ( not rng f c= F or Intersection f in F )
assume A8: rng f c= F ; ::_thesis: Intersection f in F
 dom (Complement f) = NAT by FUNCT_2:def_1;
then reconsider M = rng (Complement f) as non empty V53() Subset-Family of X by CARD_3:93;
 M c= F
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in M or e in F )
assume  e in M ; ::_thesis: e in F
then consider n being set  such that
A9: n in NAT and
A10: e = (Complement f) . n by FUNCT_2:11;
reconsider n = n as Element of NAT by A9;
A11: f . n in rng f by NAT_1:51;
 e = (f . n) ` by A10, PROB_1:def_2;
hence  e in F by A6, A8, A11, PROB_1:def_1; ::_thesis: verum
end;
then  ( Intersection f = (union M) ` & union M in F ) by A7, Def5, CARD_3:def_4;
hence  Intersection f in F by A6, PROB_1:def_1; ::_thesis: verum
end;
end;

registration
let X be set ;
cluster non empty compl-closed sigma-multiplicative  ->  for Element of bool (bool X);
coherence
 for b1 being SigmaField of X holds not b1 is empty ;
end;

theorem Th22: :: MEASURE1:22
for X being set
for S being non empty Subset-Family of X holds
( ( ( for A being set st A in S holds
X \ A in S ) & ( for M being N_Sub_set_fam of X st M c= S holds
meet M in S ) ) iff S is SigmaField of X )
proof
let X be set ; ::_thesis: for S being non empty Subset-Family of X holds
( ( ( for A being set st A in S holds
X \ A in S ) & ( for M being N_Sub_set_fam of X st M c= S holds
meet M in S ) ) iff S is SigmaField of X )
let S be non empty Subset-Family of X; ::_thesis: ( ( ( for A being set st A in S holds
X \ A in S ) & ( for M being N_Sub_set_fam of X st M c= S holds
meet M in S ) ) iff S is SigmaField of X )
hereby  ::_thesis: ( S is SigmaField of X implies ( ( for A being set st A in S holds
X \ A in S ) & ( for M being N_Sub_set_fam of X st M c= S holds
meet M in S ) ) )
assume that
A1: for A being set st A in S holds
X \ A in S and
A2: for M being N_Sub_set_fam of X st M c= S holds
meet M in S ; ::_thesis: S is SigmaField of X
 for M being N_Sub_set_fam of X st M c= S holds
union M in S
proof
let M be N_Sub_set_fam of X; ::_thesis: ( M c= S implies union M in S )
assume A3: M c= S ; ::_thesis: union M in S
A4: X \ M c= S
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X \ M or y in S )
assume A5: y in X \ M ; ::_thesis: y in S
then reconsider B = y as Subset of X ;
 B ` in M by A5, SETFAM_1:def_7;
then  (B `) ` in S by A1, A3;
hence  y in S ; ::_thesis: verum
end;
 X \ M is N_Sub_set_fam of X by Th21;
then  X \ (meet (X \ M)) in S by A1, A2, A4;
hence  union M in S by Th4; ::_thesis: verum
end;
then reconsider S9 = S as non empty compl-closed sigma-additive Subset-Family of X by A1, Def1, Def5;
 S9 is SigmaField of X ;
hence  S is SigmaField of X ; ::_thesis: verum
end;
assume A6: S is SigmaField of X ; ::_thesis: ( ( for A being set st A in S holds
X \ A in S ) & ( for M being N_Sub_set_fam of X st M c= S holds
meet M in S ) )
 for M being N_Sub_set_fam of X st M c= S holds
meet M in S
proof
let M be N_Sub_set_fam of X; ::_thesis: ( M c= S implies meet M in S )
assume A7: M c= S ; ::_thesis: meet M in S
A8: X \ M c= S
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X \ M or y in S )
assume A9: y in X \ M ; ::_thesis: y in S
then reconsider B = y as Subset of X ;
 B ` in M by A9, SETFAM_1:def_7;
then  (B `) ` in S by A6, A7, PROB_1:def_1;
hence  y in S ; ::_thesis: verum
end;
 X \ M is N_Sub_set_fam of X by Th21;
then  union (X \ M) in S by A6, A8, Def5;
then  X \ (union (X \ M)) in S by A6, Def1;
hence  meet M in S by Th4; ::_thesis: verum
end;
hence  ( ( for A being set st A in S holds
X \ A in S ) & ( for M being N_Sub_set_fam of X st M c= S holds
meet M in S ) ) by A6, Def1; ::_thesis: verum
end;

registration
let X be set ;
let S be SigmaField of X;
cluster Relation-like NAT -defined S -valued Function-like non empty V14( NAT ) V18( NAT ,S) disjoint_valued for Element of bool [:NAT,S:];
existence
 ex b1 being Function of NAT,S st b1 is disjoint_valued
proof
consider F being Function of NAT,{{}} such that
A1: for n being Element of NAT holds F . n = {} by Th16;
 {} in S by PROB_1:4;
then  {{}} c= S by ZFMISC_1:31;
then reconsider F = F as Function of NAT,S by FUNCT_2:7;
take  F ; ::_thesis: F is disjoint_valued
A2: for n being set holds F . n = {}
proof
let n be set ; ::_thesis: F . n = {}
percases ( n in dom F or not n in dom F ) ;
suppose n in dom F ; ::_thesis: F . n = {}
hence  F . n = {} by A1; ::_thesis: verum
end;
suppose not n in dom F ; ::_thesis: F . n = {}
hence  F . n = {} by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
thus  for x, y being set st x <> y holds
F . x misses F . y :: according to PROB_2:def_2 ::_thesis: verum
proof
let x, y be set ; ::_thesis: ( x <> y implies F . x misses F . y )
 F . x = {} by A2;
hence  ( x <> y implies F . x misses F . y ) by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;

definition
let X be set ;
let S be SigmaField of X;
mode Sep_Sequence of S is disjoint_valued Function of NAT,S;
end;

definition
let X be set ;
let S be SigmaField of X;
let F be Function of NAT,S;
:: original: rng
redefine func rng F ->  non empty Subset-Family of X;
coherence
 rng F is non empty Subset-Family of X
proof
 rng F <> {} ;
hence  rng F is non empty Subset-Family of X by XBOOLE_1:1; ::_thesis: verum
end;
end;

theorem Th23: :: MEASURE1:23
for X being set
for S being SigmaField of X
for F being Function of NAT,S holds rng F is N_Sub_set_fam of X
proof
let X be set ; ::_thesis: for S being SigmaField of X
for F being Function of NAT,S holds rng F is N_Sub_set_fam of X
let S be SigmaField of X; ::_thesis: for F being Function of NAT,S holds rng F is N_Sub_set_fam of X
let F be Function of NAT,S; ::_thesis: rng F is N_Sub_set_fam of X
 ex H being Function of NAT,(bool X) st rng F = rng H
proof
 rng F c= bool X ;
then reconsider F = F as Function of NAT,(bool X) by FUNCT_2:6;
take  F ; ::_thesis: rng F = rng F
thus  rng F = rng F ; ::_thesis: verum
end;
hence  rng F is N_Sub_set_fam of X by SUPINF_2:def_8; ::_thesis: verum
end;

theorem Th24: :: MEASURE1:24
for X being set
for S being SigmaField of X
for F being Function of NAT,S holds union (rng F) is Element of S
proof
let X be set ; ::_thesis: for S being SigmaField of X
for F being Function of NAT,S holds union (rng F) is Element of S
let S be SigmaField of X; ::_thesis: for F being Function of NAT,S holds union (rng F) is Element of S
let F be Function of NAT,S; ::_thesis: union (rng F) is Element of S
 ( rng F is N_Sub_set_fam of X & rng F c= S ) by Th23, RELAT_1:def_19;
hence  union (rng F) is Element of S by Def5; ::_thesis: verum
end;

theorem Th25: :: MEASURE1:25
for Y, S being non empty set
for F being Function of Y,S
for M being Function of S,ExtREAL st M is V89() holds
M * F is V89()
proof
let Y, S be non empty set ; ::_thesis: for F being Function of Y,S
for M being Function of S,ExtREAL st M is V89() holds
M * F is V89()
let F be Function of Y,S; ::_thesis: for M being Function of S,ExtREAL st M is V89() holds
M * F is V89()
let M be Function of S,ExtREAL; ::_thesis: ( M is V89() implies M * F is V89() )
assume A1: M is V89() ; ::_thesis: M * F is V89()
 for n being Element of Y holds 0. <= (M * F) . n
proof
let n be Element of Y; ::_thesis: 0. <= (M * F) . n
 dom (M * F) = Y by FUNCT_2:def_1;
then  (M * F) . n = M . (F . n) by FUNCT_1:12;
hence  0. <= (M * F) . n by A1, Def2; ::_thesis: verum
end;
hence  M * F is V89() by SUPINF_2:39; ::_thesis: verum
end;

theorem Th26: :: MEASURE1:26
for X being set
for S being SigmaField of X
for a, b being R_eal ex M being Function of S,ExtREAL st
for A being Element of S holds
( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) )
proof
let X be set ; ::_thesis: for S being SigmaField of X
for a, b being R_eal ex M being Function of S,ExtREAL st
for A being Element of S holds
( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) )
let S be SigmaField of X; ::_thesis: for a, b being R_eal ex M being Function of S,ExtREAL st
for A being Element of S holds
( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) )
let a, b be R_eal; ::_thesis: ex M being Function of S,ExtREAL st
for A being Element of S holds
( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) )
defpred S1[ set , set ] means ( ( $1 = {} implies $2 = a ) & ( $1 <> {} implies $2 = b ) );
A1: for x being set st x in S holds
ex y being set st
( y in ExtREAL & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in S implies ex y being set st
( y in ExtREAL & S1[x,y] ) )
 ( x <> {} implies ex y being set st
( y in ExtREAL & S1[x,y] ) ) ;
hence  ( x in S implies ex y being set st
( y in ExtREAL & S1[x,y] ) ) ; ::_thesis: verum
end;
 ex F being Function of S,ExtREAL st
for x being set st x in S holds
S1[x,F . x] from FUNCT_2:sch_1(A1);
then consider M being Function of S,ExtREAL such that
A2: for x being set st x in S holds
S1[x,M . x] ;
take  M ; ::_thesis: for A being Element of S holds
( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) )
thus  for A being Element of S holds
( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) ) by A2; ::_thesis: verum
end;

theorem :: MEASURE1:27
for X being set
for S being SigmaField of X ex M being Function of S,ExtREAL st
for A being Element of S holds
( ( A = {} implies M . A = 0. ) & ( A <> {} implies M . A = +infty ) ) by Th26;

theorem Th28: :: MEASURE1:28
for X being set
for S being SigmaField of X ex M being Function of S,ExtREAL st
for A being Element of S holds M . A = 0.
proof
let X be set ; ::_thesis: for S being SigmaField of X ex M being Function of S,ExtREAL st
for A being Element of S holds M . A = 0.
let S be SigmaField of X; ::_thesis: ex M being Function of S,ExtREAL st
for A being Element of S holds M . A = 0.
consider M being Function of S,ExtREAL such that
A1: for A being Element of S holds
( ( A = {} implies M . A = 0. ) & ( A <> {} implies M . A = 0. ) ) by Th26;
take  M ; ::_thesis: for A being Element of S holds M . A = 0.
thus  for A being Element of S holds M . A = 0. by A1; ::_thesis: verum
end;

definition
let X be set ;
let S be SigmaField of X;
let F be Function of S,ExtREAL;
attrF is sigma-additive  means :Def6: :: MEASURE1:def 6
 for s being Sep_Sequence of S holds SUM (F * s) = F . (union (rng s));
end;

:: deftheorem Def6 defines sigma-additive MEASURE1:def_6_:_
 for X being set
for S being SigmaField of X
for F being Function of S,ExtREAL holds
( F is sigma-additive iff for s being Sep_Sequence of S holds SUM (F * s) = F . (union (rng s)) );

registration
let X be set ;
let S be SigmaField of X;
cluster Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed V89() sigma-additive for Element of bool [:S,ExtREAL:];
existence
 ex b1 being Function of S,ExtREAL st
( b1 is V89() & b1 is sigma-additive & b1 is zeroed )
proof
consider M being Function of S,ExtREAL such that
A1: for A being Element of S holds M . A = 0. by Th28;
take  M ; ::_thesis: ( M is V89() & M is sigma-additive & M is zeroed )
 for A being Element of S holds 0. <= M . A by A1;
hence A2: M is V89() by Def2; ::_thesis: ( M is sigma-additive & M is zeroed )
thus  M is sigma-additive ::_thesis: M is zeroed
proof
let F be Sep_Sequence of S; :: according to MEASURE1:def_6 ::_thesis: SUM (M * F) = M . (union (rng F))
A3: for r being Element of NAT st 0 <= r holds
(M * F) . r = 0.
proof
let r be Element of NAT ; ::_thesis: ( 0 <= r implies (M * F) . r = 0. )
 dom (M * F) = NAT by FUNCT_2:def_1;
then  (M * F) . r = M . (F . r) by FUNCT_1:12;
hence  ( 0 <= r implies (M * F) . r = 0. ) by A1; ::_thesis: verum
end;
 M * F is V89() by A2, Th25;
then A4: SUM (M * F) = (Ser (M * F)) . 0 by A3, SUPINF_2:48;
 union (rng F) is Element of S by Th24;
then A5: M . (union (rng F)) = 0. by A1;
 (Ser (M * F)) . 0 = (M * F) . 0 by SUPINF_2:44;
hence  SUM (M * F) = M . (union (rng F)) by A5, A3, A4; ::_thesis: verum
end;
 {} is Element of S by PROB_1:4;
then  M . {} = 0. by A1;
hence  M is zeroed by VALUED_0:def_19; ::_thesis: verum
end;
end;

definition
let X be set ;
let S be SigmaField of X;
mode sigma_Measure of S is zeroed V89() sigma-additive Function of S,ExtREAL;
end;

registration
let X be set ;
cluster non empty compl-closed sigma-additive  ->  non empty cup-closed for Element of bool (bool X);
coherence
 for b1 being non empty Subset-Family of X st b1 is sigma-additive & b1 is compl-closed holds
b1 is cup-closed ;
end;

theorem Th29: :: MEASURE1:29
for X being set
for S being SigmaField of X
for M being sigma_Measure of S holds M is Measure of S
proof
let X be set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S holds M is Measure of S
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S holds M is Measure of S
let M be sigma_Measure of S; ::_thesis: M is Measure of S
 for A, B being Element of S st A misses B holds
M . (A \/ B) = (M . A) + (M . B)
proof
set n2 = 1 + 1;
let A, B be Element of S; ::_thesis: ( A misses B implies M . (A \/ B) = (M . A) + (M . B) )
assume A1: A misses B ; ::_thesis: M . (A \/ B) = (M . A) + (M . B)
A2: ( A in S & B in S ) ;
reconsider A = A, B = B as Subset of X ;
 {} is Subset of X by XBOOLE_1:2;
then consider F being Function of NAT,(bool X) such that
A3: rng F = {A,B,{}} and
A4: ( F . 0 = A & F . 1 = B ) and
A5: for n being Element of NAT st 1 < n holds
F . n = {} by Th17;
 {} in S by PROB_1:4;
then  for x being set st x in {A,B,{}} holds
x in S by A2, ENUMSET1:def_1;
then  {A,B,{}} c= S by TARSKI:def_3;
then reconsider F = F as Function of NAT,S by A3, FUNCT_2:6;
A6: for n, m being Element of NAT st n <> m holds
F . n misses F . m
proof
let n, m be Element of NAT ; ::_thesis: ( n <> m implies F . n misses F . m )
A7: ( n = 0 or n = 1 or 1 < n ) by NAT_1:25;
A8: ( m = 0 or m = 1 or 1 < m ) by NAT_1:25;
A9: ( 1 < n & m = 1 implies F . n misses F . m )
proof
assume that
A10: 1 < n and
 m = 1 ; ::_thesis: F . n misses F . m
 F . n = {} by A5, A10;
then  (F . n) /\ (F . m) = {} ;
hence  F . n misses F . m by XBOOLE_0:def_7; ::_thesis: verum
end;
A11: ( 1 < n & m = 0 implies F . n misses F . m )
proof
assume that
A12: 1 < n and
 m = 0 ; ::_thesis: F . n misses F . m
 F . n = {} by A5, A12;
then  (F . n) /\ (F . m) = {} ;
hence  F . n misses F . m by XBOOLE_0:def_7; ::_thesis: verum
end;
A13: ( 1 < n & 1 < m implies F . n misses F . m )
proof
assume that
A14: 1 < n and
 1 < m ; ::_thesis: F . n misses F . m
 F . n = {} by A5, A14;
then  (F . n) /\ (F . m) = {} ;
hence  F . n misses F . m by XBOOLE_0:def_7; ::_thesis: verum
end;
A15: ( n = 1 & 1 < m implies F . n misses F . m )
proof
assume that
 n = 1 and
A16: 1 < m ; ::_thesis: F . n misses F . m
 F . m = {} by A5, A16;
then  (F . n) /\ (F . m) = {} ;
hence  F . n misses F . m by XBOOLE_0:def_7; ::_thesis: verum
end;
A17: ( n = 0 & 1 < m implies F . n misses F . m )
proof
assume that
 n = 0 and
A18: 1 < m ; ::_thesis: F . n misses F . m
 F . m = {} by A5, A18;
then  (F . n) /\ (F . m) = {} ;
hence  F . n misses F . m by XBOOLE_0:def_7; ::_thesis: verum
end;
assume  n <> m ; ::_thesis: F . n misses F . m
hence  F . n misses F . m by A1, A4, A7, A8, A17, A15, A11, A9, A13; ::_thesis: verum
end;
 for m, n being set st m <> n holds
F . m misses F . n
proof
let m, n be set ; ::_thesis: ( m <> n implies F . m misses F . n )
assume A19: m <> n ; ::_thesis: F . m misses F . n
percases ( ( m in NAT & n in NAT ) or not m in NAT or not n in NAT ) ;
suppose ( m in NAT & n in NAT ) ; ::_thesis: F . m misses F . n
hence  F . m misses F . n by A6, A19; ::_thesis: verum
end;
suppose ( not m in NAT or not n in NAT ) ; ::_thesis: F . m misses F . n
then  ( not m in dom F or not n in dom F ) ;
then  ( F . m = {} or F . n = {} ) by FUNCT_1:def_2;
hence  F . m misses F . n by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
then reconsider F = F as disjoint_valued Function of NAT,S by PROB_2:def_2;
 union {A,B,{}} = union {A,B} by Th1;
then A20: union (rng F) = A \/ B by A3, ZFMISC_1:75;
A21: for r being Element of NAT holds
( (M * F) . 0 = M . A & (M * F) . 1 = M . B & ( 1 + 1 <= r implies (M * F) . r = 0. ) )
proof
let r be Element of NAT ; ::_thesis: ( (M * F) . 0 = M . A & (M * F) . 1 = M . B & ( 1 + 1 <= r implies (M * F) . r = 0. ) )
A22: for r being Element of NAT holds (M * F) . r = M . (F . r)
proof
let r be Element of NAT ; ::_thesis: (M * F) . r = M . (F . r)
 dom (M * F) = NAT by FUNCT_2:def_1;
hence  (M * F) . r = M . (F . r) by FUNCT_1:12; ::_thesis: verum
end;
 ( 1 + 1 <= r implies (M * F) . r = 0. )
proof
assume  1 + 1 <= r ; ::_thesis: (M * F) . r = 0.
then  1 < r by NAT_1:13;
then  F . r = {} by A5;
then  (M * F) . r = M . {} by A22;
hence  (M * F) . r = 0. by VALUED_0:def_19; ::_thesis: verum
end;
hence  ( (M * F) . 0 = M . A & (M * F) . 1 = M . B & ( 1 + 1 <= r implies (M * F) . r = 0. ) ) by A4, A22; ::_thesis: verum
end;
set H = M * F;
A23: 0 + 1 = 0 + 1 ;
set y1 = (Ser (M * F)) . 1;
A24: M * F is V89() by Th25;
reconsider A = A, B = B as Element of S ;
 (Ser (M * F)) . (1 + 1) = ((Ser (M * F)) . 1) + ((M * F) . (1 + 1)) by SUPINF_2:44;
then (Ser (M * F)) . (1 + 1) = ((Ser (M * F)) . 1) + 0. by A21
.= (Ser (M * F)) . 1 by XXREAL_3:4
.= ((Ser (M * F)) . 0) + ((M * F) . 1) by A23, SUPINF_2:44
.= (M . A) + (M . B) by A21, SUPINF_2:44 ;
then  SUM (M * F) = (M . A) + (M . B) by A21, A24, SUPINF_2:48;
hence  M . (A \/ B) = (M . A) + (M . B) by A20, Def6; ::_thesis: verum
end;
hence  M is Measure of S by Def3; ::_thesis: verum
end;

theorem :: MEASURE1:30
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for A, B being Element of S st A misses B holds
M . (A \/ B) = (M . A) + (M . B)
proof
let X be set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for A, B being Element of S st A misses B holds
M . (A \/ B) = (M . A) + (M . B)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for A, B being Element of S st A misses B holds
M . (A \/ B) = (M . A) + (M . B)
let M be sigma_Measure of S; ::_thesis: for A, B being Element of S st A misses B holds
M . (A \/ B) = (M . A) + (M . B)
let A, B be Element of S; ::_thesis: ( A misses B implies M . (A \/ B) = (M . A) + (M . B) )
assume A1: A misses B ; ::_thesis: M . (A \/ B) = (M . A) + (M . B)
 M is Measure of S by Th29;
hence  M . (A \/ B) = (M . A) + (M . B) by A1, Def3; ::_thesis: verum
end;

theorem Th31: :: MEASURE1:31
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for A, B being Element of S st A c= B holds
M . A <= M . B
proof
let X be set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for A, B being Element of S st A c= B holds
M . A <= M . B
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for A, B being Element of S st A c= B holds
M . A <= M . B
let M be sigma_Measure of S; ::_thesis: for A, B being Element of S st A c= B holds
M . A <= M . B
let A, B be Element of S; ::_thesis: ( A c= B implies M . A <= M . B )
assume A1: A c= B ; ::_thesis: M . A <= M . B
 M is Measure of S by Th29;
hence  M . A <= M . B by A1, Th8; ::_thesis: verum
end;

theorem :: MEASURE1:32
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for A, B being Element of S st A c= B & M . A < +infty holds
M . (B \ A) = (M . B) - (M . A)
proof
let X be set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for A, B being Element of S st A c= B & M . A < +infty holds
M . (B \ A) = (M . B) - (M . A)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for A, B being Element of S st A c= B & M . A < +infty holds
M . (B \ A) = (M . B) - (M . A)
let M be sigma_Measure of S; ::_thesis: for A, B being Element of S st A c= B & M . A < +infty holds
M . (B \ A) = (M . B) - (M . A)
let A, B be Element of S; ::_thesis: ( A c= B & M . A < +infty implies M . (B \ A) = (M . B) - (M . A) )
assume A1: ( A c= B & M . A < +infty ) ; ::_thesis: M . (B \ A) = (M . B) - (M . A)
 M is Measure of S by Th29;
hence  M . (B \ A) = (M . B) - (M . A) by A1, Th9; ::_thesis: verum
end;

theorem Th33: :: MEASURE1:33
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)
proof
let X be set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)
let M be sigma_Measure of S; ::_thesis: for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)
let A, B be Element of S; ::_thesis: M . (A \/ B) <= (M . A) + (M . B)
 M is Measure of S by Th29;
hence  M . (A \/ B) <= (M . A) + (M . B) by Th10; ::_thesis: verum
end;

theorem :: MEASURE1:34
for X being set
for S being SigmaField of X
for M being sigma_Measure of S holds
( {} in S & X in S & ( for A, B being set st A in S & B in S holds
( X \ A in S & A \/ B in S & A /\ B in S ) ) ) by Def1, FINSUB_1:def_1, FINSUB_1:def_2, PROB_1:4, PROB_1:5;

theorem :: MEASURE1:35
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for T being N_Sub_set_fam of X st ( for A being set st A in T holds
A in S ) holds
( union T in S & meet T in S )
proof
let X be set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for T being N_Sub_set_fam of X st ( for A being set st A in T holds
A in S ) holds
( union T in S & meet T in S )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for T being N_Sub_set_fam of X st ( for A being set st A in T holds
A in S ) holds
( union T in S & meet T in S )
let M be sigma_Measure of S; ::_thesis: for T being N_Sub_set_fam of X st ( for A being set st A in T holds
A in S ) holds
( union T in S & meet T in S )
let T be N_Sub_set_fam of X; ::_thesis: ( ( for A being set st A in T holds
A in S ) implies ( union T in S & meet T in S ) )
assume A1: for A being set st A in T holds
A in S ; ::_thesis: ( union T in S & meet T in S )
 T c= S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T or x in S )
assume  x in T ; ::_thesis: x in S
hence  x in S by A1; ::_thesis: verum
end;
hence  ( union T in S & meet T in S ) by Def5, Th22; ::_thesis: verum
end;

definition
let X be set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
mode measure_zero of M ->  Element of S means :Def7: :: MEASURE1:def 7
M . it = 0. ;
existence
 ex b1 being Element of S st M . b1 = 0.
proof
 {} is Element of S by PROB_1:4;
then consider A being Element of S such that
A1: A = {} ;
take  A ; ::_thesis: M . A = 0.
thus  M . A = 0. by A1, VALUED_0:def_19; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines measure_zero MEASURE1:def_7_:_
 for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being Element of S holds
( b4 is measure_zero of M iff M . b4 = 0. );

theorem :: MEASURE1:36
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for B being measure_zero of M st A c= B holds
A is measure_zero of M
proof
let X be set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for B being measure_zero of M st A c= B holds
A is measure_zero of M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for A being Element of S
for B being measure_zero of M st A c= B holds
A is measure_zero of M
let M be sigma_Measure of S; ::_thesis: for A being Element of S
for B being measure_zero of M st A c= B holds
A is measure_zero of M
let A be Element of S; ::_thesis: for B being measure_zero of M st A c= B holds
A is measure_zero of M
let B be measure_zero of M; ::_thesis: ( A c= B implies A is measure_zero of M )
assume  A c= B ; ::_thesis: A is measure_zero of M
then  M . A <= M . B by Th31;
then A1: M . A <= 0. by Def7;
 0. <= M . A by Def2;
then  M . A = 0. by A1, XXREAL_0:1;
hence  A is measure_zero of M by Def7; ::_thesis: verum
end;

theorem :: MEASURE1:37
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for A, B being measure_zero of M holds
( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )
proof
let X be set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for A, B being measure_zero of M holds
( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for A, B being measure_zero of M holds
( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )
let M be sigma_Measure of S; ::_thesis: for A, B being measure_zero of M holds
( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )
let A, B be measure_zero of M; ::_thesis: ( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )
A1: 0. <= M . (A /\ B) by Def2;
A2: 0. <= M . (A \ B) by Def2;
A3: M . A = 0. by Def7;
then  M . (A \ B) <= 0. by Th31, XBOOLE_1:36;
then A4: M . (A \ B) = 0. by A2, XXREAL_0:1;
 M . B = 0. by Def7;
then  M . (A \/ B) <= 0. + 0. by A3, Th33;
then A5: M . (A \/ B) <= 0. by XXREAL_3:4;
 0. <= M . (A \/ B) by Def2;
then A6: M . (A \/ B) = 0. by A5, XXREAL_0:1;
 M . (A /\ B) <= 0. by A3, Th31, XBOOLE_1:17;
then  M . (A /\ B) = 0. by A1, XXREAL_0:1;
hence  ( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M ) by A6, A4, Def7; ::_thesis: verum
end;

theorem :: MEASURE1:38
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for B being measure_zero of M holds
( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )
proof
let X be set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for B being measure_zero of M holds
( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for A being Element of S
for B being measure_zero of M holds
( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )
let M be sigma_Measure of S; ::_thesis: for A being Element of S
for B being measure_zero of M holds
( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )
let A be Element of S; ::_thesis: for B being measure_zero of M holds
( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )
let B be measure_zero of M; ::_thesis: ( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )
A1: M . A = M . ((A /\ B) \/ (A \ B)) by XBOOLE_1:51;
A2: M . B = 0. by Def7;
then A3: M . (A /\ B) <= 0. by Th31, XBOOLE_1:17;
A4: 0. <= M . (A /\ B) by Def2;
then  M . (A /\ B) = 0. by A3, XXREAL_0:1;
then  M . A <= 0. + (M . (A \ B)) by A1, Th33;
then A5: M . A <= M . (A \ B) by XXREAL_3:4;
 M . (A \/ B) <= (M . A) + 0. by A2, Th33;
then A6: M . (A \/ B) <= M . A by XXREAL_3:4;
 ( M . A <= M . (A \/ B) & M . (A \ B) <= M . A ) by Th31, XBOOLE_1:7, XBOOLE_1:36;
hence  ( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A ) by A4, A6, A3, A5, XXREAL_0:1; ::_thesis: verum
end;