let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma holds P is sigma_Measure of Sigma
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma holds P is sigma_Measure of Sigma
let P be Probability of Sigma; :: thesis: P is sigma_Measure of Sigma
set Z = Sigma;
reconsider P1 = P as Function of Sigma,ExtREAL by FUNCT_2:9, NUMBERS:31;
for x being R_eal st x in rng P1 holds
0. <= x

proof

let x be R_eal; :: thesis: ( x in rng P1 implies 0. <= x )
assume A1: x in rng P1 ; :: thesis: 0. <= x
dom P1 = Sigma by FUNCT_2:def 1;
then consider y being set such that
A2: y in Sigma and
A3: P1 . y = x by A1, FUNCT_1:def 5;
reconsider y1 = y as Event of Sigma by A2;
0 <= P . y1 by PROB_1:def 13;
hence 0. <= x by A3; :: thesis: verum

end;

then A4: rng P1 is nonnegative by SUPINF_2:def 15;
for F being Sep_Sequence of Sigma holds SUM (P1 * F) = P1 . (union (rng F))

proof

let F be Sep_Sequence of Sigma; :: thesis: SUM (P1 * F) = P1 . (union (rng F))
reconsider F2 = F as V215() SetSequence of Sigma by Th2;
for n being Element of NAT holds (P * F2) . n >= 0 by PROB_3:4;
then A5: P * F2 is nonnegative by RINFSUP1:def 3;
Partial_Sums (P * F2) is convergent by PROB_3:50;
then P * F2 is summable by SERIES_1:def 2;
then ( P . (Union F2) = Sum (P * F2) & Sum (P * F2) = SUM (P1 * F) ) by A5, Th13, PROB_3:51;
hence SUM (P1 * F) = P1 . (union (rng F)) by CARD_3:def 4; :: thesis: verum

end;

hence P is sigma_Measure of Sigma by A4, MEASURE1:def 11, SUPINF_2:def 22; :: thesis: verum