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 Element of NAT holds (Partial_Sums (P * ASeq)) . n = 0

proof

defpred S₁[ Element of NAT ] means (Partial_Sums (P * ASeq)) . $1 = 0 ;
A2: S₁[ 0 ]

proof

thus (Partial_Sums (P * ASeq)) . 0 = (P * ASeq) . 0 by SERIES_1:def 1
.= P . (ASeq . 0 ) by FUNCT_2:21
.= 0 by A1 ; :: thesis: verum

end;

A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: 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 A4, FUNCT_2:21
.= 0 by A1 ; :: thesis: verum

end;

thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A3); :: thesis: verum

end;

then for n being Element of 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:3;
A6: P . (Union ASeq) <= 0

proof

@Partial_Diff_Union ASeq is disjoint_valued by PROB_3:41;
then A7: Partial_Sums (P * (@Partial_Diff_Union ASeq)) is convergent by PROB_3:50;

now

let n be Element of NAT ; :: thesis: (P * (@Partial_Diff_Union ASeq)) . n <= (P * ASeq) . n
(@Partial_Diff_Union ASeq) . n c= ASeq . n by PROB_3:37;
hence (P * (@Partial_Diff_Union ASeq)) . n <= (P * ASeq) . n by PROB_3:5; :: thesis: verum

end;

then for n being Element of NAT holds (Partial_Sums (P * (@Partial_Diff_Union ASeq))) . n <= (Partial_Sums (P * ASeq)) . n by SERIES_1:17;
then Sum (P * (@Partial_Diff_Union ASeq)) <= 0 by A5, A7, SEQ_2:32;
then P . (Union (@Partial_Diff_Union ASeq)) <= 0 by PROB_3:41, PROB_3:51;
hence P . (Union ASeq) <= 0 by PROB_3:40; :: thesis: verum

end;

P . (Union ASeq) >= 0

proof

Union ASeq is Event of Sigma by PROB_1:58;
hence P . (Union ASeq) >= 0 by PROB_1:def 13; :: thesis: verum

end;

hence P . (Union ASeq) = 0 by A6; :: thesis: verum

end;

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

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: P . (ASeq . n) = 0
reconsider Y1 = ASeq . n as Event of Sigma ;
reconsider Y2 = Union ASeq as Event of Sigma by PROB_1:58;
Y1 c= Y2

proof

ASeq . n in rng ASeq by SETLIM_1:4;
then ASeq . n c= union (rng ASeq) by ZFMISC_1:92;
hence Y1 c= Y2 by CARD_3:def 4; :: thesis: verum

end;

hence P . (ASeq . n) = 0 by A8, Th7; :: thesis: verum

end;