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 n being Element of NAT holds P . (ASeq . n) = 0 ) iff P . (Union ASeq) = 0 )
let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( ( for n being Element of NAT holds P . (ASeq . n) = 0 ) iff P . (Union ASeq) = 0 )
let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma holds
( ( for n being Element of NAT holds P . (ASeq . n) = 0 ) iff P . (Union ASeq) = 0 )
let P be Probability of Sigma; :: thesis: ( ( for n being Element of NAT holds P . (ASeq . n) = 0 ) iff P . (Union ASeq) = 0 )

hereby :: thesis: ( P . (Union ASeq) = 0 implies for n being Element of NAT holds P . (ASeq . n) = 0 )

assume A1: for n being Element of NAT holds P . (ASeq . n) = 0 ; :: thesis: P . (Union ASeq) = 0
for n being Nat holds (Partial_Sums (P * ASeq)) . n = 0

proof

defpred S₁[ Nat] means (Partial_Sums (P * ASeq)) . $1 = 0 ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
thus (Partial_Sums (P * ASeq)) . (k + 1) = ((Partial_Sums (P * ASeq)) . k) + ((P * ASeq) . (k + 1)) by SERIES_1:def 1
.= 0 + (P . (ASeq . (k + 1))) by A3, FUNCT_2:15
.= 0 by A1 ; :: thesis: verum

end;

(Partial_Sums (P * ASeq)) . 0 = (P * ASeq) . 0 by SERIES_1:def 1
.= P . (ASeq . 0) by FUNCT_2:15
.= 0 by A1 ;
then A4: S₁[ 0 ] ;
thus for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A2); :: thesis: verum

end;

then for n being Nat st 0 <= n holds
(Partial_Sums (P * ASeq)) . n = 0 ;
then A5: ( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = 0 ) by PROB_1:1;

now :: thesis: for n being Nat holds (P * (Partial_Diff_Union ASeq)) . n <= (P * ASeq) . n

let n be Nat; :: thesis: (P * (Partial_Diff_Union ASeq)) . n <= (P * ASeq) . n
(Partial_Diff_Union ASeq) . n c= ASeq . n by PROB_3:33;
hence (P * (Partial_Diff_Union ASeq)) . n <= (P * ASeq) . n by PROB_3:5; :: thesis: verum

end;

then A6: for n being Nat holds (Partial_Sums (P * (Partial_Diff_Union ASeq))) . n <= (Partial_Sums (P * ASeq)) . n by SERIES_1:14;
Partial_Sums (P * (Partial_Diff_Union ASeq)) is convergent by PROB_3:45;
then Sum (P * (Partial_Diff_Union ASeq)) <= 0 by A5, A6, SEQ_2:18;
then P . (Union (Partial_Diff_Union ASeq)) <= 0 by PROB_3:46;
then A7: P . (Union ASeq) <= 0 by PROB_3:36;
Union ASeq is Event of Sigma by PROB_1:26;
hence P . (Union ASeq) = 0 by A7, PROB_1:def 8; :: thesis: verum

end;

assume A8: P . (Union ASeq) = 0 ; :: thesis: for n being Element of NAT holds P . (ASeq . n) = 0

hereby :: thesis: verum

reconsider Y2 = Union ASeq as Event of Sigma by PROB_1:26;
let n be Element of NAT ; :: thesis: P . (ASeq . n) = 0
reconsider Y1 = ASeq . n as Event of Sigma ;
ASeq . n in rng ASeq by SETLIM_1:4;
then ASeq . n c= union (rng ASeq) by ZFMISC_1:74;
then Y1 c= Y2 by CARD_3:def 4;
hence P . (ASeq . n) = 0 by A8, Th6; :: thesis: verum

end;