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

let A be Element of S; :: thesis: M . A <= R_EAL 1
reconsider X = X as Element of S by PROB_1:11;
M . A <= M . X by MEASURE1:62;
hence M . A <= R_EAL 1 by A1; :: thesis: verum

end;

A3: dom M = S by FUNCT_2:def 1;
A5: 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 A6: x in S ; :: thesis: M . x in REAL
reconsider x = x as Element of S by A6;
A7: ( R_EAL 1 is Real & 0 is Real ) by MEASURE6:def 1;
A8: 0. <= M . x by MEASURE1:def 4;
M . x <= R_EAL 1 by A2;
then M . x is Real by A7, A8, XXREAL_0:45;
hence M . x in REAL ; :: thesis: verum

end;

then reconsider P1 = M as Function of S, REAL by A3, FUNCT_2:5;
reconsider P1 = P1 as Function of S, REAL ;
A9: for A being Event of S holds 0 <= P1 . A by MEASURE1:def 4;
A12: P1 . X = 1 by A1, MEASURE6:def 1;
A13: 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 A14: 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 A14, MEASURE1:61
.= (P1 . A) + (P1 . B) by SUPINF_2:1 ;
hence P1 . (A \/ B) = (P1 . A) + (P1 . B) ; :: thesis: verum

end;

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 A15: ASeq is non-ascending ; :: thesis: ( P1 * ASeq is convergent & lim (P1 * ASeq) = P1 . (Intersection ASeq) )
reconsider F = ASeq as Function of NAT ,S by Th2;
A16: for n being Element of NAT holds F . (n + 1) c= F . n by A15, PROB_2:14;
A17: M . (F . 0 ) < +infty by A5, XXREAL_0:9;
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 ;
A18: 0 <= P1 . A by A9;
dom (P1 * ASeq) = NAT by SEQ_1:3;
hence 0 <= (P1 * ASeq) . n by A18, FUNCT_1:22; :: thesis: verum

end;

then A19: P1 * ASeq is bounded_below by RINFSUP1:10;
A20: P1 * ASeq is non-increasing

proof

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 A21: ( (M * F) . n = M . (F . n) & (M * F) . (n + 1) = M . (F . (n + 1)) ) by FUNCT_1:22;
then A22: ( (M * F) . (n + 1) is Real & (M * F) . n is Real ) by A5;
F . (n + 1) c= F . n by A15, PROB_2:14;
then consider p, q being Real such that
A23: ( p = (M * F) . (n + 1) & q = (M * F) . n & p <= q ) by A21, A22, MEASURE1:62;
thus (P1 * ASeq) . (n + 1) <= (P1 * ASeq) . n by A23; :: thesis: verum

end;

hence P1 * ASeq is non-increasing by SEQM_3:def 14; :: thesis: verum

end;

lim (P1 * ASeq) = inf (rng (M * F))

proof

thus lim (P1 * ASeq) = inf (P1 * ASeq) by A19, A20, RINFSUP1:25
.= inf (rng (M * F)) by A19, Th12 ; :: thesis: verum

end;

then lim (P1 * ASeq) = M . (meet (rng F)) by A16, A17, MEASURE3:14
.= P1 . (Intersection ASeq) by SETLIM_1:8 ;
hence ( P1 * ASeq is convergent & lim (P1 * ASeq) = P1 . (Intersection ASeq) ) by A19, A20; :: thesis: verum

end;

hence M is Probability of S by A9, A12, A13, PROB_1:def 13; :: thesis: verum