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:11;
let A be Element of S; :: thesis: M . A <= R_EAL 1
M . A <= M . X by MEASURE1:62;
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 4;
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:5;
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 4, SEQ_1:3;
hence 0 <= (P1 * ASeq) . n by FUNCT_1:22; :: thesis: verum

end;

then A7: P1 * ASeq is bounded_below 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:14;
A9: M . (F . 0 ) < +infty by A3, XXREAL_0:9;

now

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:22;
F . (n + 1) c= F . n by A6, PROB_2:14;
hence (P1 * ASeq) . (n + 1) <= (P1 * ASeq) . n by A10, MEASURE1:62; :: thesis: verum

end;

then A11: P1 * ASeq is non-increasing by SEQM_3:def 14;
then lim (P1 * ASeq) = lower_bound (P1 * ASeq) by A7, RINFSUP1:25
.= inf (rng (M * F)) by A7, Th12 ;
then lim (P1 * ASeq) = M . (meet (rng F)) by A8, A9, MEASURE3:14
.= 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:61
.= (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 4, MEASURE6:def 1;
hence M is Probability of S by A12, A5, PROB_1:def 13; :: thesis: verum