let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma st not Partial_Sums (Prob * A) is convergent & A is_all_independent_wrt Prob holds
( Prob . () = 0 & Prob . () = 1 )

let Sigma be SigmaField of Omega; :: thesis: for Prob being Probability of Sigma
for A being SetSequence of Sigma st not Partial_Sums (Prob * A) is convergent & A is_all_independent_wrt Prob holds
( Prob . () = 0 & Prob . () = 1 )

let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma st not Partial_Sums (Prob * A) is convergent & A is_all_independent_wrt Prob holds
( Prob . () = 0 & Prob . () = 1 )

let A be SetSequence of Sigma; :: thesis: ( not Partial_Sums (Prob * A) is convergent & A is_all_independent_wrt Prob implies ( Prob . () = 0 & Prob . () = 1 ) )
assume A1: not Partial_Sums (Prob * A) is convergent ; :: thesis: ( not A is_all_independent_wrt Prob or ( Prob . () = 0 & Prob . () = 1 ) )
assume A2: A is_all_independent_wrt Prob ; :: thesis: ( Prob . () = 0 & Prob . () = 1 )
A3: for n being Nat holds (Prob * A) . n >= 0
proof
let n be Nat; :: thesis: (Prob * A) . n >= 0
A4: n in NAT by ORDINAL1:def 12;
dom (Prob * A) = NAT by FUNCT_2:def 1;
then (Prob * A) . n = Prob . (A . n) by ;
hence (Prob * A) . n >= 0 by PROB_1:def 8; :: thesis: verum
end;
A5: ( ( not Prob * A is summable implies not Partial_Sums (Prob * A) is bounded_above ) & not Prob * A is summable ) by ;
Partial_Sums (Prob * A) is divergent_to+infty by ;
hence ( Prob . () = 0 & Prob . () = 1 ) by ; :: thesis: verum