let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( ( for A being set st A in rng ASeq holds
P . A = 0 ) iff P . (union (rng ASeq)) = 0 )
let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( ( for A being set st A in rng ASeq holds
P . A = 0 ) iff P . (union (rng ASeq)) = 0 )
let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma holds
( ( for A being set st A in rng ASeq holds
P . A = 0 ) iff P . (union (rng ASeq)) = 0 )
let P be Probability of Sigma; :: thesis: ( ( for A being set st A in rng ASeq holds
P . A = 0 ) iff P . (union (rng ASeq)) = 0 )

hereby :: thesis: ( P . (union (rng ASeq)) = 0 implies for A being set st A in rng ASeq holds
P . A = 0 )

assume A1: for A being set st A in rng ASeq holds
P . A = 0 ; :: thesis: P . (union (rng ASeq)) = 0
for n being Element of NAT holds P . (ASeq . n) = 0 by SETLIM_1:4, A1;
then P . (Union ASeq) = 0 by Th7;
hence P . (union (rng ASeq)) = 0 by CARD_3:def 4; :: thesis: verum

end;

assume P . (union (rng ASeq)) = 0 ; :: thesis: for A being set st A in rng ASeq holds
P . A = 0
then A2: P . (Union ASeq) = 0 by CARD_3:def 4;

hereby :: thesis: verum

let A be set ; :: thesis: ( A in rng ASeq implies P . A = 0 )
assume A in rng ASeq ; :: thesis: P . A = 0
then consider n1 being Nat such that
A3: A = ASeq . n1 by SETLIM_1:4;
n1 in NAT by ORDINAL1:def 12;
hence P . A = 0 by A2, Th7, A3; :: thesis: verum

end;