:: PROB_4 semantic presentation

begin

            Lm1:  for A, B, C being set st C c= B holds
A \ C = (A \ B) \/ (A /\ (B \ C))
proof
let A, B, C be set ; ::_thesis: ( C c= B implies A \ C = (A \ B) \/ (A /\ (B \ C)) )
assume A1: C c= B ; ::_thesis: A \ C = (A \ B) \/ (A /\ (B \ C))
thus  A \ C c= (A \ B) \/ (A /\ (B \ C)) :: according to XBOOLE_0:def_10 ::_thesis: (A \ B) \/ (A /\ (B \ C)) c= A \ C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A \ C or x in (A \ B) \/ (A /\ (B \ C)) )
assume  x in A \ C ; ::_thesis: x in (A \ B) \/ (A /\ (B \ C))
then  ( ( x in A & not x in B ) or ( x in A & x in B & not x in C ) ) by XBOOLE_0:def_5;
then  ( x in A \ B or ( x in A & x in B \ C ) ) by XBOOLE_0:def_5;
then  ( x in A \ B or x in A /\ (B \ C) ) by XBOOLE_0:def_4;
hence  x in (A \ B) \/ (A /\ (B \ C)) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A \ B) \/ (A /\ (B \ C)) or x in A \ C )
assume  x in (A \ B) \/ (A /\ (B \ C)) ; ::_thesis: x in A \ C
then  ( x in A \ B or x in A /\ (B \ C) ) by XBOOLE_0:def_3;
then A2: ( x in A \ B or ( x in A & x in B \ C ) ) by XBOOLE_0:def_4;
then  not x in C by A1, XBOOLE_0:def_5;
hence  x in A \ C by A2, XBOOLE_0:def_5; ::_thesis: verum
end;

definition
let X be set ;
let Si be SigmaField of X;
let XSeq be SetSequence of Si;
let n be Element of NAT ;
:: original: .
redefine funcXSeq . n ->  Element of Si;
coherence
 XSeq . n is Element of Si
proof
thus  XSeq . n is Element of Si ; ::_thesis: verum
end;
end;

theorem Th1: :: PROB_4:1
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds rng XSeq c= Si
proof
let X be set ; ::_thesis: for Si being SigmaField of X
for XSeq being SetSequence of Si holds rng XSeq c= Si
let Si be SigmaField of X; ::_thesis: for XSeq being SetSequence of Si holds rng XSeq c= Si
let XSeq be SetSequence of Si; ::_thesis: rng XSeq c= Si
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng XSeq or x in Si )
assume  x in rng XSeq ; ::_thesis: x in Si
then  ex n being Element of NAT st x = XSeq . n by SETLIM_1:4;
hence  x in Si ; ::_thesis: verum
end;

theorem Th2: :: PROB_4:2
for X being set
for Si being SigmaField of X
for f being Function holds
( f is SetSequence of Si iff f is Function of NAT,Si )
proof
let X be set ; ::_thesis: for Si being SigmaField of X
for f being Function holds
( f is SetSequence of Si iff f is Function of NAT,Si )
let Si be SigmaField of X; ::_thesis: for f being Function holds
( f is SetSequence of Si iff f is Function of NAT,Si )
let f be Function; ::_thesis: ( f is SetSequence of Si iff f is Function of NAT,Si )
thus  ( f is SetSequence of Si implies f is Function of NAT,Si ) ::_thesis: ( f is Function of NAT,Si implies f is SetSequence of Si )
proof
assume  f is SetSequence of Si ; ::_thesis: f is Function of NAT,Si
then reconsider f = f as SetSequence of Si ;
 ( rng f c= Si & dom f = NAT ) by Th1, FUNCT_2:def_1;
hence  f is Function of NAT,Si by FUNCT_2:2; ::_thesis: verum
end;
assume A1: f is Function of NAT,Si ; ::_thesis: f is SetSequence of Si
then reconsider f = f as SetSequence of X by FUNCT_2:7;
 f is SetSequence of Si by A1;
hence  f is SetSequence of Si ; ::_thesis: verum
end;

scheme :: PROB_4:sch 1
LambdaSigmaSSeq{ F1() ->  set , F2() ->  SigmaField of F1(), F3( set ) ->  Element of F2() } :
 ex f being SetSequence of F2() st
for n being Element of NAT holds f . n = F3(n)
proof
 ex f being SetSequence of F1() st
for n being Element of NAT holds f . n = F3(n) from FUNCT_2:sch_4();
then consider f being SetSequence of F1() such that
A1: for n being Element of NAT holds f . n = F3(n) ;
 for n being Nat holds f . n in F2()
proof
let n be Nat; ::_thesis: f . n in F2()
 n in NAT by ORDINAL1:def_12;
then  f . n = F3(n) by A1;
hence  f . n in F2() ; ::_thesis: verum
end;
then  rng f c= F2() by NAT_1:52;
then reconsider f = f as SetSequence of F2() by RELAT_1:def_19;
take  f ; ::_thesis: for n being Element of NAT holds f . n = F3(n)
thus  for n being Element of NAT holds f . n = F3(n) by A1; ::_thesis: verum
end;

registration
let X be set ;
cluster non empty V13() V16( NAT ) V17( bool X) Function-like V23( NAT ) V27( NAT , bool X) V118() for Element of bool [:NAT,(bool X):];
existence
 not for b1 being SetSequence of X holds b1 is V118()
proof
take A1 = NAT --> ({} X); ::_thesis: A1 is V118()
 for m, n being Nat st m <> n holds
A1 . m misses A1 . n
proof
let m, n be Nat; ::_thesis: ( m <> n implies A1 . m misses A1 . n )
 m in NAT by ORDINAL1:def_12;
then  A1 . m = {} by FUNCOP_1:7;
hence  ( m <> n implies A1 . m misses A1 . n ) by XBOOLE_1:65; ::_thesis: verum
end;
hence  A1 is V118() by PROB_3:def_4; ::_thesis: verum
end;
end;

registration
let X be set ;
let Si be SigmaField of X;
cluster non empty V13() V16( NAT ) V17(Si) V17( bool X) Function-like V23( NAT ) V27( NAT , bool X) V118() for Element of bool [:NAT,(bool X):];
existence
 not for b1 being SetSequence of Si holds b1 is V118()
proof
reconsider MSi = Si as SigmaField of X ;
set f = the disjoint_valued Function of NAT,MSi;
reconsider f = the disjoint_valued Function of NAT,MSi as SetSequence of Si by Th2;
take  f ; ::_thesis: f is V118()
thus  f is V118() ; ::_thesis: verum
end;
end;

theorem Th3: :: PROB_4:3
for X being set
for A, B being Subset of X st A misses B holds
(A,B) followed_by {} is disjoint_valued
proof
let X be set ; ::_thesis: for A, B being Subset of X st A misses B holds
(A,B) followed_by {} is disjoint_valued
let A, B be Subset of X; ::_thesis: ( A misses B implies (A,B) followed_by {} is disjoint_valued )
reconsider A1 = (A,B) followed_by ({} X) as SetSequence of X ;
assume A1: A misses B ; ::_thesis: (A,B) followed_by {} is disjoint_valued
 A1 is V118()
proof
A2: A1 . 1 = B by FUNCT_7:123;
let m, n be Nat; :: according to PROB_3:def_4 ::_thesis: ( m = n or A1 . m misses A1 . n )
assume A3: m <> n ; ::_thesis: A1 . m misses A1 . n
A4: A1 . 0 = A by FUNCT_7:122;
percases ( m = 0 or ( m <> 0 & m = 1 ) or ( m <> 0 & m <> 1 ) ) ;
supposeA5: m = 0 ; ::_thesis: A1 . m misses A1 . n
then  n >= 1 by A3, NAT_1:14;
then A6: n + 1 > 1 by NAT_1:13;
percases ( n > 1 or n = 1 ) by A6, NAT_1:22;
suppose n > 1 ; ::_thesis: A1 . m misses A1 . n
then  A1 . n = {} by FUNCT_7:124;
hence  A1 . m misses A1 . n by XBOOLE_1:65; ::_thesis: verum
end;
suppose n = 1 ; ::_thesis: A1 . m misses A1 . n
hence  A1 . m misses A1 . n by A1, A4, A5, FUNCT_7:123; ::_thesis: verum
end;
end;
end;
supposeA7: ( m <> 0 & m = 1 ) ; ::_thesis: A1 . m misses A1 . n
 ( n >= 1 or n <= 1 ) ;
then A8: ( n + 1 > 1 or n < 1 + 1 ) by NAT_1:13;
percases ( n > 1 or n = 0 ) by A3, A7, A8, NAT_1:14, NAT_1:22;
suppose n > 1 ; ::_thesis: A1 . m misses A1 . n
then  A1 . n = {} by FUNCT_7:124;
hence  A1 . m misses A1 . n by XBOOLE_1:65; ::_thesis: verum
end;
suppose n = 0 ; ::_thesis: A1 . m misses A1 . n
hence  A1 . m misses A1 . n by A1, A4, A2, A7; ::_thesis: verum
end;
end;
end;
supposeA9: ( m <> 0 & m <> 1 ) ; ::_thesis: A1 . m misses A1 . n
then  m >= 1 by NAT_1:14;
then  m + 1 > 1 by NAT_1:13;
then  A1 . m = {} by A9, FUNCT_7:124, NAT_1:22;
hence  A1 . m misses A1 . n by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
hence  (A,B) followed_by {} is disjoint_valued ; ::_thesis: verum
end;

theorem Th4: :: PROB_4:4
for X being set
for S being non empty set holds
( S is SigmaField of X iff ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) ) )
proof
let X be set ; ::_thesis: for S being non empty set holds
( S is SigmaField of X iff ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) ) )
let S be non empty set ; ::_thesis: ( S is SigmaField of X iff ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) ) )
thus  ( S is SigmaField of X implies ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) ) ) ::_thesis: ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) implies S is SigmaField of X )
proof
assume  S is SigmaField of X ; ::_thesis: ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) )
then reconsider S = S as SigmaField of X ;
 for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S
proof
let A1 be SetSequence of X; ::_thesis: ( rng A1 c= S implies Union A1 in S )
assume  rng A1 c= S ; ::_thesis: Union A1 in S
then reconsider A1 = A1 as SetSequence of S by RELAT_1:def_19;
 Union A1 in S by PROB_1:17;
hence  Union A1 in S ; ::_thesis: verum
end;
hence  ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) ) by PROB_1:15; ::_thesis: verum
end;
assume that
A1: S c= bool X and
A2: for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S and
A3: for A being Subset of X st A in S holds
A ` in S ; ::_thesis: S is SigmaField of X
 for A1 being SetSequence of X st rng A1 c= S holds
Intersection A1 in S
proof
let A1 be SetSequence of X; ::_thesis: ( rng A1 c= S implies Intersection A1 in S )
assume A4: rng A1 c= S ; ::_thesis: Intersection A1 in S
 for n being Nat holds (Complement A1) . n in S
proof
let n be Nat; ::_thesis: (Complement A1) . n in S
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
 A1 . n in rng A1 by NAT_1:51;
then  (A1 . n1) ` in S by A3, A4;
hence  (Complement A1) . n in S by PROB_1:def_2; ::_thesis: verum
end;
then  rng (Complement A1) c= S by NAT_1:52;
then  (Union (Complement A1)) ` in S by A2, A3;
hence  Intersection A1 in S by PROB_1:def_3; ::_thesis: verum
end;
hence  S is SigmaField of X by A1, A3, PROB_1:15; ::_thesis: verum
end;

theorem Th5: :: PROB_4:5
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being Event of Sigma holds P . (A \ B) = (P . (A \/ B)) - (P . B)
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being Event of Sigma holds P . (A \ B) = (P . (A \/ B)) - (P . B)
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for A, B being Event of Sigma holds P . (A \ B) = (P . (A \/ B)) - (P . B)
let P be Probability of Sigma; ::_thesis: for A, B being Event of Sigma holds P . (A \ B) = (P . (A \/ B)) - (P . B)
let A, B be Event of Sigma; ::_thesis: P . (A \ B) = (P . (A \/ B)) - (P . B)
 (P . (A \/ B)) - (P . B) = ((P . B) + (P . (A \ B))) - (P . B) by PROB_1:36;
hence  P . (A \ B) = (P . (A \/ B)) - (P . B) ; ::_thesis: verum
end;

theorem Th6: :: PROB_4:6
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being Event of Sigma st A c= B & P . B = 0 holds
P . A = 0
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being Event of Sigma st A c= B & P . B = 0 holds
P . A = 0
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for A, B being Event of Sigma st A c= B & P . B = 0 holds
P . A = 0
let P be Probability of Sigma; ::_thesis: for A, B being Event of Sigma st A c= B & P . B = 0 holds
P . A = 0
let A, B be Event of Sigma; ::_thesis: ( A c= B & P . B = 0 implies P . A = 0 )
assume  ( A c= B & P . B = 0 ) ; ::_thesis: P . A = 0
then  P . A <= 0 by PROB_1:34;
hence  P . A = 0 by PROB_1:def_8; ::_thesis: verum
end;

theorem Th7: :: PROB_4:7
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( ( for n being Element of NAT holds P . (ASeq . n) = 0 ) iff P . (Union ASeq) = 0 )
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( ( for n being Element of NAT holds P . (ASeq . n) = 0 ) iff P . (Union ASeq) = 0 )
let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( ( for n being Element of NAT holds P . (ASeq . n) = 0 ) iff P . (Union ASeq) = 0 )
let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma holds
( ( for n being Element of NAT holds P . (ASeq . n) = 0 ) iff P . (Union ASeq) = 0 )
let P be Probability of Sigma; ::_thesis: ( ( for n being Element of NAT holds P . (ASeq . n) = 0 ) iff P . (Union ASeq) = 0 )
hereby  ::_thesis: ( P . (Union ASeq) = 0 implies for n being Element of NAT holds P . (ASeq . n) = 0 )
assume A1: for n being Element of NAT holds P . (ASeq . n) = 0 ; ::_thesis: P . (Union ASeq) = 0
 for n being Element of NAT holds (Partial_Sums (P * ASeq)) . n = 0
proof
defpred S1[ Element of NAT ] means (Partial_Sums (P * ASeq)) . $1 = 0 ;
A2: 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 A3: S1[k] ; ::_thesis: S1[k + 1]
thus (Partial_Sums (P * ASeq)) . (k + 1) = ((Partial_Sums (P * ASeq)) . k) + ((P * ASeq) . (k + 1)) by SERIES_1:def_1
.= 0 + (P . (ASeq . (k + 1))) by A3, FUNCT_2:15
.= 0 by A1 ; ::_thesis: verum
end;
(Partial_Sums (P * ASeq)) . 0 = (P * ASeq) . 0 by SERIES_1:def_1
.= P . (ASeq . 0) by FUNCT_2:15
.= 0 by A1 ;
then A4: S1[ 0 ] ;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A2); ::_thesis: verum
end;
then  for n being Element of NAT st 0 <= n holds
(Partial_Sums (P * ASeq)) . n = 0 ;
then A5: ( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = 0 ) by PROB_1:1;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(P_*_(Partial_Diff_Union_ASeq))_._n_<=_(P_*_ASeq)_._n
let n be Element of NAT ; ::_thesis: (P * (Partial_Diff_Union ASeq)) . n <= (P * ASeq) . n
 (Partial_Diff_Union ASeq) . n c= ASeq . n by PROB_3:33;
hence  (P * (Partial_Diff_Union ASeq)) . n <= (P * ASeq) . n by PROB_3:5; ::_thesis: verum
end;
then A6: for n being Element of NAT holds (Partial_Sums (P * (Partial_Diff_Union ASeq))) . n <= (Partial_Sums (P * ASeq)) . n by SERIES_1:14;
 Partial_Sums (P * (Partial_Diff_Union ASeq)) is convergent by PROB_3:45;
then  Sum (P * (Partial_Diff_Union ASeq)) <= 0 by A5, A6, SEQ_2:18;
then  P . (Union (Partial_Diff_Union ASeq)) <= 0 by PROB_3:46;
then A7: P . (Union ASeq) <= 0 by PROB_3:36;
 Union ASeq is Event of Sigma by PROB_1:26;
hence  P . (Union ASeq) = 0 by A7, PROB_1:def_8; ::_thesis: verum
end;
assume A8: P . (Union ASeq) = 0 ; ::_thesis: for n being Element of NAT holds P . (ASeq . n) = 0
hereby  ::_thesis: verum
reconsider Y2 = Union ASeq as Event of Sigma by PROB_1:26;
let n be Element of NAT ; ::_thesis: P . (ASeq . n) = 0
reconsider Y1 = ASeq . n as Event of Sigma ;
 ASeq . n in rng ASeq by SETLIM_1:4;
then  ASeq . n c= union (rng ASeq) by ZFMISC_1:74;
then  Y1 c= Y2 by CARD_3:def_4;
hence  P . (ASeq . n) = 0 by A8, Th6; ::_thesis: verum
end;
end;

theorem Th8: :: PROB_4:8
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( ( for A being set st A in rng ASeq holds
P . A = 0 ) iff P . (union (rng ASeq)) = 0 )
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( ( for A being set st A in rng ASeq holds
P . A = 0 ) iff P . (union (rng ASeq)) = 0 )
let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( ( for A being set st A in rng ASeq holds
P . A = 0 ) iff P . (union (rng ASeq)) = 0 )
let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma holds
( ( for A being set st A in rng ASeq holds
P . A = 0 ) iff P . (union (rng ASeq)) = 0 )
let P be Probability of Sigma; ::_thesis: ( ( for A being set st A in rng ASeq holds
P . A = 0 ) iff P . (union (rng ASeq)) = 0 )
hereby  ::_thesis: ( P . (union (rng ASeq)) = 0 implies for A being set st A in rng ASeq holds
P . A = 0 )
assume A1: for A being set st A in rng ASeq holds
P . A = 0 ; ::_thesis: P . (union (rng ASeq)) = 0
 for n being Element of NAT holds P . (ASeq . n) = 0
proof
let n be Element of NAT ; ::_thesis: P . (ASeq . n) = 0
 ASeq . n in rng ASeq by SETLIM_1:4;
hence  P . (ASeq . n) = 0 by A1; ::_thesis: verum
end;
then  P . (Union ASeq) = 0 by Th7;
hence  P . (union (rng ASeq)) = 0 by CARD_3:def_4; ::_thesis: verum
end;
assume  P . (union (rng ASeq)) = 0 ; ::_thesis: for A being set st A in rng ASeq holds
P . A = 0
then A2: P . (Union ASeq) = 0 by CARD_3:def_4;
hereby  ::_thesis: verum
let A be set ; ::_thesis: ( A in rng ASeq implies P . A = 0 )
assume  A in rng ASeq ; ::_thesis: P . A = 0
then  ex n1 being Element of NAT st A = ASeq . n1 by SETLIM_1:4;
hence  P . A = 0 by A2, Th7; ::_thesis: verum
end;
end;

theorem Th9: :: PROB_4:9
for seq being Function of NAT,REAL
for Eseq being Function of NAT,ExtREAL st seq = Eseq holds
Partial_Sums seq = Ser Eseq
proof
let seq be Function of NAT,REAL; ::_thesis: for Eseq being Function of NAT,ExtREAL st seq = Eseq holds
Partial_Sums seq = Ser Eseq
let Eseq be Function of NAT,ExtREAL; ::_thesis: ( seq = Eseq implies Partial_Sums seq = Ser Eseq )
assume A1: seq = Eseq ; ::_thesis: Partial_Sums seq = Ser Eseq
reconsider Ps = Partial_Sums seq as Function of NAT,ExtREAL by FUNCT_2:7, NUMBERS:31;
defpred S1[ Element of NAT ] means Ps . $1 = (Ser Eseq) . $1;
A2: 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 A3: Ps . k = (Ser Eseq) . k ; ::_thesis: S1[k + 1]
 Ps . k = (Partial_Sums seq) . k ;
then reconsider Psk = Ps . k as Real ;
 ( Ps . (k + 1) = Psk + (seq . (k + 1)) & (Ser Eseq) . (k + 1) = ((Ser Eseq) . k) + (Eseq . (k + 1)) ) by SERIES_1:def_1, SUPINF_2:44;
hence  S1[k + 1] by A1, A3, SUPINF_2:1; ::_thesis: verum
end;
Ps . 0 = Eseq . 0 by A1, SERIES_1:def_1
.= (Ser Eseq) . 0 by SUPINF_2:44 ;
then A4: S1[ 0 ] ;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A2);
hence  Partial_Sums seq = Ser Eseq by FUNCT_2:63; ::_thesis: verum
end;

theorem Th10: :: PROB_4:10
for seq being Function of NAT,REAL
for Eseq being Function of NAT,ExtREAL st seq = Eseq & seq is V101() holds
upper_bound seq = sup (rng Eseq)
proof
let seq be Function of NAT,REAL; ::_thesis: for Eseq being Function of NAT,ExtREAL st seq = Eseq & seq is V101() holds
upper_bound seq = sup (rng Eseq)
let Eseq be Function of NAT,ExtREAL; ::_thesis: ( seq = Eseq & seq is V101() implies upper_bound seq = sup (rng Eseq) )
assume that
A1: seq = Eseq and
A2: seq is V101() ; ::_thesis: upper_bound seq = sup (rng Eseq)
reconsider s = upper_bound seq as R_eal by XXREAL_0:def_1;
A3: dom Eseq = NAT by FUNCT_2:def_1;
A4: rng Eseq <> {-infty}
proof
assume  rng Eseq = {-infty} ; ::_thesis: contradiction
then reconsider k1 = -infty as Element of rng Eseq by TARSKI:def_1;
consider n1 being set  such that
A5: n1 in NAT and
 Eseq . n1 = k1 by A3, FUNCT_1:def_3;
reconsider n1 = n1 as Element of NAT by A5;
 seq . n1 = k1 by A1;
hence  contradiction ; ::_thesis: verum
end;
 for x being ext-real number st x in rng Eseq holds
x <= s
proof
let x be ext-real number ; ::_thesis: ( x in rng Eseq implies x <= s )
assume  x in rng Eseq ; ::_thesis: x <= s
then  ex n1 being set st
( n1 in NAT & Eseq . n1 = x ) by A3, FUNCT_1:def_3;
hence  x <= s by A1, A2, RINFSUP1:7; ::_thesis: verum
end;
then A6: s is UpperBound of rng Eseq by XXREAL_2:def_1;
then A7: rng Eseq is bounded_above by XXREAL_2:def_10;
A8: s <= sup (rng Eseq)
proof
reconsider r1 = sup (rng Eseq) as Real by A7, A4, XXREAL_2:57;
 sup (rng Eseq) is UpperBound of rng Eseq by XXREAL_2:def_3;
then  for n being Element of NAT holds seq . n <= r1 by A1, A3, FUNCT_1:3, XXREAL_2:def_1;
hence  s <= sup (rng Eseq) by RINFSUP1:9; ::_thesis: verum
end;
 sup (rng Eseq) <= s by A6, XXREAL_2:def_3;
hence  upper_bound seq = sup (rng Eseq) by A8, XXREAL_0:1; ::_thesis: verum
end;

theorem Th11: :: PROB_4:11
for seq being Function of NAT,REAL
for Eseq being Function of NAT,ExtREAL st seq = Eseq & seq is V102() holds
lower_bound seq = inf (rng Eseq)
proof
let seq be Function of NAT,REAL; ::_thesis: for Eseq being Function of NAT,ExtREAL st seq = Eseq & seq is V102() holds
lower_bound seq = inf (rng Eseq)
let Eseq be Function of NAT,ExtREAL; ::_thesis: ( seq = Eseq & seq is V102() implies lower_bound seq = inf (rng Eseq) )
assume that
A1: seq = Eseq and
A2: seq is V102() ; ::_thesis: lower_bound seq = inf (rng Eseq)
reconsider s = lower_bound seq as R_eal by XXREAL_0:def_1;
A3: dom Eseq = NAT by FUNCT_2:def_1;
A4: rng Eseq <> {+infty}
proof
assume  rng Eseq = {+infty} ; ::_thesis: contradiction
then reconsider k1 = +infty as Element of rng Eseq by TARSKI:def_1;
consider n1 being set  such that
A5: n1 in NAT and
 Eseq . n1 = k1 by A3, FUNCT_1:def_3;
reconsider n1 = n1 as Element of NAT by A5;
 seq . n1 = k1 by A1;
hence  contradiction ; ::_thesis: verum
end;
 for x being ext-real number st x in rng Eseq holds
s <= x
proof
let x be ext-real number ; ::_thesis: ( x in rng Eseq implies s <= x )
assume  x in rng Eseq ; ::_thesis: s <= x
then  ex n1 being set st
( n1 in NAT & Eseq . n1 = x ) by A3, FUNCT_1:def_3;
hence  s <= x by A1, A2, RINFSUP1:8; ::_thesis: verum
end;
then A6: s is LowerBound of rng Eseq by XXREAL_2:def_2;
then A7: rng Eseq is bounded_below by XXREAL_2:def_9;
A8: inf (rng Eseq) <= s
proof
reconsider r1 = inf (rng Eseq) as Real by A7, A4, XXREAL_2:58;
 inf (rng Eseq) is LowerBound of rng Eseq by XXREAL_2:def_4;
then  for n being Element of NAT holds r1 <= seq . n by A1, A3, FUNCT_1:3, XXREAL_2:def_2;
hence  inf (rng Eseq) <= s by RINFSUP1:10; ::_thesis: verum
end;
 s <= inf (rng Eseq) by A6, XXREAL_2:def_4;
hence  lower_bound seq = inf (rng Eseq) by A8, XXREAL_0:1; ::_thesis: verum
end;

theorem Th12: :: PROB_4:12
for seq being Function of NAT,REAL
for Eseq being Function of NAT,ExtREAL st seq = Eseq & seq is nonnegative & seq is summable holds
Sum seq = SUM Eseq
proof
let seq be Function of NAT,REAL; ::_thesis: for Eseq being Function of NAT,ExtREAL st seq = Eseq & seq is nonnegative & seq is summable holds
Sum seq = SUM Eseq
let Eseq be Function of NAT,ExtREAL; ::_thesis: ( seq = Eseq & seq is nonnegative & seq is summable implies Sum seq = SUM Eseq )
assume that
A1: seq = Eseq and
A2: ( seq is nonnegative & seq is summable ) ; ::_thesis: Sum seq = SUM Eseq
A3: for n being Element of NAT holds seq . n >= 0 by A2, RINFSUP1:def_3;
 Partial_Sums seq is convergent by A2, SERIES_1:def_2;
then A4: Partial_Sums seq is bounded ;
then  upper_bound (Partial_Sums seq) = sup (rng (Ser Eseq)) by A1, Th9, Th10;
then  upper_bound (Partial_Sums seq) = SUM Eseq by SUPINF_2:def_17;
hence  Sum seq = SUM Eseq by A4, A3, RINFSUP1:24, SERIES_1:16; ::_thesis: verum
end;

theorem Th13: :: PROB_4:13
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds P is sigma_Measure of Sigma
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma holds P is sigma_Measure of Sigma
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma holds P is sigma_Measure of Sigma
let P be Probability of Sigma; ::_thesis: P is sigma_Measure of Sigma
set Z = Sigma;
reconsider P1 = P as Function of Sigma,ExtREAL by FUNCT_2:7, NUMBERS:31;
 for x being R_eal st x in rng P1 holds
0. <= x
proof
let x be R_eal; ::_thesis: ( x in rng P1 implies 0. <= x )
assume A1: x in rng P1 ; ::_thesis: 0. <= x
 dom P1 = Sigma by FUNCT_2:def_1;
then consider y being set  such that
A2: y in Sigma and
A3: P1 . y = x by A1, FUNCT_1:def_3;
reconsider y1 = y as Event of Sigma by A2;
 0 <= P . y1 by PROB_1:def_8;
hence  0. <= x by A3; ::_thesis: verum
end;
then A4: rng P1 is nonnegative by SUPINF_2:def_9;
 for F being Sep_Sequence of Sigma holds SUM (P1 * F) = P1 . (union (rng F))
proof
let F be Sep_Sequence of Sigma; ::_thesis: SUM (P1 * F) = P1 . (union (rng F))
reconsider F2 = F as V118() SetSequence of Sigma by Th2;
 for n being Element of NAT holds (P * F2) . n >= 0 by PROB_3:4;
then A5: P * F2 is nonnegative by RINFSUP1:def_3;
 Partial_Sums (P * F2) is convergent by PROB_3:45;
then  P * F2 is summable by SERIES_1:def_2;
then  ( P . (Union F2) = Sum (P * F2) & Sum (P * F2) = SUM (P1 * F) ) by A5, Th12, PROB_3:46;
hence  SUM (P1 * F) = P1 . (union (rng F)) by CARD_3:def_4; ::_thesis: verum
end;
hence  P is sigma_Measure of Sigma by A4, MEASURE1:def_6, SUPINF_2:def_16; ::_thesis: verum
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
func P2M P ->  sigma_Measure of Sigma equals :: PROB_4:def 1
P;
coherence
 P is sigma_Measure of Sigma by Th13;
end;

:: deftheorem  defines P2M PROB_4:def_1_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds P2M P = P;

theorem Th14: :: PROB_4:14
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S st M . X = R_EAL 1 holds
M is Probability of S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S st M . X = R_EAL 1 holds
M is Probability of S
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S st M . X = R_EAL 1 holds
M is Probability of S
let M be sigma_Measure of S; ::_thesis: ( M . X = R_EAL 1 implies M is Probability of S )
assume A1: M . X = R_EAL 1 ; ::_thesis: M is Probability of S
A2: for A being Element of S holds M . A <= R_EAL 1
proof
reconsider X = X as Element of S by PROB_1:5;
let A be Element of S; ::_thesis: M . A <= R_EAL 1
 M . A <= M . X by MEASURE1:31;
hence  M . A <= R_EAL 1 by A1; ::_thesis: verum
end;
A3: for x being set st x in S holds
M . x in REAL
proof
let x be set ; ::_thesis: ( x in S implies M . x in REAL )
assume  x in S ; ::_thesis: M . x in REAL
then reconsider x = x as Element of S ;
A4: ( R_EAL 1 is Real & 0 is Real ) by MEASURE6:def_1;
 ( 0. <= M . x & M . x <= R_EAL 1 ) by A2, MEASURE1:def_2;
hence  M . x in REAL by A4, XXREAL_0:45; ::_thesis: verum
end;
 dom M = S by FUNCT_2:def_1;
then reconsider P1 = M as Function of S,REAL by A3, FUNCT_2:3;
reconsider P1 = P1 as Function of S,REAL ;
A5: for ASeq being SetSequence of S st ASeq is non-ascending holds
( P1 * ASeq is convergent & lim (P1 * ASeq) = P1 . (Intersection ASeq) )
proof
let ASeq be SetSequence of S; ::_thesis: ( ASeq is non-ascending implies ( P1 * ASeq is convergent & lim (P1 * ASeq) = P1 . (Intersection ASeq) ) )
assume A6: ASeq is non-ascending ; ::_thesis: ( P1 * ASeq is convergent & lim (P1 * ASeq) = P1 . (Intersection ASeq) )
 for n being Element of NAT holds 0 <= (P1 * ASeq) . n
proof
let n be Element of NAT ; ::_thesis: 0 <= (P1 * ASeq) . n
reconsider A = ASeq . n as Event of S ;
 ( 0 <= P1 . A & dom (P1 * ASeq) = NAT ) by MEASURE1:def_2, SEQ_1:1;
hence  0 <= (P1 * ASeq) . n by FUNCT_1:12; ::_thesis: verum
end;
then A7: P1 * ASeq is V102() by RINFSUP1:10;
reconsider F = ASeq as Function of NAT,S by Th2;
A8: for n being Element of NAT holds F . (n + 1) c= F . n by A6, PROB_2:6;
A9: M . (F . 0) < +infty by A3, XXREAL_0:9;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(P1_*_ASeq)_._(n_+_1)_<=_(P1_*_ASeq)_._n
let n be Element of NAT ; ::_thesis: (P1 * ASeq) . (n + 1) <= (P1 * ASeq) . n
 dom (M * F) = NAT by FUNCT_2:def_1;
then A10: ( (M * F) . n = M . (F . n) & (M * F) . (n + 1) = M . (F . (n + 1)) ) by FUNCT_1:12;
 F . (n + 1) c= F . n by A6, PROB_2:6;
hence  (P1 * ASeq) . (n + 1) <= (P1 * ASeq) . n by A10, MEASURE1:31; ::_thesis: verum
end;
then A11: P1 * ASeq is non-increasing by SEQM_3:def_9;
then  lim (P1 * ASeq) = lower_bound (P1 * ASeq) by A7, RINFSUP1:25
.= inf (rng (M * F)) by A7, Th11 ;
then  lim (P1 * ASeq) = M . (meet (rng F)) by A8, A9, MEASURE3:12
.= P1 . (Intersection ASeq) by SETLIM_1:8 ;
hence  ( P1 * ASeq is convergent & lim (P1 * ASeq) = P1 . (Intersection ASeq) ) by A7, A11; ::_thesis: verum
end;
A12: for A, B being Event of S st A misses B holds
P1 . (A \/ B) = (P1 . A) + (P1 . B)
proof
let A, B be Event of S; ::_thesis: ( A misses B implies P1 . (A \/ B) = (P1 . A) + (P1 . B) )
assume A13: A misses B ; ::_thesis: P1 . (A \/ B) = (P1 . A) + (P1 . B)
reconsider A = A, B = B as Element of S ;
reconsider A2 = A, B2 = B as Element of S ;
P1 . (A \/ B) = (M . A2) + (M . B2) by A13, MEASURE1:30
.= (P1 . A) + (P1 . B) by SUPINF_2:1 ;
hence  P1 . (A \/ B) = (P1 . A) + (P1 . B) ; ::_thesis: verum
end;
 ( ( for A being Event of S holds 0 <= P1 . A ) & P1 . X = 1 ) by A1, MEASURE1:def_2, MEASURE6:def_1;
hence  M is Probability of S by A12, A5, PROB_1:def_8; ::_thesis: verum
end;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
assume A1: M . X = R_EAL 1 ;
func M2P M ->  Probability of S equals :: PROB_4:def 2
M;
coherence
 M is Probability of S by A1, Th14;
end;

:: deftheorem  defines M2P PROB_4:def_2_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S st M . X = R_EAL 1 holds
M2P M = M;

Lm2:  for X being set
for A1 being SetSequence of X st A1 is non-descending holds
for n being Element of NAT holds (Partial_Union A1) . n = A1 . n
proof
let X be set ; ::_thesis: for A1 being SetSequence of X st A1 is non-descending holds
for n being Element of NAT holds (Partial_Union A1) . n = A1 . n
let A1 be SetSequence of X; ::_thesis: ( A1 is non-descending implies for n being Element of NAT holds (Partial_Union A1) . n = A1 . n )
defpred S1[ Element of NAT ] means (Partial_Union A1) . $1 = A1 . $1;
assume A1: A1 is non-descending ; ::_thesis: for n being Element of NAT holds (Partial_Union A1) . n = A1 . n
A2: 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 A3: S1[k] ; ::_thesis: S1[k + 1]
A4: A1 . k c= A1 . (k + 1) by A1, PROB_2:7;
thus (Partial_Union A1) . (k + 1) = (A1 . k) \/ (A1 . (k + 1)) by A3, PROB_3:def_2
.= A1 . (k + 1) by A4, XBOOLE_1:12 ; ::_thesis: verum
end;
A5: S1[ 0 ] by PROB_3:def_2;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A2); ::_thesis: verum
end;

theorem Th15: :: PROB_4:15
for X being set
for A1 being SetSequence of X st A1 is non-descending holds
Partial_Union A1 = A1
proof
let X be set ; ::_thesis: for A1 being SetSequence of X st A1 is non-descending holds
Partial_Union A1 = A1
let A1 be SetSequence of X; ::_thesis: ( A1 is non-descending implies Partial_Union A1 = A1 )
assume  A1 is non-descending ; ::_thesis: Partial_Union A1 = A1
then  for n being Element of NAT holds (Partial_Union A1) . n = A1 . n by Lm2;
hence  Partial_Union A1 = A1 by FUNCT_2:63; ::_thesis: verum
end;

theorem Th16: :: PROB_4:16
for X being set
for A1 being SetSequence of X st A1 is non-descending holds
( (Partial_Diff_Union A1) . 0 = A1 . 0 & ( for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) ) )
proof
let X be set ; ::_thesis: for A1 being SetSequence of X st A1 is non-descending holds
( (Partial_Diff_Union A1) . 0 = A1 . 0 & ( for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) ) )
let A1 be SetSequence of X; ::_thesis: ( A1 is non-descending implies ( (Partial_Diff_Union A1) . 0 = A1 . 0 & ( for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) ) ) )
assume A1: A1 is non-descending ; ::_thesis: ( (Partial_Diff_Union A1) . 0 = A1 . 0 & ( for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) ) )
thus  (Partial_Diff_Union A1) . 0 = A1 . 0 by PROB_3:def_3; ::_thesis: for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n)
thus  for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) ::_thesis: verum
proof
let n be Element of NAT ; ::_thesis: (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n)
thus (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) by PROB_3:def_3
.= (A1 . (n + 1)) \ (A1 . n) by A1, Lm2 ; ::_thesis: verum
end;
end;

theorem :: PROB_4:17
for X being set
for A1 being SetSequence of X st A1 is non-descending holds
for n being Element of NAT holds A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n)
proof
let X be set ; ::_thesis: for A1 being SetSequence of X st A1 is non-descending holds
for n being Element of NAT holds A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n)
let A1 be SetSequence of X; ::_thesis: ( A1 is non-descending implies for n being Element of NAT holds A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n) )
assume A1: A1 is non-descending ; ::_thesis: for n being Element of NAT holds A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n)
thus  for n being Element of NAT holds A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n) ::_thesis: verum
proof
let n be Element of NAT ; ::_thesis: A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n)
A2: A1 . n c= A1 . (n + 1) by A1, PROB_2:7;
thus ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n) = ((A1 . (n + 1)) \ ((Partial_Union A1) . n)) \/ (A1 . n) by PROB_3:def_3
.= ((A1 . (n + 1)) \ (A1 . n)) \/ (A1 . n) by A1, Lm2
.= (A1 . (n + 1)) \/ (A1 . n) by XBOOLE_1:39
.= A1 . (n + 1) by A2, XBOOLE_1:12 ; ::_thesis: verum
end;
end;

theorem Th18: :: PROB_4:18
for X being set
for A1 being SetSequence of X st A1 is non-descending holds
for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) misses A1 . n
proof
let X be set ; ::_thesis: for A1 being SetSequence of X st A1 is non-descending holds
for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) misses A1 . n
let A1 be SetSequence of X; ::_thesis: ( A1 is non-descending implies for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) misses A1 . n )
assume A1: A1 is non-descending ; ::_thesis: for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) misses A1 . n
let n be Element of NAT ; ::_thesis: (Partial_Diff_Union A1) . (n + 1) misses A1 . n
 (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) by A1, Th16;
hence  (Partial_Diff_Union A1) . (n + 1) misses A1 . n by XBOOLE_1:79; ::_thesis: verum
end;

theorem :: PROB_4:19
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si st XSeq is non-descending holds
Partial_Union XSeq = XSeq by Th15;

theorem :: PROB_4:20
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si st XSeq is non-descending holds
( (Partial_Diff_Union XSeq) . 0 = XSeq . 0 & ( for n being Element of NAT holds (Partial_Diff_Union XSeq) . (n + 1) = (XSeq . (n + 1)) \ (XSeq . n) ) ) by Th16;

theorem :: PROB_4:21
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si st XSeq is non-descending holds
for n being Element of NAT holds (Partial_Diff_Union XSeq) . (n + 1) misses XSeq . n by Th18;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
predP is_complete Sigma means :Def3: :: PROB_4:def 3
 for A being Subset of Omega
for B being set st B in Sigma & A c= B & P . B = 0 holds
A in Sigma;
end;

:: deftheorem Def3 defines is_complete PROB_4:def_3_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds
( P is_complete Sigma iff for A being Subset of Omega
for B being set st B in Sigma & A c= B & P . B = 0 holds
A in Sigma );

theorem :: PROB_4:22
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds
( P is_complete Sigma iff P2M P is_complete Sigma )
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma holds
( P is_complete Sigma iff P2M P is_complete Sigma )
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma holds
( P is_complete Sigma iff P2M P is_complete Sigma )
let P be Probability of Sigma; ::_thesis: ( P is_complete Sigma iff P2M P is_complete Sigma )
hereby  ::_thesis: ( P2M P is_complete Sigma implies P is_complete Sigma )
assume  P is_complete Sigma ; ::_thesis: P2M P is_complete Sigma
then  for A being Subset of Omega
for B being set st B in Sigma & A c= B & (P2M P) . B = 0. holds
A in Sigma by Def3;
hence  P2M P is_complete Sigma by MEASURE3:def_1; ::_thesis: verum
end;
assume  P2M P is_complete Sigma ; ::_thesis: P is_complete Sigma
then  for A being Subset of Omega
for B being set st B in Sigma & A c= B & P . B = 0 holds
A in Sigma by MEASURE3:def_1;
hence  P is_complete Sigma by Def3; ::_thesis: verum
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
mode thin of P ->  Subset of Omega means :Def4: :: PROB_4:def 4
 ex A being set st
( A in Sigma & it c= A & P . A = 0 );
existence
 ex b1 being Subset of Omega ex A being set st
( A in Sigma & b1 c= A & P . A = 0 )
proof
reconsider B = {} as Subset of Omega by XBOOLE_1:2;
take  B ; ::_thesis: ex A being set st
( A in Sigma & B c= A & P . A = 0 )
take A = {} ; ::_thesis: ( A in Sigma & B c= A & P . A = 0 )
thus  A in Sigma by PROB_1:4; ::_thesis: ( B c= A & P . A = 0 )
thus  B c= A ; ::_thesis: P . A = 0
thus  P . A = 0 by VALUED_0:def_19; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines thin PROB_4:def_4_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for b4 being Subset of Omega holds
( b4 is thin of P iff ex A being set st
( A in Sigma & b4 c= A & P . A = 0 ) );

theorem Th23: :: PROB_4:23
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for Y being Subset of Omega holds
( Y is thin of P iff Y is thin of P2M P )
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for Y being Subset of Omega holds
( Y is thin of P iff Y is thin of P2M P )
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for Y being Subset of Omega holds
( Y is thin of P iff Y is thin of P2M P )
let P be Probability of Sigma; ::_thesis: for Y being Subset of Omega holds
( Y is thin of P iff Y is thin of P2M P )
let Y be Subset of Omega; ::_thesis: ( Y is thin of P iff Y is thin of P2M P )
hereby  ::_thesis: ( Y is thin of P2M P implies Y is thin of P )
assume  Y is thin of P ; ::_thesis: Y is thin of P2M P
then  ex A being set st
( A in Sigma & Y c= A & P . A = 0 ) by Def4;
hence  Y is thin of P2M P by MEASURE3:def_2; ::_thesis: verum
end;
assume  Y is thin of P2M P ; ::_thesis: Y is thin of P
then  ex B being set st
( B in Sigma & Y c= B & (P2M P) . B = 0. ) by MEASURE3:def_2;
hence  Y is thin of P by Def4; ::_thesis: verum
end;

theorem Th24: :: PROB_4:24
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds {} is thin of P
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma holds {} is thin of P
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma holds {} is thin of P
let P be Probability of Sigma; ::_thesis: {} is thin of P
 ( P . {} = 0 & {} in Sigma ) by PROB_1:4, VALUED_0:def_19;
hence  {} is thin of P by Def4; ::_thesis: verum
end;

theorem Th25: :: PROB_4:25
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B1, B2 being set st B1 in Sigma & B2 in Sigma holds
for C1, C2 being thin of P st B1 \/ C1 = B2 \/ C2 holds
P . B1 = P . B2
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B1, B2 being set st B1 in Sigma & B2 in Sigma holds
for C1, C2 being thin of P st B1 \/ C1 = B2 \/ C2 holds
P . B1 = P . B2
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for B1, B2 being set st B1 in Sigma & B2 in Sigma holds
for C1, C2 being thin of P st B1 \/ C1 = B2 \/ C2 holds
P . B1 = P . B2
let P be Probability of Sigma; ::_thesis: for B1, B2 being set st B1 in Sigma & B2 in Sigma holds
for C1, C2 being thin of P st B1 \/ C1 = B2 \/ C2 holds
P . B1 = P . B2
let B1, B2 be set ; ::_thesis: ( B1 in Sigma & B2 in Sigma implies for C1, C2 being thin of P st B1 \/ C1 = B2 \/ C2 holds
P . B1 = P . B2 )
assume A1: ( B1 in Sigma & B2 in Sigma ) ; ::_thesis: for C1, C2 being thin of P st B1 \/ C1 = B2 \/ C2 holds
P . B1 = P . B2
let C1, C2 be thin of P; ::_thesis: ( B1 \/ C1 = B2 \/ C2 implies P . B1 = P . B2 )
assume A2: B1 \/ C1 = B2 \/ C2 ; ::_thesis: P . B1 = P . B2
then A3: B1 c= B2 \/ C2 by XBOOLE_1:7;
A4: B2 c= B1 \/ C1 by A2, XBOOLE_1:7;
consider D1 being set  such that
A5: D1 in Sigma and
A6: C1 c= D1 and
A7: P . D1 = 0 by Def4;
A8: B1 \/ C1 c= B1 \/ D1 by A6, XBOOLE_1:9;
consider D2 being set  such that
A9: D2 in Sigma and
A10: C2 c= D2 and
A11: P . D2 = 0 by Def4;
A12: B2 \/ C2 c= B2 \/ D2 by A10, XBOOLE_1:9;
reconsider B1 = B1, B2 = B2, D1 = D1, D2 = D2 as Event of Sigma by A1, A5, A9;
A13: P . (B1 \/ D1) <= (P . B1) + (P . D1) by PROB_1:39;
 P . B2 <= P . (B1 \/ D1) by A4, A8, PROB_1:34, XBOOLE_1:1;
then A14: P . B2 <= P . B1 by A7, A13, XXREAL_0:2;
A15: P . (B2 \/ D2) <= (P . B2) + (P . D2) by PROB_1:39;
 P . B1 <= P . (B2 \/ D2) by A3, A12, PROB_1:34, XBOOLE_1:1;
then  P . B1 <= P . B2 by A11, A15, XXREAL_0:2;
hence  P . B1 = P . B2 by A14, XXREAL_0:1; ::_thesis: verum
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
func COM (Sigma,P) ->  non empty Subset-Family of Omega means :Def5: :: PROB_4:def 5
 for A being set holds
( A in it iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) );
existence
 ex b1 being non empty Subset-Family of Omega st
for A being set holds
( A in b1 iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) )
proof
A1: {} is thin of P by Th24;
A2: for A being set st A = {} holds
ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C )
proof
let A be set ; ::_thesis: ( A = {} implies ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) )
consider B being set  such that
A3: B = {} and
A4: B in Sigma by PROB_1:4;
consider C being thin of P such that
A5: C = {} by A1;
assume  A = {} ; ::_thesis: ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C )
then  A = B \/ C by A3, A5;
hence  ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) by A4; ::_thesis: verum
end;
defpred S1[ set ] means  for A being set st A = $1 holds
ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C );
consider D being set  such that
A6: for y being set holds
( y in D iff ( y in bool Omega & S1[y] ) ) from XBOOLE_0:sch_1();
A7: for A being set holds
( A in D iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) )
proof
let A be set ; ::_thesis: ( A in D iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) )
A8: ( A in D iff ( A in bool Omega & ( for y being set st y = A holds
ex B being set st
( B in Sigma & ex C being thin of P st y = B \/ C ) ) ) ) by A6;
 ( ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) implies A in D )
proof
assume A9: ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ; ::_thesis: A in D
then  A c= Omega by XBOOLE_1:8;
hence  A in D by A8, A9; ::_thesis: verum
end;
hence  ( A in D iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) by A6; ::_thesis: verum
end;
A10: D c= bool Omega
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in bool Omega )
assume  x in D ; ::_thesis: x in bool Omega
hence  x in bool Omega by A6; ::_thesis: verum
end;
 {} c= Omega by XBOOLE_1:2;
then reconsider D = D as non empty Subset-Family of Omega by A6, A10, A2;
take  D ; ::_thesis: for A being set holds
( A in D iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) )
thus  for A being set holds
( A in D iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) by A7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty Subset-Family of Omega st ( for A being set holds
( A in b1 iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) & ( for A being set holds
( A in b2 iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) holds
b1 = b2
proof
let D1, D2 be non empty Subset-Family of Omega; ::_thesis: ( ( for A being set holds
( A in D1 iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) & ( for A being set holds
( A in D2 iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) implies D1 = D2 )
assume that
A11: for A being set holds
( A in D1 iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) and
A12: for A being set holds
( A in D2 iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ; ::_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 )
thus  ( A in D1 implies A in D2 ) ::_thesis: ( A in D2 implies A in D1 )
proof
assume  A in D1 ; ::_thesis: A in D2
then  ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) by A11;
hence  A in D2 by A12; ::_thesis: verum
end;
assume  A in D2 ; ::_thesis: A in D1
then  ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) by A12;
hence  A in D1 by A11; ::_thesis: verum
end;
hence  D1 = D2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines COM PROB_4:def_5_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for b4 being non empty Subset-Family of Omega holds
( b4 = COM (Sigma,P) iff for A being set holds
( A in b4 iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) );

theorem Th26: :: PROB_4:26
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for C being thin of P holds C in COM (Sigma,P)
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for C being thin of P holds C in COM (Sigma,P)
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for C being thin of P holds C in COM (Sigma,P)
let P be Probability of Sigma; ::_thesis: for C being thin of P holds C in COM (Sigma,P)
let C be thin of P; ::_thesis: C in COM (Sigma,P)
reconsider B = {} as Element of Sigma by PROB_1:4;
 B \/ C in COM (Sigma,P) by Def5;
hence  C in COM (Sigma,P) ; ::_thesis: verum
end;

theorem Th27: :: PROB_4:27
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds COM (Sigma,P) = COM (Sigma,(P2M P))
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma holds COM (Sigma,P) = COM (Sigma,(P2M P))
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma holds COM (Sigma,P) = COM (Sigma,(P2M P))
let P be Probability of Sigma; ::_thesis: COM (Sigma,P) = COM (Sigma,(P2M P))
A1: COM (Sigma,(P2M P)) c= COM (Sigma,P)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in COM (Sigma,(P2M P)) or x in COM (Sigma,P) )
assume  x in COM (Sigma,(P2M P)) ; ::_thesis: x in COM (Sigma,P)
then consider B being set  such that
A2: B in Sigma and
A3: ex C being thin of P2M P st x = B \/ C by MEASURE3:def_3;
consider C being thin of P2M P such that
A4: x = B \/ C by A3;
reconsider C1 = C as thin of P by Th23;
 x = B \/ C1 by A4;
hence  x in COM (Sigma,P) by A2, Def5; ::_thesis: verum
end;
 COM (Sigma,P) c= COM (Sigma,(P2M P))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in COM (Sigma,P) or x in COM (Sigma,(P2M P)) )
assume  x in COM (Sigma,P) ; ::_thesis: x in COM (Sigma,(P2M P))
then consider B being set  such that
A5: B in Sigma and
A6: ex C being thin of P st x = B \/ C by Def5;
consider C being thin of P such that
A7: x = B \/ C by A6;
reconsider C1 = C as thin of P2M P by Th23;
 x = B \/ C1 by A7;
hence  x in COM (Sigma,(P2M P)) by A5, MEASURE3:def_3; ::_thesis: verum
end;
hence  COM (Sigma,P) = COM (Sigma,(P2M P)) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
let A be Element of COM (Sigma,P);
func P_COM2M_COM A ->  Element of COM (Sigma,(P2M P)) equals :: PROB_4:def 6
A;
correctness
coherence
A is Element of COM (Sigma,(P2M P));
by Th27;
end;

:: deftheorem  defines P_COM2M_COM PROB_4:def_6_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM (Sigma,P) holds P_COM2M_COM A = A;

theorem Th28: :: PROB_4:28
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds Sigma c= COM (Sigma,P)
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma holds Sigma c= COM (Sigma,P)
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma holds Sigma c= COM (Sigma,P)
let P be Probability of Sigma; ::_thesis: Sigma c= COM (Sigma,P)
reconsider C = {} as thin of P by Th24;
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in Sigma or A in COM (Sigma,P) )
assume A1: A in Sigma ; ::_thesis: A in COM (Sigma,P)
 A = A \/ C ;
hence  A in COM (Sigma,P) by A1, Def5; ::_thesis: verum
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
let A be Element of COM (Sigma,P);
func ProbPart A ->  non empty Subset-Family of Omega means :Def7: :: PROB_4:def 7
 for B being set holds
( B in it iff ( B in Sigma & B c= A & A \ B is thin of P ) );
existence
 ex b1 being non empty Subset-Family of Omega st
for B being set holds
( B in b1 iff ( B in Sigma & B c= A & A \ B is thin of P ) )
proof
defpred S1[ set ] means  for t being set st t = $1 holds
( t in Sigma & t c= A & A \ t is thin of P );
consider D being set  such that
A1: for t being set holds
( t in D iff ( t in bool Omega & S1[t] ) ) from XBOOLE_0:sch_1();
A2: for B being set holds
( B in D iff ( B in Sigma & B c= A & A \ B is thin of P ) )
proof
let B be set ; ::_thesis: ( B in D iff ( B in Sigma & B c= A & A \ B is thin of P ) )
 ( B in Sigma & B c= A & A \ B is thin of P implies B in D )
proof
assume that
A3: B in Sigma and
A4: ( B c= A & A \ B is thin of P ) ; ::_thesis: B in D
 for t being set st t = B holds
( t in Sigma & t c= A & A \ t is thin of P ) by A3, A4;
hence  B in D by A1, A3; ::_thesis: verum
end;
hence  ( B in D iff ( B in Sigma & B c= A & A \ B is thin of P ) ) by A1; ::_thesis: verum
end;
A5: D c= bool Omega
proof
let B be set ; :: according to TARSKI:def_3 ::_thesis: ( not B in D or B in bool Omega )
assume  B in D ; ::_thesis: B in bool Omega
then  B in Sigma by A2;
hence  B in bool Omega ; ::_thesis: verum
end;
 D <> {}
proof
consider B being set  such that
A6: B in Sigma and
A7: ex C being thin of P st A = B \/ C by Def5;
consider C being thin of P such that
A8: A = B \/ C by A7;
consider E being set  such that
A9: E in Sigma and
A10: C c= E and
A11: P . E = 0 by Def4;
 A \ B = C \ B by A8, XBOOLE_1:40;
then  A \ B c= C by XBOOLE_1:36;
then  A \ B c= E by A10, XBOOLE_1:1;
then A12: A \ B is thin of P by A9, A11, Def4;
 B c= A by A8, XBOOLE_1:7;
hence  D <> {} by A2, A6, A12; ::_thesis: verum
end;
then reconsider D = D as non empty Subset-Family of Omega by A5;
take  D ; ::_thesis: for B being set holds
( B in D iff ( B in Sigma & B c= A & A \ B is thin of P ) )
thus  for B being set holds
( B in D iff ( B in Sigma & B c= A & A \ B is thin of P ) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty Subset-Family of Omega st ( for B being set holds
( B in b1 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ) & ( for B being set holds
( B in b2 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ) holds
b1 = b2
proof
let D1, D2 be non empty Subset-Family of Omega; ::_thesis: ( ( for B being set holds
( B in D1 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ) & ( for B being set holds
( B in D2 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ) implies D1 = D2 )
assume that
A13: for B being set holds
( B in D1 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) and
A14: for B being set holds
( B in D2 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ; ::_thesis: D1 = D2
 for B being set holds
( B in D1 iff B in D2 )
proof
let B be set ; ::_thesis: ( B in D1 iff B in D2 )
thus  ( B in D1 implies B in D2 ) ::_thesis: ( B in D2 implies B in D1 )
proof
assume A15: B in D1 ; ::_thesis: B in D2
then A16: A \ B is thin of P by A13;
 ( B in Sigma & B c= A ) by A13, A15;
hence  B in D2 by A14, A16; ::_thesis: verum
end;
assume A17: B in D2 ; ::_thesis: B in D1
then A18: A \ B is thin of P by A14;
 ( B in Sigma & B c= A ) by A14, A17;
hence  B in D1 by A13, A18; ::_thesis: verum
end;
hence  D1 = D2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines ProbPart PROB_4:def_7_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM (Sigma,P)
for b5 being non empty Subset-Family of Omega holds
( b5 = ProbPart A iff for B being set holds
( B in b5 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) );

theorem :: PROB_4:29
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM (Sigma,P) holds ProbPart A = MeasPart (P_COM2M_COM A)
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM (Sigma,P) holds ProbPart A = MeasPart (P_COM2M_COM A)
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for A being Element of COM (Sigma,P) holds ProbPart A = MeasPart (P_COM2M_COM A)
let P be Probability of Sigma; ::_thesis: for A being Element of COM (Sigma,P) holds ProbPart A = MeasPart (P_COM2M_COM A)
let A be Element of COM (Sigma,P); ::_thesis: ProbPart A = MeasPart (P_COM2M_COM A)
A1: MeasPart (P_COM2M_COM A) c= ProbPart A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MeasPart (P_COM2M_COM A) or x in ProbPart A )
assume A2: x in MeasPart (P_COM2M_COM A) ; ::_thesis: x in ProbPart A
 (P_COM2M_COM A) \ x is thin of P2M P by A2, MEASURE3:def_4;
then A3: A \ x is thin of P by Th23;
 ( x in Sigma & x c= P_COM2M_COM A ) by A2, MEASURE3:def_4;
hence  x in ProbPart A by A3, Def7; ::_thesis: verum
end;
 ProbPart A c= MeasPart (P_COM2M_COM A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ProbPart A or x in MeasPart (P_COM2M_COM A) )
assume A4: x in ProbPart A ; ::_thesis: x in MeasPart (P_COM2M_COM A)
 A \ x is thin of P by A4, Def7;
then A5: (P_COM2M_COM A) \ x is thin of P2M P by Th23;
 ( x in Sigma & x c= A ) by A4, Def7;
hence  x in MeasPart (P_COM2M_COM A) by A5, MEASURE3:def_4; ::_thesis: verum
end;
hence  ProbPart A = MeasPart (P_COM2M_COM A) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: PROB_4:30
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM (Sigma,P)
for A1, A2 being set st A1 in ProbPart A & A2 in ProbPart A holds
P . A1 = P . A2
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM (Sigma,P)
for A1, A2 being set st A1 in ProbPart A & A2 in ProbPart A holds
P . A1 = P . A2
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for A being Element of COM (Sigma,P)
for A1, A2 being set st A1 in ProbPart A & A2 in ProbPart A holds
P . A1 = P . A2
let P be Probability of Sigma; ::_thesis: for A being Element of COM (Sigma,P)
for A1, A2 being set st A1 in ProbPart A & A2 in ProbPart A holds
P . A1 = P . A2
let A be Element of COM (Sigma,P); ::_thesis: for A1, A2 being set st A1 in ProbPart A & A2 in ProbPart A holds
P . A1 = P . A2
let A1, A2 be set ; ::_thesis: ( A1 in ProbPart A & A2 in ProbPart A implies P . A1 = P . A2 )
assume that
A1: A1 in ProbPart A and
A2: A2 in ProbPart A ; ::_thesis: P . A1 = P . A2
reconsider C1 = A \ A1, C2 = A \ A2 as thin of P by A1, A2, Def7;
A3: A2 c= A by A2, Def7;
 A1 c= A by A1, Def7;
then A4: A1 \/ C1 = A by XBOOLE_1:45
.= A2 \/ C2 by A3, XBOOLE_1:45 ;
 ( A1 in Sigma & A2 in Sigma ) by A1, A2, Def7;
hence  P . A1 = P . A2 by A4, Th25; ::_thesis: verum
end;

theorem Th31: :: PROB_4:31
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being Function of NAT,(COM (Sigma,P)) ex BSeq being SetSequence of Sigma st
for n being Element of NAT holds BSeq . n in ProbPart (F . n)
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being Function of NAT,(COM (Sigma,P)) ex BSeq being SetSequence of Sigma st
for n being Element of NAT holds BSeq . n in ProbPart (F . n)
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for F being Function of NAT,(COM (Sigma,P)) ex BSeq being SetSequence of Sigma st
for n being Element of NAT holds BSeq . n in ProbPart (F . n)
let P be Probability of Sigma; ::_thesis: for F being Function of NAT,(COM (Sigma,P)) ex BSeq being SetSequence of Sigma st
for n being Element of NAT holds BSeq . n in ProbPart (F . n)
let F be Function of NAT,(COM (Sigma,P)); ::_thesis: ex BSeq being SetSequence of Sigma st
for n being Element of NAT holds BSeq . n in ProbPart (F . n)
defpred S1[ Element of NAT , set ] means  for n being Element of NAT
for y being set st n = $1 & y = $2 holds
y in ProbPart (F . n);
A1: for t being Element of NAT ex A being Element of Sigma st S1[t,A]
proof
let t be Element of NAT ; ::_thesis: ex A being Element of Sigma st S1[t,A]
set A = the Element of ProbPart (F . t);
reconsider A = the Element of ProbPart (F . t) as Element of Sigma by Def7;
take  A ; ::_thesis: S1[t,A]
thus  S1[t,A] ; ::_thesis: verum
end;
 ex G being Function of NAT,Sigma st
for t being Element of NAT holds S1[t,G . t] from FUNCT_2:sch_3(A1);
then consider G being Function of NAT,Sigma such that
A2: for t, n being Element of NAT
for y being set st n = t & y = G . t holds
y in ProbPart (F . n) ;
reconsider BSeq = G as SetSequence of Omega by FUNCT_2:7;
reconsider BSeq = BSeq as SetSequence of Sigma ;
take  BSeq ; ::_thesis: for n being Element of NAT holds BSeq . n in ProbPart (F . n)
thus  for n being Element of NAT holds BSeq . n in ProbPart (F . n) by A2; ::_thesis: verum
end;

theorem Th32: :: PROB_4:32
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being Function of NAT,(COM (Sigma,P))
for BSeq being SetSequence of Sigma ex CSeq being SetSequence of Omega st
for n being Element of NAT holds CSeq . n = (F . n) \ (BSeq . n)
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being Function of NAT,(COM (Sigma,P))
for BSeq being SetSequence of Sigma ex CSeq being SetSequence of Omega st
for n being Element of NAT holds CSeq . n = (F . n) \ (BSeq . n)
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for F being Function of NAT,(COM (Sigma,P))
for BSeq being SetSequence of Sigma ex CSeq being SetSequence of Omega st
for n being Element of NAT holds CSeq . n = (F . n) \ (BSeq . n)
let P be Probability of Sigma; ::_thesis: for F being Function of NAT,(COM (Sigma,P))
for BSeq being SetSequence of Sigma ex CSeq being SetSequence of Omega st
for n being Element of NAT holds CSeq . n = (F . n) \ (BSeq . n)
let F be Function of NAT,(COM (Sigma,P)); ::_thesis: for BSeq being SetSequence of Sigma ex CSeq being SetSequence of Omega st
for n being Element of NAT holds CSeq . n = (F . n) \ (BSeq . n)
let G be SetSequence of Sigma; ::_thesis: ex CSeq being SetSequence of Omega st
for n being Element of NAT holds CSeq . n = (F . n) \ (G . n)
defpred S1[ Element of NAT , set ] means  for n being Element of NAT
for y being set st n = $1 & y = $2 holds
y = (F . n) \ (G . n);
A1: for t being Element of NAT ex A being Element of bool Omega st S1[t,A]
proof
let t be Element of NAT ; ::_thesis: ex A being Element of bool Omega st S1[t,A]
 F . t is Element of COM (Sigma,P) ;
then reconsider A = (F . t) \ (G . t) as Element of bool Omega by XBOOLE_1:1;
take  A ; ::_thesis: S1[t,A]
thus  S1[t,A] ; ::_thesis: verum
end;
 ex H being Function of NAT,(bool Omega) st
for t being Element of NAT holds S1[t,H . t] from FUNCT_2:sch_3(A1);
then consider H being Function of NAT,(bool Omega) such that
A2: for t, n being Element of NAT
for y being set st n = t & y = H . t holds
y = (F . n) \ (G . n) ;
take  H ; ::_thesis: for n being Element of NAT holds H . n = (F . n) \ (G . n)
thus  for n being Element of NAT holds H . n = (F . n) \ (G . n) by A2; ::_thesis: verum
end;

theorem Th33: :: PROB_4:33
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for BSeq being SetSequence of Omega st ( for n being Element of NAT holds BSeq . n is thin of P ) holds
ex CSeq being SetSequence of Sigma st
for n being Element of NAT holds
( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 )
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for BSeq being SetSequence of Omega st ( for n being Element of NAT holds BSeq . n is thin of P ) holds
ex CSeq being SetSequence of Sigma st
for n being Element of NAT holds
( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 )
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for BSeq being SetSequence of Omega st ( for n being Element of NAT holds BSeq . n is thin of P ) holds
ex CSeq being SetSequence of Sigma st
for n being Element of NAT holds
( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 )
let P be Probability of Sigma; ::_thesis: for BSeq being SetSequence of Omega st ( for n being Element of NAT holds BSeq . n is thin of P ) holds
ex CSeq being SetSequence of Sigma st
for n being Element of NAT holds
( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 )
let BSeq be SetSequence of Omega; ::_thesis: ( ( for n being Element of NAT holds BSeq . n is thin of P ) implies ex CSeq being SetSequence of Sigma st
for n being Element of NAT holds
( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 ) )
defpred S1[ Element of NAT , set ] means  for n being Element of NAT
for y being set st n = $1 & y = $2 holds
( y in Sigma & BSeq . n c= y & P . y = 0 );
assume A1: for n being Element of NAT holds BSeq . n is thin of P ; ::_thesis: ex CSeq being SetSequence of Sigma st
for n being Element of NAT holds
( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 )
A2: for t being Element of NAT ex A being Element of Sigma st S1[t,A]
proof
let t be Element of NAT ; ::_thesis: ex A being Element of Sigma st S1[t,A]
 BSeq . t is thin of P by A1;
then consider A being set  such that
A3: A in Sigma and
A4: ( BSeq . t c= A & P . A = 0 ) by Def4;
reconsider A = A as Element of Sigma by A3;
take  A ; ::_thesis: S1[t,A]
thus  S1[t,A] by A4; ::_thesis: verum
end;
 ex G being Function of NAT,Sigma st
for t being Element of NAT holds S1[t,G . t] from FUNCT_2:sch_3(A2);
then consider G being Function of NAT,Sigma such that
A5: for t, n being Element of NAT
for y being set st n = t & y = G . t holds
( y in Sigma & BSeq . n c= y & P . y = 0 ) ;
reconsider CSeq = G as SetSequence of Omega by FUNCT_2:7;
reconsider CSeq = CSeq as SetSequence of Sigma ;
take  CSeq ; ::_thesis: for n being Element of NAT holds
( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 )
thus  for n being Element of NAT holds
( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 ) by A5; ::_thesis: verum
end;

theorem Th34: :: PROB_4:34
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for D being non empty Subset-Family of Omega st ( for A being set holds
( A in D iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) holds
D is SigmaField of Omega
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for D being non empty Subset-Family of Omega st ( for A being set holds
( A in D iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) holds
D is SigmaField of Omega
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for D being non empty Subset-Family of Omega st ( for A being set holds
( A in D iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) holds
D is SigmaField of Omega
let P be Probability of Sigma; ::_thesis: for D being non empty Subset-Family of Omega st ( for A being set holds
( A in D iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) holds
D is SigmaField of Omega
let D be non empty Subset-Family of Omega; ::_thesis: ( ( for A being set holds
( A in D iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) implies D is SigmaField of Omega )
assume A1: for A being set holds
( A in D iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ; ::_thesis: D is SigmaField of Omega
A2: for A1 being SetSequence of Omega st rng A1 c= D holds
Union A1 in D
proof
let A1 be SetSequence of Omega; ::_thesis: ( rng A1 c= D implies Union A1 in D )
reconsider F = A1 as Function of NAT,(bool Omega) ;
A3: dom F = NAT by FUNCT_2:def_1;
assume A4: rng A1 c= D ; ::_thesis: Union A1 in D
A5: for n being Element of NAT ex B being set st
( B in Sigma & ex C being thin of P st F . n = B \/ C )
proof
let n be Element of NAT ; ::_thesis: ex B being set st
( B in Sigma & ex C being thin of P st F . n = B \/ C )
 F . n in rng F by NAT_1:51;
hence  ex B being set st
( B in Sigma & ex C being thin of P st F . n = B \/ C ) by A1, A4; ::_thesis: verum
end;
 for n being Element of NAT holds F . n in COM (Sigma,P)
proof
let n be Element of NAT ; ::_thesis: F . n in COM (Sigma,P)
 ex B being set st
( B in Sigma & ex C being thin of P st F . n = B \/ C ) by A5;
hence  F . n in COM (Sigma,P) by Def5; ::_thesis: verum
end;
then  for n being set st n in NAT holds
F . n in COM (Sigma,P) ;
then reconsider F = F as Function of NAT,(COM (Sigma,P)) by A3, FUNCT_2:3;
consider BSeq being SetSequence of Sigma such that
A6: for n being Element of NAT holds BSeq . n in ProbPart (F . n) by Th31;
consider CSeq being SetSequence of Omega such that
A7: for n being Element of NAT holds CSeq . n = (F . n) \ (BSeq . n) by Th32;
A8: for n being Element of NAT holds
( BSeq . n in Sigma & BSeq . n c= F . n & (F . n) \ (BSeq . n) is thin of P )
proof
let n be Element of NAT ; ::_thesis: ( BSeq . n in Sigma & BSeq . n c= F . n & (F . n) \ (BSeq . n) is thin of P )
 BSeq . n in ProbPart (F . n) by A6;
hence  ( BSeq . n in Sigma & BSeq . n c= F . n & (F . n) \ (BSeq . n) is thin of P ) by Def7; ::_thesis: verum
end;
 for n being Element of NAT holds CSeq . n is thin of P
proof
let n be Element of NAT ; ::_thesis: CSeq . n is thin of P
 (F . n) \ (BSeq . n) is thin of P by A8;
hence  CSeq . n is thin of P by A7; ::_thesis: verum
end;
then consider DSeq being SetSequence of Sigma such that
A9: for n being Element of NAT holds
( CSeq . n c= DSeq . n & P . (DSeq . n) = 0 ) by Th33;
A10: Union A1 = union (rng A1) by CARD_3:def_4;
 ex B being set st
( B in Sigma & ex C being thin of P st Union A1 = B \/ C )
proof
set B = union (rng BSeq);
take  union (rng BSeq) ; ::_thesis: ( union (rng BSeq) in Sigma & ex C being thin of P st Union A1 = (union (rng BSeq)) \/ C )
A11: union (rng BSeq) c= union (rng F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng BSeq) or x in union (rng F) )
assume  x in union (rng BSeq) ; ::_thesis: x in union (rng F)
then consider Z being set  such that
A12: x in Z and
A13: Z in rng BSeq by TARSKI:def_4;
 dom BSeq = NAT by FUNCT_2:def_1;
then consider n being set  such that
A14: n in NAT and
A15: Z = BSeq . n by A13, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A14;
set P = F . n;
A16: BSeq . n c= F . n by A8;
 ex P being set st
( P in rng F & x in P )
proof
take  F . n ; ::_thesis: ( F . n in rng F & x in F . n )
thus  ( F . n in rng F & x in F . n ) by A3, A12, A15, A16, FUNCT_1:def_3; ::_thesis: verum
end;
hence  x in union (rng F) by TARSKI:def_4; ::_thesis: verum
end;
A17: ex C being thin of P st Union A1 = (union (rng BSeq)) \/ C
proof
set C = (Union A1) \ (union (rng BSeq));
 Union DSeq in Sigma by PROB_1:17;
then A18: union (rng DSeq) in Sigma by CARD_3:def_4;
A19: (Union A1) \ (union (rng BSeq)) c= union (rng CSeq)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Union A1) \ (union (rng BSeq)) or x in union (rng CSeq) )
assume A20: x in (Union A1) \ (union (rng BSeq)) ; ::_thesis: x in union (rng CSeq)
then  x in union (rng F) by A10, XBOOLE_0:def_5;
then consider Z being set  such that
A21: x in Z and
A22: Z in rng F by TARSKI:def_4;
consider n being set  such that
A23: n in NAT and
A24: Z = F . n by A3, A22, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A23;
A25: not x in union (rng BSeq) by A20, XBOOLE_0:def_5;
 not x in BSeq . n
proof
 dom BSeq = NAT by FUNCT_2:def_1;
then A26: BSeq . n in rng BSeq by FUNCT_1:def_3;
assume  x in BSeq . n ; ::_thesis: contradiction
hence  contradiction by A25, A26, TARSKI:def_4; ::_thesis: verum
end;
then A27: x in (F . n) \ (BSeq . n) by A21, A24, XBOOLE_0:def_5;
 ex Z being set st
( x in Z & Z in rng CSeq )
proof
take  CSeq . n ; ::_thesis: ( x in CSeq . n & CSeq . n in rng CSeq )
 dom CSeq = NAT by FUNCT_2:def_1;
hence  ( x in CSeq . n & CSeq . n in rng CSeq ) by A7, A27, FUNCT_1:def_3; ::_thesis: verum
end;
hence  x in union (rng CSeq) by TARSKI:def_4; ::_thesis: verum
end;
 for A being set st A in rng DSeq holds
P . A = 0
proof
let A be set ; ::_thesis: ( A in rng DSeq implies P . A = 0 )
A28: dom DSeq = NAT by FUNCT_2:def_1;
assume  A in rng DSeq ; ::_thesis: P . A = 0
then  ex n being set st
( n in NAT & A = DSeq . n ) by A28, FUNCT_1:def_3;
hence  P . A = 0 by A9; ::_thesis: verum
end;
then A29: P . (union (rng DSeq)) = 0 by Th8;
 union (rng CSeq) c= union (rng DSeq)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng CSeq) or x in union (rng DSeq) )
assume  x in union (rng CSeq) ; ::_thesis: x in union (rng DSeq)
then consider Z being set  such that
A30: x in Z and
A31: Z in rng CSeq by TARSKI:def_4;
 dom CSeq = NAT by FUNCT_2:def_1;
then consider n being set  such that
A32: n in NAT and
A33: Z = CSeq . n by A31, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A32;
 n in dom DSeq by A32, FUNCT_2:def_1;
then A34: DSeq . n in rng DSeq by FUNCT_1:def_3;
 CSeq . n c= DSeq . n by A9;
hence  x in union (rng DSeq) by A30, A33, A34, TARSKI:def_4; ::_thesis: verum
end;
then  (Union A1) \ (union (rng BSeq)) c= union (rng DSeq) by A19, XBOOLE_1:1;
then A35: (Union A1) \ (union (rng BSeq)) is thin of P by A29, A18, Def4;
Union A1 = ((Union A1) \ (union (rng BSeq))) \/ ((union (rng F)) /\ (union (rng BSeq))) by A10, XBOOLE_1:51
.= (union (rng BSeq)) \/ ((Union A1) \ (union (rng BSeq))) by A11, XBOOLE_1:28 ;
then consider C being thin of P such that
A36: Union A1 = (union (rng BSeq)) \/ C by A35;
take  C ; ::_thesis: Union A1 = (union (rng BSeq)) \/ C
thus  Union A1 = (union (rng BSeq)) \/ C by A36; ::_thesis: verum
end;
 Union BSeq in Sigma by PROB_1:17;
hence  ( union (rng BSeq) in Sigma & ex C being thin of P st Union A1 = (union (rng BSeq)) \/ C ) by A17, CARD_3:def_4; ::_thesis: verum
end;
hence  Union A1 in D by A1; ::_thesis: verum
end;
 for A being Subset of Omega st A in D holds
A ` in D
proof
let A be Subset of Omega; ::_thesis: ( A in D implies A ` in D )
assume A37: A in D ; ::_thesis: A ` in D
 ex Q being set st
( Q in Sigma & ex W being thin of P st Omega \ A = Q \/ W )
proof
consider B being set  such that
A38: B in Sigma and
A39: ex C being thin of P st A = B \/ C by A1, A37;
consider C being thin of P such that
A40: A = B \/ C by A39;
reconsider B = B as Subset of Omega by A38;
set H = Omega \ B;
consider G being set  such that
A41: G in Sigma and
A42: C c= G and
A43: P . G = 0 by Def4;
set Q = (Omega \ B) \ G;
A44: Omega \ A = (Omega \ B) \ C by A40, XBOOLE_1:41;
A45: ex W being thin of P st Omega \ A = ((Omega \ B) \ G) \/ W
proof
set W = (Omega \ B) /\ (G \ C);
 (Omega \ B) /\ (G \ C) c= Omega \ B by XBOOLE_1:17;
then reconsider W = (Omega \ B) /\ (G \ C) as Subset of Omega by XBOOLE_1:1;
reconsider W = W as thin of P by A41, A43, Def4;
take  W ; ::_thesis: Omega \ A = ((Omega \ B) \ G) \/ W
thus  Omega \ A = ((Omega \ B) \ G) \/ W by A42, A44, Lm1; ::_thesis: verum
end;
take  (Omega \ B) \ G ; ::_thesis: ( (Omega \ B) \ G in Sigma & ex W being thin of P st Omega \ A = ((Omega \ B) \ G) \/ W )
 B ` in Sigma by A38, PROB_1:def_1;
hence  ( (Omega \ B) \ G in Sigma & ex W being thin of P st Omega \ A = ((Omega \ B) \ G) \/ W ) by A41, A45, PROB_1:6; ::_thesis: verum
end;
hence  A ` in D by A1; ::_thesis: verum
end;
hence  D is SigmaField of Omega by A2, Th4; ::_thesis: verum
end;

registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
cluster COM (Sigma,P) ->  non empty compl-closed sigma-multiplicative ;
coherence
 ( COM (Sigma,P) is compl-closed & COM (Sigma,P) is sigma-multiplicative )
proof
 for A being set holds
( A in COM (Sigma,P) iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) by Def5;
hence  ( COM (Sigma,P) is compl-closed & COM (Sigma,P) is sigma-multiplicative ) by Th34; ::_thesis: verum
end;
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
:: original: thin
redefine mode thin of P ->  Event of COM (Sigma,P);
coherence
 for b1 being thin of P holds b1 is Event of COM (Sigma,P) by Th26;
end;

theorem Th35: :: PROB_4:35
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being set holds
( A in COM (Sigma,P) iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) )
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being set holds
( A in COM (Sigma,P) iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) )
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for A being set holds
( A in COM (Sigma,P) iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) )
let P be Probability of Sigma; ::_thesis: for A being set holds
( A in COM (Sigma,P) iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) )
let A be set ; ::_thesis: ( A in COM (Sigma,P) iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) )
thus  ( A in COM (Sigma,P) implies ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) ) ::_thesis: ( ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) implies A in COM (Sigma,P) )
proof
assume  A in COM (Sigma,P) ; ::_thesis: ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 )
then consider B being set  such that
A1: B in Sigma and
A2: ex C being thin of P st A = B \/ C by Def5;
consider C being thin of P such that
A3: A = B \/ C by A2;
reconsider B = B as Event of Sigma by A1;
consider D being set  such that
A4: D in Sigma and
A5: C c= D and
A6: P . D = 0 by Def4;
reconsider D = D as Event of Sigma by A4;
reconsider E = D \/ B as Event of Sigma ;
A7: P . (D \/ B) <= (P . D) + (P . B) by PROB_1:39;
P . (E \ B) = P . (D \ B) by XBOOLE_1:40
.= (P . (D \/ B)) - (P . B) by Th5 ;
then  P . (E \ B) <= 0 by A6, A7, XREAL_1:47;
then A8: P . (E \ B) = 0 by PROB_1:def_8;
 A c= E by A3, A5, XBOOLE_1:9;
hence  ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) by A2, A8, XBOOLE_1:7; ::_thesis: verum
end;
thus  ( ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) implies A in COM (Sigma,P) ) ::_thesis: verum
proof
given A1, A2 being set  such that A9: A1 in Sigma and
A10: A2 in Sigma and
A11: A1 c= A and
A12: A c= A2 and
A13: P . (A2 \ A1) = 0 ; ::_thesis: A in COM (Sigma,P)
reconsider A2 = A2 as Element of Sigma by A10;
reconsider A1 = A1 as Element of Sigma by A9;
set C = A \ A1;
A14: A \ A1 is thin of P
proof
reconsider D = A2 \ A1 as Element of Sigma ;
A15: A \ A1 c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A \ A1 or x in D )
assume  x in A \ A1 ; ::_thesis: x in D
then  ( x in A & not x in A1 ) by XBOOLE_0:def_5;
hence  x in D by A12, XBOOLE_0:def_5; ::_thesis: verum
end;
then  A \ A1 c= Omega by XBOOLE_1:1;
hence  A \ A1 is thin of P by A13, A15, Def4; ::_thesis: verum
end;
 A = A1 \/ (A \ A1) by A11, XBOOLE_1:45;
hence  A in COM (Sigma,P) by A14, Def5; ::_thesis: verum
end;
end;

theorem :: PROB_4:36
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for C being non empty Subset-Family of Omega st ( for A being set holds
( A in C iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) ) ) holds
C = COM (Sigma,P)
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for C being non empty Subset-Family of Omega st ( for A being set holds
( A in C iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) ) ) holds
C = COM (Sigma,P)
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for C being non empty Subset-Family of Omega st ( for A being set holds
( A in C iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) ) ) holds
C = COM (Sigma,P)
let P be Probability of Sigma; ::_thesis: for C being non empty Subset-Family of Omega st ( for A being set holds
( A in C iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) ) ) holds
C = COM (Sigma,P)
let C be non empty Subset-Family of Omega; ::_thesis: ( ( for A being set holds
( A in C iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) ) ) implies C = COM (Sigma,P) )
assume A1: for A being set holds
( A in C iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) ) ; ::_thesis: C = COM (Sigma,P)
now__::_thesis:_for_A_being_set_holds_
(_A_in_C_iff_A_in_COM_(Sigma,P)_)
let A be set ; ::_thesis: ( A in C iff A in COM (Sigma,P) )
 ( A in C iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) ) by A1;
hence  ( A in C iff A in COM (Sigma,P) ) by Th35; ::_thesis: verum
end;
hence  C = COM (Sigma,P) by TARSKI:1; ::_thesis: verum
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
func COM P ->  Probability of COM (Sigma,P) means :Def8: :: PROB_4:def 8
 for B being set st B in Sigma holds
for C being thin of P holds it . (B \/ C) = P . B;
existence
 ex b1 being Probability of COM (Sigma,P) st
for B being set st B in Sigma holds
for C being thin of P holds b1 . (B \/ C) = P . B
proof
reconsider C = {} as thin of P by Th24;
defpred S1[ set , set ] means  for x, y being set st x in COM (Sigma,P) & x = $1 & y = $2 holds
for B being set st B in Sigma holds
for C being thin of P st x = B \/ C holds
y = P . B;
set B = {} ;
A1: {} is thin of P by Th24;
A2: for x being set st x in COM (Sigma,P) holds
ex y being set st
( y in REAL & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in COM (Sigma,P) implies ex y being set st
( y in REAL & S1[x,y] ) )
assume  x in COM (Sigma,P) ; ::_thesis: ex y being set st
( y in REAL & S1[x,y] )
then consider B being set  such that
A3: ( B in Sigma & ex C being thin of P st x = B \/ C ) by Def5;
take  P . B ; ::_thesis: ( P . B in REAL & S1[x,P . B] )
thus  ( P . B in REAL & S1[x,P . B] ) by A3, Th25, FUNCT_2:5; ::_thesis: verum
end;
consider comP being Function of (COM (Sigma,P)),REAL such that
A4: for x being set st x in COM (Sigma,P) holds
S1[x,comP . x] from FUNCT_2:sch_1(A2);
A5: for B being set st B in Sigma holds
for C being thin of P holds comP . (B \/ C) = P . B
proof
let B be set ; ::_thesis: ( B in Sigma implies for C being thin of P holds comP . (B \/ C) = P . B )
assume A6: B in Sigma ; ::_thesis: for C being thin of P holds comP . (B \/ C) = P . B
let C be thin of P; ::_thesis: comP . (B \/ C) = P . B
 B \/ C in COM (Sigma,P) by A6, Def5;
hence  comP . (B \/ C) = P . B by A4, A6; ::_thesis: verum
end;
A7: for BSeq being SetSequence of COM (Sigma,P) st BSeq is V118() holds
Sum (comP * BSeq) = comP . (Union BSeq)
proof
let BSeq be SetSequence of COM (Sigma,P); ::_thesis: ( BSeq is V118() implies Sum (comP * BSeq) = comP . (Union BSeq) )
assume A8: BSeq is V118() ; ::_thesis: Sum (comP * BSeq) = comP . (Union BSeq)
reconsider F = BSeq as Function of NAT,(bool Omega) ;
 rng F c= COM (Sigma,P) by RELAT_1:def_19;
then reconsider F = F as Function of NAT,(COM (Sigma,P)) by FUNCT_2:6;
consider CSeq being SetSequence of Sigma such that
A9: for n being Element of NAT holds CSeq . n in ProbPart (F . n) by Th31;
consider B being set  such that
A10: B = union (rng CSeq) ;
 Union CSeq in Sigma by PROB_1:17;
then reconsider B = B as Element of Sigma by A10, CARD_3:def_4;
consider DSeq being SetSequence of Omega such that
A11: for n being Element of NAT holds DSeq . n = (F . n) \ (CSeq . n) by Th32;
A12: for n being Element of NAT holds
( CSeq . n in Sigma & CSeq . n c= F . n & (F . n) \ (CSeq . n) is thin of P )
proof
let n be Element of NAT ; ::_thesis: ( CSeq . n in Sigma & CSeq . n c= F . n & (F . n) \ (CSeq . n) is thin of P )
 CSeq . n in ProbPart (F . n) by A9;
hence  ( CSeq . n in Sigma & CSeq . n c= F . n & (F . n) \ (CSeq . n) is thin of P ) by Def7; ::_thesis: verum
end;
 for n being Element of NAT holds DSeq . n is thin of P
proof
let n be Element of NAT ; ::_thesis: DSeq . n is thin of P
 (F . n) \ (CSeq . n) is thin of P by A12;
hence  DSeq . n is thin of P by A11; ::_thesis: verum
end;
then consider ESeq being SetSequence of Sigma such that
A13: for n being Element of NAT holds
( DSeq . n c= ESeq . n & P . (ESeq . n) = 0 ) by Th33;
A14: dom BSeq = NAT by FUNCT_2:def_1;
A15: B c= union (rng F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in union (rng F) )
assume  x in B ; ::_thesis: x in union (rng F)
then consider Z being set  such that
A16: x in Z and
A17: Z in rng CSeq by A10, TARSKI:def_4;
 dom CSeq = NAT by FUNCT_2:def_1;
then consider n being set  such that
A18: n in NAT and
A19: Z = CSeq . n by A17, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A18;
set P = F . n;
A20: CSeq . n c= F . n by A12;
 ex P being set st
( P in rng F & x in P )
proof
take  F . n ; ::_thesis: ( F . n in rng F & x in F . n )
thus  ( F . n in rng F & x in F . n ) by A14, A16, A19, A20, FUNCT_1:def_3; ::_thesis: verum
end;
hence  x in union (rng F) by TARSKI:def_4; ::_thesis: verum
end;
A21: ex C being thin of P st union (rng F) = B \/ C
proof
set C = (union (rng F)) \ B;
A22: union (rng F) = ((union (rng F)) \ B) \/ ((union (rng F)) /\ B) by XBOOLE_1:51
.= B \/ ((union (rng F)) \ B) by A15, XBOOLE_1:28 ;
reconsider C = (union (rng F)) \ B as Subset of Omega ;
A23: C c= union (rng DSeq)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in union (rng DSeq) )
assume A24: x in C ; ::_thesis: x in union (rng DSeq)
then  x in union (rng F) by XBOOLE_0:def_5;
then consider Z being set  such that
A25: x in Z and
A26: Z in rng F by TARSKI:def_4;
consider n being set  such that
A27: n in NAT and
A28: Z = F . n by A14, A26, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A27;
A29: not x in union (rng CSeq) by A10, A24, XBOOLE_0:def_5;
 not x in CSeq . n
proof
 dom CSeq = NAT by FUNCT_2:def_1;
then A30: CSeq . n in rng CSeq by FUNCT_1:def_3;
assume  x in CSeq . n ; ::_thesis: contradiction
hence  contradiction by A29, A30, TARSKI:def_4; ::_thesis: verum
end;
then A31: x in (F . n) \ (CSeq . n) by A25, A28, XBOOLE_0:def_5;
 ex Z being set st
( x in Z & Z in rng DSeq )
proof
take  DSeq . n ; ::_thesis: ( x in DSeq . n & DSeq . n in rng DSeq )
 dom DSeq = NAT by FUNCT_2:def_1;
hence  ( x in DSeq . n & DSeq . n in rng DSeq ) by A11, A31, FUNCT_1:def_3; ::_thesis: verum
end;
hence  x in union (rng DSeq) by TARSKI:def_4; ::_thesis: verum
end;
 for A being set st A in rng ESeq holds
P . A = 0
proof
let A be set ; ::_thesis: ( A in rng ESeq implies P . A = 0 )
A32: dom ESeq = NAT by FUNCT_2:def_1;
assume  A in rng ESeq ; ::_thesis: P . A = 0
then  ex n being set st
( n in NAT & A = ESeq . n ) by A32, FUNCT_1:def_3;
hence  P . A = 0 by A13; ::_thesis: verum
end;
then A33: P . (union (rng ESeq)) = 0 by Th8;
 Union ESeq in Sigma by PROB_1:17;
then A34: union (rng ESeq) in Sigma by CARD_3:def_4;
 union (rng DSeq) c= union (rng ESeq)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng DSeq) or x in union (rng ESeq) )
assume  x in union (rng DSeq) ; ::_thesis: x in union (rng ESeq)
then consider Z being set  such that
A35: x in Z and
A36: Z in rng DSeq by TARSKI:def_4;
 dom DSeq = NAT by FUNCT_2:def_1;
then consider n being set  such that
A37: n in NAT and
A38: Z = DSeq . n by A36, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A37;
 n in dom ESeq by A37, FUNCT_2:def_1;
then A39: ESeq . n in rng ESeq by FUNCT_1:def_3;
 DSeq . n c= ESeq . n by A13;
hence  x in union (rng ESeq) by A35, A38, A39, TARSKI:def_4; ::_thesis: verum
end;
then  C c= union (rng ESeq) by A23, XBOOLE_1:1;
then  C is thin of P by A34, A33, Def4;
then consider C being thin of P such that
A40: union (rng F) = B \/ C by A22;
take  C ; ::_thesis: union (rng F) = B \/ C
thus  union (rng F) = B \/ C by A40; ::_thesis: verum
end;
 for n, m being set st n <> m holds
CSeq . n misses CSeq . m
proof
let n, m be set ; ::_thesis: ( n <> m implies CSeq . n misses CSeq . m )
A41: dom F = NAT by FUNCT_2:def_1
.= dom CSeq by FUNCT_2:def_1 ;
 for n being set holds CSeq . n c= F . n
proof
let n be set ; ::_thesis: CSeq . n c= F . n
percases ( n in dom F or not n in dom F ) ;
suppose n in dom F ; ::_thesis: CSeq . n c= F . n
hence  CSeq . n c= F . n by A12; ::_thesis: verum
end;
supposeA42: not n in dom F ; ::_thesis: CSeq . n c= F . n
then F . n = {} by FUNCT_1:def_2
.= CSeq . n by A41, A42, FUNCT_1:def_2 ;
hence  CSeq . n c= F . n ; ::_thesis: verum
end;
end;
end;
then A43: ( CSeq . n c= F . n & CSeq . m c= F . m ) ;
assume  n <> m ; ::_thesis: CSeq . n misses CSeq . m
then  F . n misses F . m by A8, PROB_2:def_2;
then  (F . n) /\ (F . m) = {} by XBOOLE_0:def_7;
then  (CSeq . n) /\ (CSeq . m) = {} by A43, XBOOLE_1:3, XBOOLE_1:27;
hence  CSeq . n misses CSeq . m by XBOOLE_0:def_7; ::_thesis: verum
end;
then A44: CSeq is V118() by PROB_2:def_2;
 Sum (comP * F) = comP . (Union F)
proof
A45: for n being Element of NAT holds comP . (F . n) = P . (CSeq . n)
proof
let n be Element of NAT ; ::_thesis: comP . (F . n) = P . (CSeq . n)
 (F . n) \ (CSeq . n) is thin of P by A12;
then consider C being thin of P such that
A46: C = (F . n) \ (CSeq . n) ;
F . n = ((F . n) /\ (CSeq . n)) \/ ((F . n) \ (CSeq . n)) by XBOOLE_1:51
.= (CSeq . n) \/ C by A12, A46, XBOOLE_1:28 ;
hence  comP . (F . n) = P . (CSeq . n) by A5; ::_thesis: verum
end;
 for x being Element of NAT holds (comP * F) . x = (P * CSeq) . x
proof
let x be Element of NAT ; ::_thesis: (comP * F) . x = (P * CSeq) . x
(comP * F) . x = comP . (F . x) by FUNCT_2:15
.= P . (CSeq . x) by A45
.= (P * CSeq) . x by FUNCT_2:15 ;
hence  (comP * F) . x = (P * CSeq) . x ; ::_thesis: verum
end;
then A47: Sum (comP * F) = Sum (P * CSeq) by FUNCT_2:63;
 comP . (union (rng F)) = P . (union (rng CSeq)) by A5, A10, A21;
then comP . (Union F) = P . (union (rng CSeq)) by CARD_3:def_4
.= P . (Union CSeq) by CARD_3:def_4 ;
hence  Sum (comP * F) = comP . (Union F) by A44, A47, PROB_3:46; ::_thesis: verum
end;
hence  Sum (comP * BSeq) = comP . (Union BSeq) ; ::_thesis: verum
end;
A48: for x being Element of COM (Sigma,P) holds comP . x >= 0
proof
let x be Element of COM (Sigma,P); ::_thesis: comP . x >= 0
consider B being set  such that
A49: B in Sigma and
A50: ex C being thin of P st x = B \/ C by Def5;
reconsider B = B as Element of Sigma by A49;
 comP . x = P . B by A4, A50;
hence  comP . x >= 0 by PROB_1:def_8; ::_thesis: verum
end;
 {} = {} \/ C ;
then A51: comP . {} = P . {} by A5, PROB_1:4
.= 0 by VALUED_0:def_19 ;
A52: for A, B being Event of COM (Sigma,P) st A misses B holds
comP . (A \/ B) = (comP . A) + (comP . B)
proof
let A, B be Event of COM (Sigma,P); ::_thesis: ( A misses B implies comP . (A \/ B) = (comP . A) + (comP . B) )
assume A53: A misses B ; ::_thesis: comP . (A \/ B) = (comP . A) + (comP . B)
reconsider A1 = A, B1 = B as Subset of Omega ;
reconsider BSeq = (A1,B1) followed_by ({} Omega) as SetSequence of Omega ;
A54: BSeq . 1 = B by FUNCT_7:123;
A55: BSeq . 0 = A by FUNCT_7:122;
 for n being Nat holds BSeq . n in COM (Sigma,P)
proof
let n be Nat; ::_thesis: BSeq . n in COM (Sigma,P)
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: BSeq . n in COM (Sigma,P)
hence  BSeq . n in COM (Sigma,P) by A55; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: BSeq . n in COM (Sigma,P)
then  n >= 1 by NAT_1:14;
then A56: n + 1 > 1 by NAT_1:13;
percases ( n > 1 or n = 1 ) by A56, NAT_1:22;
suppose n > 1 ; ::_thesis: BSeq . n in COM (Sigma,P)
then  BSeq . n = {} by FUNCT_7:124;
hence  BSeq . n in COM (Sigma,P) by PROB_1:4; ::_thesis: verum
end;
suppose n = 1 ; ::_thesis: BSeq . n in COM (Sigma,P)
hence  BSeq . n in COM (Sigma,P) by A54; ::_thesis: verum
end;
end;
end;
end;
end;
then  rng BSeq c= COM (Sigma,P) by NAT_1:52;
then reconsider BSeq = BSeq as SetSequence of COM (Sigma,P) by RELAT_1:def_19;
 for m being Element of NAT st 2 <= m holds
(Partial_Sums (comP * BSeq)) . m = (comP . A) + (comP . B)
proof
A57: (Partial_Sums (comP * BSeq)) . 0 = (comP * BSeq) . 0 by SERIES_1:def_1
.= comP . A by A55, FUNCT_2:15 ;
 0 + 1 = 1 ;
then A58: (Partial_Sums (comP * BSeq)) . 1 = ((Partial_Sums (comP * BSeq)) . 0) + ((comP * BSeq) . 1) by SERIES_1:def_1
.= (comP . A) + (comP . B) by A54, A57, FUNCT_2:15 ;
A59: for n being Element of NAT holds (Partial_Sums (comP * BSeq)) . (2 + n) = (comP . A) + (comP . B)
proof
defpred S2[ Element of NAT ] means (Partial_Sums (comP * BSeq)) . (2 + $1) = (comP . A) + (comP . B);
A60: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A61: S2[k] ; ::_thesis: S2[k + 1]
A62: (2 + k) + 1 > 0 + 1 by XREAL_1:8;
thus (Partial_Sums (comP * BSeq)) . (2 + (k + 1)) = ((Partial_Sums (comP * BSeq)) . (2 + k)) + ((comP * BSeq) . ((2 + k) + 1)) by SERIES_1:def_1
.= ((comP . A) + (comP . B)) + (comP . (BSeq . ((2 + k) + 1))) by A61, FUNCT_2:15
.= ((comP . A) + (comP . B)) + (comP . {}) by A62, FUNCT_7:124
.= (comP . A) + (comP . B) by A51 ; ::_thesis: verum
end;
 2 = 1 + 1 ;
then (Partial_Sums (comP * BSeq)) . (2 + 0) = ((Partial_Sums (comP * BSeq)) . 1) + ((comP * BSeq) . 2) by SERIES_1:def_1
.= ((comP . A) + (comP . B)) + (comP . (BSeq . 2)) by A58, FUNCT_2:15
.= ((comP . A) + (comP . B)) + (comP . {}) by FUNCT_7:124
.= (comP . A) + (comP . B) by A51 ;
then A63: S2[ 0 ] ;
thus  for k being Element of NAT holds S2[k] from NAT_1:sch_1(A63, A60); ::_thesis: verum
end;
let m be Element of NAT ; ::_thesis: ( 2 <= m implies (Partial_Sums (comP * BSeq)) . m = (comP . A) + (comP . B) )
assume  2 <= m ; ::_thesis: (Partial_Sums (comP * BSeq)) . m = (comP . A) + (comP . B)
then consider k being Nat such that
A64: m = 2 + k by NAT_1:10;
 k in NAT by ORDINAL1:def_12;
hence  (Partial_Sums (comP * BSeq)) . m = (comP . A) + (comP . B) by A59, A64; ::_thesis: verum
end;
then A65: ( Union BSeq = A \/ B & Sum (comP * BSeq) = (comP . A) + (comP . B) ) by DYNKIN:3, PROB_1:1;
 BSeq is V118() by A53, Th3;
hence  comP . (A \/ B) = (comP . A) + (comP . B) by A7, A65; ::_thesis: verum
end;
A66: for A, B being Event of COM (Sigma,P) st A c= B holds
comP . (B \ A) = (comP . B) - (comP . A)
proof
let A, B be Event of COM (Sigma,P); ::_thesis: ( A c= B implies comP . (B \ A) = (comP . B) - (comP . A) )
assume A67: A c= B ; ::_thesis: comP . (B \ A) = (comP . B) - (comP . A)
(comP . A) + (comP . (B \ A)) = comP . (A \/ (B \ A)) by A52, XBOOLE_1:79
.= comP . B by A67, XBOOLE_1:45 ;
hence  comP . (B \ A) = (comP . B) - (comP . A) ; ::_thesis: verum
end;
A68: for A, B being Event of COM (Sigma,P) st A c= B holds
comP . A <= comP . B
proof
let A, B be Event of COM (Sigma,P); ::_thesis: ( A c= B implies comP . A <= comP . B )
assume  A c= B ; ::_thesis: comP . A <= comP . B
then  comP . (B \ A) = (comP . B) - (comP . A) by A66;
then  0 <= (comP . B) - (comP . A) by A48;
then  0 + (comP . A) <= comP . B by XREAL_1:19;
hence  comP . A <= comP . B ; ::_thesis: verum
end;
A69: for BSeq being SetSequence of COM (Sigma,P) st BSeq is non-descending holds
comP * BSeq is non-decreasing
proof
let BSeq be SetSequence of COM (Sigma,P); ::_thesis: ( BSeq is non-descending implies comP * BSeq is non-decreasing )
assume A70: BSeq is non-descending ; ::_thesis: comP * BSeq is non-decreasing
 for n, m being Element of NAT st n <= m holds
(comP * BSeq) . n <= (comP * BSeq) . m
proof
let n, m be Element of NAT ; ::_thesis: ( n <= m implies (comP * BSeq) . n <= (comP * BSeq) . m )
assume  n <= m ; ::_thesis: (comP * BSeq) . n <= (comP * BSeq) . m
then  BSeq . n c= BSeq . m by A70, PROB_1:def_5;
then  comP . (BSeq . n) <= comP . (BSeq . m) by A68;
then  (comP * BSeq) . n <= comP . (BSeq . m) by FUNCT_2:15;
hence  (comP * BSeq) . n <= (comP * BSeq) . m by FUNCT_2:15; ::_thesis: verum
end;
hence  comP * BSeq is non-decreasing by SEQM_3:6; ::_thesis: verum
end;
A71: comP . Omega = comP . ({} \/ Omega)
.= P . Omega by A5, A1, PROB_1:5
.= 1 by PROB_1:def_8 ;
A72: for A being Event of COM (Sigma,P) holds comP . A <= 1
proof
reconsider B = Omega as Event of COM (Sigma,P) by PROB_1:23;
let A be Event of COM (Sigma,P); ::_thesis: comP . A <= 1
 comP . A <= comP . B by A68;
hence  comP . A <= 1 by A71; ::_thesis: verum
end;
A73: for BSeq being SetSequence of COM (Sigma,P)
for n being Element of NAT holds (comP * BSeq) . n <= 1
proof
let BSeq be SetSequence of COM (Sigma,P); ::_thesis: for n being Element of NAT holds (comP * BSeq) . n <= 1
let n be Element of NAT ; ::_thesis: (comP * BSeq) . n <= 1
 (comP * BSeq) . n = comP . (BSeq . n) by FUNCT_2:15;
hence  (comP * BSeq) . n <= 1 by A72; ::_thesis: verum
end;
A74: for BSeq being SetSequence of COM (Sigma,P) st BSeq is non-descending holds
( comP * BSeq is V101() & comP * BSeq is convergent )
proof
let BSeq be SetSequence of COM (Sigma,P); ::_thesis: ( BSeq is non-descending implies ( comP * BSeq is V101() & comP * BSeq is convergent ) )
assume  BSeq is non-descending ; ::_thesis: ( comP * BSeq is V101() & comP * BSeq is convergent )
then A75: comP * BSeq is non-decreasing by A69;
 for n being Element of NAT holds (comP * BSeq) . n < 2
proof
let n be Element of NAT ; ::_thesis: (comP * BSeq) . n < 2
 ((comP * BSeq) . n) + 0 < 1 + 1 by A73, XREAL_1:8;
hence  (comP * BSeq) . n < 2 ; ::_thesis: verum
end;
hence  comP * BSeq is V101() by SEQ_2:def_3; ::_thesis: comP * BSeq is convergent
hence  comP * BSeq is convergent by A75; ::_thesis: verum
end;
 for BSeq being SetSequence of COM (Sigma,P) st BSeq is non-descending holds
( comP * BSeq is convergent & lim (comP * BSeq) = comP . (Union BSeq) )
proof
let BSeq be SetSequence of COM (Sigma,P); ::_thesis: ( BSeq is non-descending implies ( comP * BSeq is convergent & lim (comP * BSeq) = comP . (Union BSeq) ) )
assume A76: BSeq is non-descending ; ::_thesis: ( comP * BSeq is convergent & lim (comP * BSeq) = comP . (Union BSeq) )
reconsider CSeq = Partial_Diff_Union BSeq as SetSequence of COM (Sigma,P) ;
A77: for n being Element of NAT holds (Partial_Sums (comP * CSeq)) . n = (comP * BSeq) . n
proof
defpred S2[ Element of NAT ] means (Partial_Sums (comP * CSeq)) . $1 = (comP * BSeq) . $1;
A78: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A79: S2[k] ; ::_thesis: S2[k + 1]
A80: BSeq . k c= BSeq . (k + 1) by A76, PROB_2:7;
thus (Partial_Sums (comP * CSeq)) . (k + 1) = ((comP * BSeq) . k) + ((comP * CSeq) . (k + 1)) by A79, SERIES_1:def_1
.= (comP . (BSeq . k)) + ((comP * CSeq) . (k + 1)) by FUNCT_2:15
.= (comP . (BSeq . k)) + (comP . (CSeq . (k + 1))) by FUNCT_2:15
.= comP . ((BSeq . k) \/ (CSeq . (k + 1))) by A52, A76, Th18
.= comP . ((BSeq . k) \/ ((BSeq . (k + 1)) \ (BSeq . k))) by A76, Th16
.= comP . ((BSeq . k) \/ (BSeq . (k + 1))) by XBOOLE_1:39
.= comP . (BSeq . (k + 1)) by A80, XBOOLE_1:12
.= (comP * BSeq) . (k + 1) by FUNCT_2:15 ; ::_thesis: verum
end;
(Partial_Sums (comP * CSeq)) . 0 = (comP * CSeq) . 0 by SERIES_1:def_1
.= comP . (CSeq . 0) by FUNCT_2:15
.= comP . (BSeq . 0) by A76, Th16
.= (comP * BSeq) . 0 by FUNCT_2:15 ;
then A81: S2[ 0 ] ;
thus  for k being Element of NAT holds S2[k] from NAT_1:sch_1(A81, A78); ::_thesis: verum
end;
comP . (Union BSeq) = comP . (Union CSeq) by PROB_3:36
.= Sum (comP * CSeq) by A7
.= lim (Partial_Sums (comP * CSeq)) ;
hence  ( comP * BSeq is convergent & lim (comP * BSeq) = comP . (Union BSeq) ) by A74, A76, A77, FUNCT_2:63; ::_thesis: verum
end;
then reconsider comP = comP as Probability of COM (Sigma,P) by A48, A71, A52, PROB_2:10;
take  comP ; ::_thesis: for B being set st B in Sigma holds
for C being thin of P holds comP . (B \/ C) = P . B
thus  for B being set st B in Sigma holds
for C being thin of P holds comP . (B \/ C) = P . B by A5; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Probability of COM (Sigma,P) st ( for B being set st B in Sigma holds
for C being thin of P holds b1 . (B \/ C) = P . B ) & ( for B being set st B in Sigma holds
for C being thin of P holds b2 . (B \/ C) = P . B ) holds
b1 = b2
proof
let P1, P2 be Probability of COM (Sigma,P); ::_thesis: ( ( for B being set st B in Sigma holds
for C being thin of P holds P1 . (B \/ C) = P . B ) & ( for B being set st B in Sigma holds
for C being thin of P holds P2 . (B \/ C) = P . B ) implies P1 = P2 )
assume that
A82: for B being set st B in Sigma holds
for C being thin of P holds P1 . (B \/ C) = P . B and
A83: for B being set st B in Sigma holds
for C being thin of P holds P2 . (B \/ C) = P . B ; ::_thesis: P1 = P2
 for x being set st x in COM (Sigma,P) holds
P1 . x = P2 . x
proof
let x be set ; ::_thesis: ( x in COM (Sigma,P) implies P1 . x = P2 . x )
assume  x in COM (Sigma,P) ; ::_thesis: P1 . x = P2 . x
then consider B being set  such that
A84: ( B in Sigma & ex C being thin of P st x = B \/ C ) by Def5;
P1 . x = P . B by A82, A84
.= P2 . x by A83, A84 ;
hence  P1 . x = P2 . x ; ::_thesis: verum
end;
hence  P1 = P2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines COM PROB_4:def_8_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for b4 being Probability of COM (Sigma,P) holds
( b4 = COM P iff for B being set st B in Sigma holds
for C being thin of P holds b4 . (B \/ C) = P . B );

theorem :: PROB_4:37
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds COM P = COM (P2M P)
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma holds COM P = COM (P2M P)
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma holds COM P = COM (P2M P)
let P be Probability of Sigma; ::_thesis: COM P = COM (P2M P)
set Y = COM P;
 COM (Sigma,P) = COM (Sigma,(P2M P)) by Th27;
then reconsider Y1 = P2M (COM P) as sigma_Measure of (COM (Sigma,(P2M P))) ;
 for B being set st B in Sigma holds
for C being thin of P2M P holds Y1 . (B \/ C) = (P2M P) . B
proof
let B be set ; ::_thesis: ( B in Sigma implies for C being thin of P2M P holds Y1 . (B \/ C) = (P2M P) . B )
assume A1: B in Sigma ; ::_thesis: for C being thin of P2M P holds Y1 . (B \/ C) = (P2M P) . B
let C be thin of P2M P; ::_thesis: Y1 . (B \/ C) = (P2M P) . B
reconsider C1 = C as thin of P by Th23;
 (COM P) . (B \/ C1) = P . B by A1, Def8;
hence  Y1 . (B \/ C) = (P2M P) . B ; ::_thesis: verum
end;
hence  COM P = COM (P2M P) by MEASURE3:def_5; ::_thesis: verum
end;

theorem :: PROB_4:38
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds COM P is_complete COM (Sigma,P)
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma holds COM P is_complete COM (Sigma,P)
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma holds COM P is_complete COM (Sigma,P)
let P be Probability of Sigma; ::_thesis: COM P is_complete COM (Sigma,P)
 for A being Subset of Omega
for B being set st B in COM (Sigma,P) & A c= B & (COM P) . B = 0 holds
A in COM (Sigma,P)
proof
let A be Subset of Omega; ::_thesis: for B being set st B in COM (Sigma,P) & A c= B & (COM P) . B = 0 holds
A in COM (Sigma,P)
let B be set ; ::_thesis: ( B in COM (Sigma,P) & A c= B & (COM P) . B = 0 implies A in COM (Sigma,P) )
assume A1: B in COM (Sigma,P) ; ::_thesis: ( not A c= B or not (COM P) . B = 0 or A in COM (Sigma,P) )
assume that
A2: A c= B and
A3: (COM P) . B = 0 ; ::_thesis: A in COM (Sigma,P)
 ex B1 being set st
( B1 in Sigma & ex C1 being thin of P st A = B1 \/ C1 )
proof
take  {} ; ::_thesis: ( {} in Sigma & ex C1 being thin of P st A = {} \/ C1 )
consider B2 being set  such that
A4: B2 in Sigma and
A5: ex C2 being thin of P st B = B2 \/ C2 by A1, Def5;
A6: P . B2 = 0 by A3, A4, A5, Def8;
consider C2 being thin of P such that
A7: B = B2 \/ C2 by A5;
set C1 = (A /\ B2) \/ (A /\ C2);
consider D2 being set  such that
A8: D2 in Sigma and
A9: C2 c= D2 and
A10: P . D2 = 0 by Def4;
set O = B2 \/ D2;
 A /\ C2 c= C2 by XBOOLE_1:17;
then A11: ( A /\ B2 c= B2 & A /\ C2 c= D2 ) by A9, XBOOLE_1:1, XBOOLE_1:17;
 ex O being set st
( O in Sigma & (A /\ B2) \/ (A /\ C2) c= O & P . O = 0 )
proof
reconsider B2 = B2, D2 = D2 as Element of Sigma by A4, A8;
take  B2 \/ D2 ; ::_thesis: ( B2 \/ D2 in Sigma & (A /\ B2) \/ (A /\ C2) c= B2 \/ D2 & P . (B2 \/ D2) = 0 )
 P . (B2 \/ D2) <= 0 + 0 by A6, A10, PROB_1:39;
hence  ( B2 \/ D2 in Sigma & (A /\ B2) \/ (A /\ C2) c= B2 \/ D2 & P . (B2 \/ D2) = 0 ) by A11, PROB_1:def_8, XBOOLE_1:13; ::_thesis: verum
end;
then A12: (A /\ B2) \/ (A /\ C2) is thin of P by Def4;
A = A /\ (B2 \/ C2) by A2, A7, XBOOLE_1:28
.= {} \/ ((A /\ B2) \/ (A /\ C2)) by XBOOLE_1:23 ;
hence  ( {} in Sigma & ex C1 being thin of P st A = {} \/ C1 ) by A12, PROB_1:4; ::_thesis: verum
end;
hence  A in COM (Sigma,P) by Def5; ::_thesis: verum
end;
hence  COM P is_complete COM (Sigma,P) by Def3; ::_thesis: verum
end;

theorem Th39: :: PROB_4:39
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Event of Sigma holds P . A = (COM P) . A
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Event of Sigma holds P . A = (COM P) . A
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for A being Event of Sigma holds P . A = (COM P) . A
let P be Probability of Sigma; ::_thesis: for A being Event of Sigma holds P . A = (COM P) . A
reconsider C = {} as thin of P by Th24;
let A be Event of Sigma; ::_thesis: P . A = (COM P) . A
thus P . A = (COM P) . (A \/ C) by Def8
.= (COM P) . A ; ::_thesis: verum
end;

theorem Th40: :: PROB_4:40
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for C being thin of P holds (COM P) . C = 0
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for C being thin of P holds (COM P) . C = 0
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for C being thin of P holds (COM P) . C = 0
let P be Probability of Sigma; ::_thesis: for C being thin of P holds (COM P) . C = 0
let C be thin of P; ::_thesis: (COM P) . C = 0
consider A being set  such that
A1: A in Sigma and
A2: C c= A and
A3: P . A = 0 by Def4;
reconsider A = A as Event of Sigma by A1;
A4: (COM P) . A = 0 by A3, Th39;
 Sigma c= COM (Sigma,P) by Th28;
then reconsider A = A as Event of COM (Sigma,P) by A1;
 (COM P) . C <= (COM P) . A by A2, PROB_1:34;
hence  (COM P) . C = 0 by A4, PROB_1:def_8; ::_thesis: verum
end;

theorem :: PROB_4:41
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM (Sigma,P)
for B being set st B in ProbPart A holds
P . B = (COM P) . A
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM (Sigma,P)
for B being set st B in ProbPart A holds
P . B = (COM P) . A
let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma
for A being Element of COM (Sigma,P)
for B being set st B in ProbPart A holds
P . B = (COM P) . A
let P be Probability of Sigma; ::_thesis: for A being Element of COM (Sigma,P)
for B being set st B in ProbPart A holds
P . B = (COM P) . A
let A be Element of COM (Sigma,P); ::_thesis: for B being set st B in ProbPart A holds
P . B = (COM P) . A
let B be set ; ::_thesis: ( B in ProbPart A implies P . B = (COM P) . A )
assume A1: B in ProbPart A ; ::_thesis: P . B = (COM P) . A
reconsider C = A \ B as thin of P by A1, Def7;
A2: B in Sigma by A1, Def7;
 B c= A by A1, Def7;
then A3: A = B \/ C by XBOOLE_1:45;
 Sigma c= COM (Sigma,P) by Th28;
then reconsider B = B as Event of COM (Sigma,P) by A2;
reconsider A = A as Event of COM (Sigma,P) ;
 B misses C by XBOOLE_1:79;
then A4: (COM P) . A = ((COM P) . B) + ((COM P) . C) by A3, PROB_1:def_8
.= ((COM P) . B) + 0 by Th40
.= (COM P) . B ;
reconsider B = B as Event of Sigma by A1, Def7;
 (COM P) . A = P . B by A4, Th39;
hence  P . B = (COM P) . A ; ::_thesis: verum
end;