deffunc H₁( Element of bool E) -> Element of REAL = prob $1;
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)
thus EP . (A \/ B) = prob (A \/ B) by A1
.= ((prob A) + (prob B)) - (prob (A /\ B)) by RPR_1:20
.= ((prob A) + (prob B)) - 0 by A3, RPR_1:16
.= (EP . A) + (prob B) by A1
.= (EP . A) + (EP . B) by A1 ; :: thesis: verum

end;

A4: 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 = prob A by A1;
hence 0 <= EP . A ; :: thesis: verum

end;

take EP ; :: thesis: ( EP is Probability of Trivial-SigmaField E & ( for A being Event of E holds EP . A = prob A ) )
A5: 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 Element of NAT such that
A6: for m being Element of NAT st N <= m holds
Intersection ASeq = ASeq . m by Th15;

now

let m be Element of NAT ; :: thesis: ( N <= m implies (EP * ASeq) . m = EP . (Intersection ASeq) )
assume A7: N <= m ; :: thesis: (EP * ASeq) . m = EP . (Intersection ASeq)
m in NAT ;
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 A6, A7 ;
:: thesis: verum

end;

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

end;

EP . E = prob ([#] E) by A1
.= 1 by RPR_1:15 ;
hence ( EP is Probability of Trivial-SigmaField E & ( for A being Event of E holds EP . A = prob A ) ) by A1, A4, A2, A5, PROB_1:def 8; :: thesis: verum