deffunc H₁( Element of bool E) -> Element of REAL = In ((prob $1),REAL);
consider EP being Function of (Trivial-SigmaField E),REAL such that
A1: for x being Element of Trivial-SigmaField E holds EP . x = H₁(x) from FUNCT_2:sch 4();
A2: for A, B being Event of Trivial-SigmaField E st A misses B holds
EP . (A \/ B) = (EP . A) + (EP . B)

proof

let A, B be Event of Trivial-SigmaField E; :: thesis: ( A misses B implies EP . (A \/ B) = (EP . A) + (EP . B) )
assume A3: A misses B ; :: thesis: EP . (A \/ B) = (EP . A) + (EP . B)
A4: EP . B = H₁(B) by A1
.= prob B ;
thus EP . (A \/ B) = H₁(A \/ B) by A1
.= prob (A \/ B)
.= ((prob A) + (prob B)) - (prob (A /\ B)) by RPR_1:20
.= ((prob A) + (prob B)) - 0 by A3, RPR_1:16
.= H₁(A) + (prob B)
.= (EP . A) + (prob B) by A1
.= (EP . A) + (EP . B) by A4
.= (EP . A) + (EP . B) ; :: thesis: verum

end;

A5: for A being Event of Trivial-SigmaField E holds 0 <= EP . A

proof

let A be Event of Trivial-SigmaField E; :: thesis: 0 <= EP . A
EP . A = H₁(A) by A1
.= prob A ;
hence 0 <= EP . A ; :: thesis: verum

end;

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

proof

let ASeq be SetSequence of Trivial-SigmaField E; :: 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
A7: for m being Nat st N <= m holds
Intersection ASeq = ASeq . m by Th15;

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 A8: 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 A7, A8 ;
:: thesis: verum

end;

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

end;

EP . E = H₁( [#] E) by A1
.= prob ([#] E)
.= 1 by RPR_1:15 ;
then reconsider EP = EP as Probability of Trivial-SigmaField E by A5, A2, A6, PROB_1:def 8;
take EP ; :: thesis: for A being Event of E holds EP . A = prob A
let A be Event of E; :: thesis: EP . A = prob A
thus EP . A = H₁(A) by A1
.= prob A ; :: thesis: verum