let S be non empty finite set ; :: thesis: for D being EqSampleSpaces of S ex EP being Probability of Trivial-SigmaField S st
for x being set st x in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & EP . x = Prob (ch,D) )
let D be EqSampleSpaces of S; :: thesis: ex EP being Probability of Trivial-SigmaField S st
for x being set st x in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & EP . x = Prob (ch,D) )
defpred S₁[ object , object ] means ex D1 being set ex ch being Function of S,BOOLEAN st
( D1 = $1 & ch = chi (D1,S) & $2 = Prob (ch,D) );

A1: now :: thesis: for x being object st x in Trivial-SigmaField S holds
ex y being object st
( y in REAL & S₁[x,y] )

let x be object ; :: thesis: ( x in Trivial-SigmaField S implies ex y being object st
( y in REAL & S₁[x,y] ) )
assume x in Trivial-SigmaField S ; :: thesis: ex y being object st
( y in REAL & S₁[x,y] )
reconsider xx = x as set by TARSKI:1;
reconsider ch = chi (xx,S) as Function of S,BOOLEAN by MARGREL1:def 11;
Prob (ch,D) in REAL by XREAL_0:def 1;
hence ex y being object st
( y in REAL & S₁[x,y] ) ; :: thesis: verum

end;

consider EP being Function of (Trivial-SigmaField S),REAL such that
A2: for x being object st x in Trivial-SigmaField S holds
S₁[x,EP . x] from FUNCT_2:sch 1(A1);
A3: for A, B being Event of Trivial-SigmaField S st A misses B holds
EP . (A \/ B) = (EP . A) + (EP . B)

proof

let A, B be Event of Trivial-SigmaField S; :: thesis: ( A misses B implies EP . (A \/ B) = (EP . A) + (EP . B) )
assume A4: A misses B ; :: thesis: EP . (A \/ B) = (EP . A) + (EP . B)
S₁[A,EP . A] by A2;
then consider chA being Function of S,BOOLEAN such that
A5: ( chA = chi (A,S) & EP . A = Prob (chA,D) ) ;
S₁[B,EP . B] by A2;
then consider chB being Function of S,BOOLEAN such that
A6: ( chB = chi (B,S) & EP . B = Prob (chB,D) ) ;
S₁[A \/ B,EP . (A \/ B)] by A2;
then consider chAB being Function of S,BOOLEAN such that
A7: ( chAB = chi ((A \/ B),S) & EP . (A \/ B) = Prob (chAB,D) ) ;
A8: chAB = chA 'or' chB by A5, A6, A7, Th31;
thus EP . (A \/ B) = ((Prob (chA,D)) + (Prob (chB,D))) - (Prob ((chA '&' chB),D)) by Th27, A7, A8
.= ((Prob (chA,D)) + (Prob (chB,D))) - 0 by A5, A6, A4, Th32
.= (EP . A) + (EP . B) by A6, A5 ; :: thesis: verum

end;

A9: for A being Event of Trivial-SigmaField S holds 0 <= EP . A

proof

let A be Event of Trivial-SigmaField S; :: thesis: 0 <= EP . A
S₁[A,EP . A] by A2;
then consider chA being Function of S,BOOLEAN such that
A10: ( chA = chi (A,S) & EP . A = Prob (chA,D) ) ;
thus 0 <= EP . A by A10, Th30; :: thesis: verum

end;

A11: for ASeq being SetSequence of Trivial-SigmaField S st ASeq is non-ascending holds
( EP * ASeq is convergent & lim (EP * ASeq) = EP . (Intersection ASeq) )

proof

let ASeq be SetSequence of Trivial-SigmaField S; :: thesis: ( ASeq is non-ascending implies ( EP * ASeq is convergent & lim (EP * ASeq) = EP . (Intersection ASeq) ) )
assume ASeq is non-ascending ; :: thesis: ( EP * ASeq is convergent & lim (EP * ASeq) = EP . (Intersection ASeq) )
then consider N being Nat such that
A12: for m being Nat st N <= m holds
Intersection ASeq = ASeq . m by RANDOM_1:15;

now :: thesis: for m being Nat st N <= m holds
(EP * ASeq) . m = EP . (Intersection ASeq)

let m be Nat; :: thesis: ( N <= m implies (EP * ASeq) . m = EP . (Intersection ASeq) )
assume A13: N <= m ; :: thesis: (EP * ASeq) . m = EP . (Intersection ASeq)
m in NAT by ORDINAL1:def 12;
then m in dom ASeq by FUNCT_2:def 1;
hence (EP * ASeq) . m = EP . (ASeq . m) by FUNCT_1:13
.= EP . (Intersection ASeq) by A12, A13 ;
:: thesis: verum

end;

hence ( EP * ASeq is convergent & lim (EP * ASeq) = EP . (Intersection ASeq) ) by PROB_1:1; :: thesis: verum

end;

S₁[ [#] S,EP . ([#] S)] by A2;
then consider chS being Function of S,BOOLEAN such that
A14: ( chS = chi (S,S) & EP . S = Prob (chS,D) ) ;
reconsider EP = EP as Probability of Trivial-SigmaField S by A9, A3, PROB_1:def 8, Th29, A11, A14;
take EP ; :: thesis: for x being set st x in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & EP . x = Prob (ch,D) )
let x be set ; :: thesis: ( x in Trivial-SigmaField S implies ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & EP . x = Prob (ch,D) ) )
assume x in Trivial-SigmaField S ; :: thesis: ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & EP . x = Prob (ch,D) )
then S₁[x,EP . x] by A2;
hence ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & EP . x = Prob (ch,D) ) ; :: thesis: verum