let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S st M . X = 1 holds
M is Probability of S
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S st M . X = 1 holds
M is Probability of S
let M be sigma_Measure of S; :: thesis: ( M . X = 1 implies M is Probability of S )
assume A1: M . X = 1 ; :: thesis: M is Probability of S
A2: for A being Element of S holds M . A <= 1

proof

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

end;

A3: for x being object st x in S holds
M . x in REAL

proof

let x be object ; :: 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: ( 1 in REAL & 0 in REAL ) by XREAL_0:def 1;
( 0. <= M . x & M . x <= 1 ) by A2, MEASURE1:def 2;
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:3;
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 Nat holds 0 <= (P1 * ASeq) . n

proof

let n be Nat; :: thesis: 0 <= (P1 * ASeq) . n
A7: n in NAT by ORDINAL1:def 12;
reconsider A = ASeq . n as Event of S ;
( 0 <= P1 . A & dom (P1 * ASeq) = NAT ) by MEASURE1:def 2, SEQ_1:1;
hence 0 <= (P1 * ASeq) . n by FUNCT_1:12, A7; :: thesis: verum

end;

then A8: P1 * ASeq is bounded_below by RINFSUP1:10;
reconsider F = ASeq as sequence of S by Th2;
A9: for n being Nat holds F . (n + 1) c= F . n by A6, PROB_2:6;
A10: M . (F . 0) < +infty by A3, XXREAL_0:9;

now :: thesis: for n being Nat holds (P1 * ASeq) . (n + 1) <= (P1 * ASeq) . n

let n be Nat; :: thesis: (P1 * ASeq) . (n + 1) <= (P1 * ASeq) . n
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
dom (M * F) = NAT by FUNCT_2:def 1;
then A11: ( (M * F) . nn = M . (F . nn) & (M * F) . (nn + 1) = M . (F . (nn + 1)) ) by FUNCT_1:12;
F . (n + 1) c= F . n by A6, PROB_2:6;
hence (P1 * ASeq) . (n + 1) <= (P1 * ASeq) . n by A11, MEASURE1:31; :: thesis: verum

end;

then A12: P1 * ASeq is non-increasing by SEQM_3:def 9;
then lim (P1 * ASeq) = lower_bound (P1 * ASeq) by A8, RINFSUP1:25
.= inf (rng (M * F)) by A8, Th11 ;
then lim (P1 * ASeq) = M . (meet (rng F)) by A9, A10, MEASURE3:12
.= P1 . (Intersection ASeq) by SETLIM_1:8 ;
hence ( P1 * ASeq is convergent & lim (P1 * ASeq) = P1 . (Intersection ASeq) ) by A8, A12; :: thesis: verum

end;

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:30
.= (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 2;
hence M is Probability of S by A13, A5, PROB_1:def 8; :: thesis: verum