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 A is_all_independent_wrt Prob holds
( ( Prob . () = 0 or Prob . () = 1 ) & ( Prob . () = 0 or Prob . () = 1 ) )

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

let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma st A is_all_independent_wrt Prob holds
( ( Prob . () = 0 or Prob . () = 1 ) & ( Prob . () = 0 or Prob . () = 1 ) )

let A be SetSequence of Sigma; :: thesis: ( A is_all_independent_wrt Prob implies ( ( Prob . () = 0 or Prob . () = 1 ) & ( Prob . () = 0 or Prob . () = 1 ) ) )
assume A1: A is_all_independent_wrt Prob ; :: thesis: ( ( Prob . () = 0 or Prob . () = 1 ) & ( Prob . () = 0 or Prob . () = 1 ) )
per cases ( Partial_Sums (Prob * A) is convergent or not Partial_Sums (Prob * A) is convergent ) ;
suppose Partial_Sums (Prob * A) is convergent ; :: thesis: ( ( Prob . () = 0 or Prob . () = 1 ) & ( Prob . () = 0 or Prob . () = 1 ) )
hence ( ( Prob . () = 0 or Prob . () = 1 ) & ( Prob . () = 0 or Prob . () = 1 ) ) by Th16; :: thesis: verum
end;
suppose not Partial_Sums (Prob * A) is convergent ; :: thesis: ( ( Prob . () = 0 or Prob . () = 1 ) & ( Prob . () = 0 or Prob . () = 1 ) )
hence ( ( Prob . () = 0 or Prob . () = 1 ) & ( Prob . () = 0 or Prob . () = 1 ) ) by ; :: thesis: verum
end;
end;