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:52;
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:5;
consider BSeq being SetSequence of such that
A6: for n being Element of NAT holds BSeq . n in ProbPart (F . n) by Th32;
consider CSeq being SetSequence of Omega such that
A7: for n being Element of NAT holds CSeq . n = (F . n) \ (BSeq . n) by Th33;
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 such that
A9: for n being Element of NAT holds
( CSeq . n c= DSeq . n & P . (DSeq . n) = 0 ) by Th34;
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 5;
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 5; :: 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:46;
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 5;
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 5;
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 5; :: 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 5;
hence P . A = 0 by A9; :: thesis: verum

end;

then A29: P . (union (rng DSeq)) = 0 by Th9;
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 5;
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 5;
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:46;
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:12; :: thesis: verum

end;

hence A ` in D by A1; :: thesis: verum

end;

hence D is SigmaField of Omega by A2, Th5; :: thesis: verum