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:7, NUMBERS:31;
for x being ExtReal st x in rng P1 holds
0. <= x

proof

let x be ExtReal; :: 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 object such that
A2: y in Sigma and
A3: P1 . y = x by A1, FUNCT_1:def 3;
reconsider y1 = y as Event of Sigma by A2;
0 <= P . y1 by PROB_1:def 8;
hence 0. <= x by A3; :: thesis: verum

end;

then A4: rng P1 is nonnegative by SUPINF_2:def 9;
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 disjoint_valued SetSequence of Sigma by Th2;
for n being 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:45;
then P * F2 is summable ;
then ( P . (Union F2) = Sum (P * F2) & Sum (P * F2) = SUM (P1 * F) ) by A5, Th12, PROB_3:46;
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 6, SUPINF_2:def 12; :: thesis: verum