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 holds
( ( Partial_Sums (Prob * A) is convergent implies ( Prob . () = 0 & Prob . () = 1 ) ) & ( A is_all_independent_wrt Prob & Partial_Sums (Prob * A) is divergent_to+infty implies ( Prob . () = 0 & Prob . () = 1 ) ) )

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

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

let A be SetSequence of Sigma; :: thesis: ( ( Partial_Sums (Prob * A) is convergent implies ( Prob . () = 0 & Prob . () = 1 ) ) & ( A is_all_independent_wrt Prob & Partial_Sums (Prob * A) is divergent_to+infty implies ( Prob . () = 0 & Prob . () = 1 ) ) )
A1: ( Partial_Sums (Prob * A) is convergent implies Prob . () = 1 )
proof
assume A2: Partial_Sums (Prob * A) is convergent ; :: thesis: Prob . () = 1
A3: Prob . () = Prob . () by Th15;
for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds
( Prob . () = 1 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )
proof
let A be SetSequence of Sigma; :: thesis: ( Partial_Sums (Prob * A) is convergent implies ( Prob . () = 1 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent ) )
assume A4: Partial_Sums (Prob * A) is convergent ; :: thesis: ( Prob . () = 1 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )
( (Prob . ()) + (Prob . ()) = 0 + (Prob . ()) & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent ) by ;
hence ( Prob . () = 1 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent ) by Th15; :: thesis: verum
end;
hence Prob . () = 1 by A2, A3; :: thesis: verum
end;
A5: for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds
Prob . () = 0
proof
let A be SetSequence of Sigma; :: thesis: ( Partial_Sums (Prob * A) is convergent implies Prob . () = 0 )
assume A6: Partial_Sums (Prob * A) is convergent ; :: thesis: Prob . () = 0
Prob . () = Prob . () by Th15;
hence Prob . () = 0 by ; :: thesis: verum
end;
for B being SetSequence of Sigma st B is_all_independent_wrt Prob & Partial_Sums (Prob * B) is divergent_to+infty holds
( Prob . () = 0 & Prob . () = 1 )
proof
let B be SetSequence of Sigma; :: thesis: ( B is_all_independent_wrt Prob & Partial_Sums (Prob * B) is divergent_to+infty implies ( Prob . () = 0 & Prob . () = 1 ) )
assume that
A7: B is_all_independent_wrt Prob and
A8: Partial_Sums (Prob * B) is divergent_to+infty ; :: thesis: ( Prob . () = 0 & Prob . () = 1 )
A9: Prob . () = Prob . () by Th15;
A10: Prob . () = Prob . () by Th15;
for B being SetSequence of Sigma st B is_all_independent_wrt Prob & Partial_Sums (Prob * B) is divergent_to+infty holds
( Prob . () = 0 & Prob . () = 1 )
proof
let B be SetSequence of Sigma; :: thesis: ( B is_all_independent_wrt Prob & Partial_Sums (Prob * B) is divergent_to+infty implies ( Prob . () = 0 & Prob . () = 1 ) )
assume that
A11: B is_all_independent_wrt Prob and
A12: Partial_Sums (Prob * B) is divergent_to+infty ; :: thesis: ( Prob . () = 0 & Prob . () = 1 )
A13: for Q being SetSequence of Sigma holds Intersect_Shift_Seq Q is non-descending A14: Intersect_Shift_Seq () is non-descending by A13;
reconsider CB = Complement B as SetSequence of Sigma ;
A15: Prob . (@lim_inf CB) = lim (Prob * ) by ;
A16: for n being Nat holds (Prob * ) . n = 0
proof
let n be Nat; :: thesis: (Prob * ) . n = 0
A17: n in NAT by ORDINAL1:def 12;
dom (Prob * ) = NAT by FUNCT_2:def 1;
then A18: (Prob * ) . n = Prob . ( . n) by ;
(Intersect_Shift_Seq ()) . n = Intersection (() ^\ n) by Def9;
then A19: (Prob * ) . n = Prob . (Intersection (Partial_Intersection (() ^\ n))) by ;
Partial_Intersection (() ^\ n) is non-ascending by PROB_3:27;
then A20: (Prob * ) . n = lim (Prob * (Partial_Intersection (() ^\ n))) by ;
A21: for k being Nat holds (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k <= ((1 + (Partial_Sums (Prob * (B ^\ n)))) ") . k
proof
let k be Nat; :: thesis: (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k <= ((1 + (Partial_Sums (Prob * (B ^\ n)))) ") . k
A22: for k being Nat holds B ^\ k is_all_independent_wrt Prob
proof
let k be Nat; :: thesis: B ^\ k is_all_independent_wrt Prob
for C being SetSequence of Sigma st ex e being sequence of NAT st
( e is one-to-one & ( for n being Nat holds (B ^\ k) . (e . n) = C . n ) ) holds
for n being Nat holds (Partial_Product (Prob * C)) . n = Prob . ()
proof
let C be SetSequence of Sigma; :: thesis: ( ex e being sequence of NAT st
( e is one-to-one & ( for n being Nat holds (B ^\ k) . (e . n) = C . n ) ) implies for n being Nat holds (Partial_Product (Prob * C)) . n = Prob . () )

given e being sequence of NAT such that A23: e is one-to-one and
A24: for n being Nat holds (B ^\ k) . (e . n) = C . n ; :: thesis: for n being Nat holds (Partial_Product (Prob * C)) . n = Prob . ()
A25: B ^\ k = B *
proof
for n being object st n in NAT holds
(B ^\ k) . n = (B * ) . n
proof
let n be object ; :: thesis: ( n in NAT implies (B ^\ k) . n = (B * ) . n )
assume n in NAT ; :: thesis: (B ^\ k) . n = (B * ) . n
then reconsider n = n as Element of NAT ;
dom (B * ) = NAT by FUNCT_2:def 1;
then A26: (B * ) . n = B . ( . n) by FUNCT_1:12;
(Special_Function2 k) . n = n + k by Def3;
hence (B ^\ k) . n = (B * ) . n by ; :: thesis: verum
end;
hence B ^\ k = B * ; :: thesis: verum
end;
A27: for n being Nat holds (B * ) . (e . n) = B . (( * e) . n)
proof
let n be Nat; :: thesis: (B * ) . (e . n) = B . (( * e) . n)
reconsider n = n as Element of NAT by ORDINAL1:def 12;
( dom (B * ) = NAT & dom ( * e) = NAT ) by FUNCT_2:def 1;
then ( (B * ) . (e . n) = B . ( . (e . n)) & ( * e) . n = . (e . n) ) by FUNCT_1:12;
hence (B * ) . (e . n) = B . (( * e) . n) ; :: thesis: verum
end;
A28: for n being Nat holds B . (( * e) . n) = C . n
proof
let n be Nat; :: thesis: B . (( * e) . n) = C . n
(B * ) . (e . n) = C . n by ;
hence B . (( * e) . n) = C . n by A27; :: thesis: verum
end;
(Special_Function2 k) * e is one-to-one by ;
hence for n being Nat holds (Partial_Product (Prob * C)) . n = Prob . () by ; :: thesis: verum
end;
hence B ^\ k is_all_independent_wrt Prob by Def6; :: thesis: verum
end;
A29: for A being SetSequence of Sigma
for n being Nat holds (Partial_Product (Prob * ())) . n <= ((1 + (Partial_Sums (Prob * A))) . n) "
proof
let A be SetSequence of Sigma; :: thesis: for n being Nat holds (Partial_Product (Prob * ())) . n <= ((1 + (Partial_Sums (Prob * A))) . n) "
let n be Nat; :: thesis: (Partial_Product (Prob * ())) . n <= ((1 + (Partial_Sums (Prob * A))) . n) "
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A30: (Partial_Product (Prob * ())) . n <= 1 / (1 + ((Partial_Sums (Prob * A)) . n))
proof
(Partial_Product (Prob * ())) . n <= (Partial_Product (JSum (Prob * A))) . n by Th4;
then A31: (Partial_Product (Prob * ())) . n <= exp_R . (- ((Partial_Sums (Prob * A)) . n)) by Th3;
exp_R . (- ((Partial_Sums (Prob * A)) . n)) <= 1 / (1 + ((Partial_Sums (Prob * A)) . n))
proof
A32: for n being Nat holds (Prob * A) . n >= 0
proof
let n be Nat; :: thesis: (Prob * A) . n >= 0
reconsider n = n as Element of NAT by ORDINAL1:def 12;
dom (Prob * A) = NAT by FUNCT_2:def 1;
then (Prob * A) . n = Prob . (A . n) by FUNCT_1:12;
hence (Prob * A) . n >= 0 by PROB_1:def 8; :: thesis: verum
end;
A33: for n being Nat holds (Partial_Sums (Prob * A)) . n >= 0
proof
let n be Nat; :: thesis: (Partial_Sums (Prob * A)) . n >= 0
defpred S1[ Nat] means (Partial_Sums (Prob * A)) . \$1 >= 0 ;
(Partial_Sums (Prob * A)) . 0 = (Prob * A) . 0 by SERIES_1:def 1;
then A34: S1[ 0 ] by A32;
A35: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A36: S1[k] ; :: thesis: S1[k + 1]
A37: (Prob * A) . (k + 1) >= 0 by A32;
(Partial_Sums (Prob * A)) . (k + 1) = ((Partial_Sums (Prob * A)) . k) + ((Prob * A) . (k + 1)) by SERIES_1:def 1;
hence S1[k + 1] by ; :: thesis: verum
end;
for k being Nat holds S1[k] from hence (Partial_Sums (Prob * A)) . n >= 0 ; :: thesis: verum
end;
for x being Element of REAL st x >= 0 holds
exp_R . (- x) <= 1 / (1 + x)
proof
let x be Element of REAL ; :: thesis: ( x >= 0 implies exp_R . (- x) <= 1 / (1 + x) )
assume A38: x >= 0 ; :: thesis: exp_R . (- x) <= 1 / (1 + x)
per cases ( x > 0 or x <= 0 ) ;
suppose A39: x > 0 ; :: thesis: exp_R . (- x) <= 1 / (1 + x)
A40: exp_R . (- x) >= 0 by SIN_COS:54;
set z = - x;
A41: (exp_R x) * (exp_R (- x)) = exp_R (x + (- x)) by SIN_COS:50;
(exp_R . (- x)) * (1 + x) <= 1 by ;
hence exp_R . (- x) <= 1 / (1 + x) by ; :: thesis: verum
end;
suppose x <= 0 ; :: thesis: exp_R . (- x) <= 1 / (1 + x)
then x = 0 by A38;
hence exp_R . (- x) <= 1 / (1 + x) by SIN_COS:51; :: thesis: verum
end;
end;
end;
hence exp_R . (- ((Partial_Sums (Prob * A)) . n)) <= 1 / (1 + ((Partial_Sums (Prob * A)) . n)) by A33; :: thesis: verum
end;
hence (Partial_Product (Prob * ())) . n <= 1 / (1 + ((Partial_Sums (Prob * A)) . n)) by ; :: thesis: verum
end;
for A being SetSequence of Sigma
for n being Nat holds 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = ((1 + (Partial_Sums (Prob * A))) . n) "
proof
let A be SetSequence of Sigma; :: thesis: for n being Nat holds 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = ((1 + (Partial_Sums (Prob * A))) . n) "
let n be Nat; :: thesis: 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = ((1 + (Partial_Sums (Prob * A))) . n) "
n in NAT by ORDINAL1:def 12;
then 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = 1 / ((1 + (Partial_Sums (Prob * A))) . n) by VALUED_1:2;
then 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = 1 * (((1 + (Partial_Sums (Prob * A))) . n) ") by XCMPLX_0:def 9;
hence 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = ((1 + (Partial_Sums (Prob * A))) . n) " ; :: thesis: verum
end;
hence (Partial_Product (Prob * ())) . n <= ((1 + (Partial_Sums (Prob * A))) . n) " by A30; :: thesis: verum
end;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
dom (Prob * (Partial_Intersection (Complement (B ^\ n)))) = NAT by FUNCT_2:def 1;
then (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k = Prob . ((Partial_Intersection (Complement (B ^\ n))) . k) by FUNCT_1:12;
then (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k = (Partial_Product (Prob * (Complement (B ^\ n)))) . k by ;
then (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k <= ((1 + (Partial_Sums (Prob * (B ^\ n)))) . k) " by A29;
hence (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k <= ((1 + (Partial_Sums (Prob * (B ^\ n)))) ") . k by VALUED_1:10; :: thesis: verum
end;
A42: Partial_Sums (Prob * (B ^\ n)) is divergent_to+infty
proof
per cases ( n = 0 or n <> 0 ) ;
suppose n <> 0 ; :: thesis: Partial_Sums (Prob * (B ^\ n)) is divergent_to+infty
then A43: n - 1 is Nat by NAT_1:20;
reconsider y = n - 1 as Element of NAT by ;
set B2 = NAT --> (- ((Partial_Sums (Prob * B)) . y));
A44: (Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y))) is divergent_to+infty by ;
for r being Real ex q being Nat st
for m being Nat st q <= m holds
r < (Partial_Sums (Prob * (B ^\ n))) . m
proof
let r be Real; :: thesis: ex q being Nat st
for m being Nat st q <= m holds
r < (Partial_Sums (Prob * (B ^\ n))) . m

for r being Real ex q being Nat st
for m being Nat st q <= m holds
r < (Partial_Sums (Prob * (B ^\ n))) . m
proof
let r be Real; :: thesis: ex q being Nat st
for m being Nat st q <= m holds
r < (Partial_Sums (Prob * (B ^\ n))) . m

A45: for m being Nat st n <= m holds
((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . m = (Partial_Sums (Prob * (B ^\ n))) . (m - n)
proof
let m be Nat; :: thesis: ( n <= m implies ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . m = (Partial_Sums (Prob * (B ^\ n))) . (m - n) )
assume n <= m ; :: thesis: ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . m = (Partial_Sums (Prob * (B ^\ n))) . (m - n)
then consider knat being Nat such that
A46: m = n + knat by NAT_1:10;
reconsider knat = knat as Nat ;
defpred S1[ Nat] means ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (n + \$1) = (Partial_Sums (Prob * (B ^\ n))) . ((n + \$1) - n);
A47: S1[ 0 ]
proof
A48: n in NAT by ORDINAL1:def 12;
dom ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) = NAT by FUNCT_2:def 1;
then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = ((Partial_Sums (Prob * B)) . n) + ((NAT --> (- ((Partial_Sums (Prob * B)) . y))) . n) by ;
then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = ((Partial_Sums (Prob * B)) . n) + (- ((Partial_Sums (Prob * B)) . (n - 1))) by ;
then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = ((Partial_Sums (Prob * B)) . n) - ((Partial_Sums (Prob * B)) . (n - 1)) ;
then A49: ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = (((Partial_Sums (Prob * B)) . (n - 1)) + ((Prob * B) . ((n - 1) + 1))) - ((Partial_Sums (Prob * B)) . (n - 1)) by SERIES_1:def 1;
dom (Prob * (B ^\ n)) = NAT by FUNCT_2:def 1;
then A50: (Prob * (B ^\ n)) . 0 = Prob . ((B ^\ n) . 0) by FUNCT_1:12;
A51: (B ^\ n) . 0 = B . (0 + n) by NAT_1:def 3;
dom (Prob * B) = NAT by FUNCT_2:def 1;
then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = (Prob * (B ^\ n)) . 0 by ;
hence S1[ 0 ] by SERIES_1:def 1; :: thesis: verum
end;
A52: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
A53: n + k in NAT by ORDINAL1:def 12;
assume A54: S1[k] ; :: thesis: S1[k + 1]
A55: dom ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) = NAT by FUNCT_2:def 1;
((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = ((Partial_Sums (Prob * B)) . ((n + k) + 1)) + ((NAT --> (- ((Partial_Sums (Prob * B)) . y))) . ((n + k) + 1)) by ;
then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = (((Partial_Sums (Prob * B)) . (n + k)) + ((Prob * B) . ((n + k) + 1))) + ((NAT --> (- ((Partial_Sums (Prob * B)) . y))) . ((n + k) + 1)) by SERIES_1:def 1;
then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = (((Partial_Sums (Prob * B)) . (n + k)) + ((Prob * B) . ((n + k) + 1))) + (- ((Partial_Sums (Prob * B)) . (n - 1))) ;
then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = (((Partial_Sums (Prob * B)) . (n + k)) + ((Prob * B) . ((n + k) + 1))) + ((NAT --> (- ((Partial_Sums (Prob * B)) . y))) . (n + k)) by ;
then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = (((Partial_Sums (Prob * B)) . (n + k)) + ((NAT --> (- ((Partial_Sums (Prob * B)) . y))) . (n + k))) + ((Prob * B) . ((n + k) + 1)) ;
then A56: ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . ((n + k) + 1) = ((Partial_Sums (Prob * (B ^\ n))) . ((n + k) - n)) + ((Prob * B) . ((n + k) + 1)) by ;
(Prob * (B ^\ n)) . (((n + k) - n) + 1) = (Prob * B) . ((n + k) + 1)
proof
dom (Prob * (B ^\ n)) = NAT by FUNCT_2:def 1;
then A57: (Prob * (B ^\ n)) . (((n + k) - n) + 1) = Prob . ((B ^\ n) . (k + 1)) by FUNCT_1:12;
A58: (B ^\ n) . (k + 1) = B . (n + (k + 1)) by NAT_1:def 3;
dom (Prob * B) = NAT by FUNCT_2:def 1;
hence (Prob * (B ^\ n)) . (((n + k) - n) + 1) = (Prob * B) . ((n + k) + 1) by ; :: thesis: verum
end;
hence S1[k + 1] by ; :: thesis: verum
end;
for k being Nat holds S1[k] from then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (n + knat) = (Partial_Sums (Prob * (B ^\ n))) . ((n + knat) - n) ;
hence ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . m = (Partial_Sums (Prob * (B ^\ n))) . (m - n) by A46; :: thesis: verum
end;
A59: ex q being Nat st
for m being Nat st q + n <= m + n holds
r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n)
proof
consider q being Nat such that
A60: for m being Nat st q <= m holds
r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . m by ;
take q ; :: thesis: for m being Nat st q + n <= m + n holds
r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n)

let m be Nat; :: thesis: ( q + n <= m + n implies r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n) )
assume q + n <= m + n ; :: thesis: r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n)
then ( q <= q + n & q + n <= m + n ) by NAT_1:11;
then q <= m + n by XXREAL_0:2;
hence r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n) by A60; :: thesis: verum
end;
consider q being Nat such that
A61: for m being Nat st q + n <= m + n holds
r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n) by A59;
take s = q + n; :: thesis: for m being Nat st s <= m holds
r < (Partial_Sums (Prob * (B ^\ n))) . m

let m be Nat; :: thesis: ( s <= m implies r < (Partial_Sums (Prob * (B ^\ n))) . m )
assume A62: s <= m ; :: thesis: r < (Partial_Sums (Prob * (B ^\ n))) . m
set z = m + n;
((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n) = (Partial_Sums (Prob * (B ^\ n))) . ((m + n) - n) by ;
hence r < (Partial_Sums (Prob * (B ^\ n))) . m by ; :: thesis: verum
end;
hence ex q being Nat st
for m being Nat st q <= m holds
r < (Partial_Sums (Prob * (B ^\ n))) . m ; :: thesis: verum
end;
hence Partial_Sums (Prob * (B ^\ n)) is divergent_to+infty by LIMFUNC1:def 4; :: thesis: verum
end;
end;
end;
A63: for A being SetSequence of Sigma st Partial_Sums (Prob * A) is divergent_to+infty holds
( lim ((1 + (Partial_Sums (Prob * A))) ") = 0 & (1 + (Partial_Sums (Prob * A))) " is convergent )
proof
let A be SetSequence of Sigma; :: thesis: ( Partial_Sums (Prob * A) is divergent_to+infty implies ( lim ((1 + (Partial_Sums (Prob * A))) ") = 0 & (1 + (Partial_Sums (Prob * A))) " is convergent ) )
A64: for A being SetSequence of Sigma st ( for r being Real ex n being Nat st
for m being Nat st n <= m holds
r < (Partial_Sums (Prob * A)) . m ) holds
for r being Real ex n being Nat st
for m being Nat st n <= m holds
r < (1 + (Partial_Sums (Prob * A))) . m
proof
let A be SetSequence of Sigma; :: thesis: ( ( for r being Real ex n being Nat st
for m being Nat st n <= m holds
r < (Partial_Sums (Prob * A)) . m ) implies for r being Real ex n being Nat st
for m being Nat st n <= m holds
r < (1 + (Partial_Sums (Prob * A))) . m )

assume A65: for r being Real ex n being Nat st
for m being Nat st n <= m holds
r < (Partial_Sums (Prob * A)) . m ; :: thesis: for r being Real ex n being Nat st
for m being Nat st n <= m holds
r < (1 + (Partial_Sums (Prob * A))) . m

let r be Real; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
r < (1 + (Partial_Sums (Prob * A))) . m

consider n being Nat such that
A66: for m being Nat st n <= m holds
r < (Partial_Sums (Prob * A)) . m by A65;
take n ; :: thesis: for m being Nat st n <= m holds
r < (1 + (Partial_Sums (Prob * A))) . m

for m being Nat st n <= m holds
r < (1 + (Partial_Sums (Prob * A))) . m
proof
let m be Nat; :: thesis: ( n <= m implies r < (1 + (Partial_Sums (Prob * A))) . m )
A67: m in NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis: r < (1 + (Partial_Sums (Prob * A))) . m
then A68: r < (Partial_Sums (Prob * A)) . m by A66;
A69: (Partial_Sums (Prob * A)) . m < ((Partial_Sums (Prob * A)) . m) + 1 by XREAL_1:29;
(1 + (Partial_Sums (Prob * A))) . m = ((Partial_Sums (Prob * A)) . m) + 1 by ;
hence r < (1 + (Partial_Sums (Prob * A))) . m by ; :: thesis: verum
end;
hence for m being Nat st n <= m holds
r < (1 + (Partial_Sums (Prob * A))) . m ; :: thesis: verum
end;
assume Partial_Sums (Prob * A) is divergent_to+infty ; :: thesis: ( lim ((1 + (Partial_Sums (Prob * A))) ") = 0 & (1 + (Partial_Sums (Prob * A))) " is convergent )
then for r being Real ex n being Nat st
for m being Nat st n <= m holds
r < (Partial_Sums (Prob * A)) . m by LIMFUNC1:def 4;
then for r being Real ex n being Nat st
for m being Nat st n <= m holds
r < (1 + (Partial_Sums (Prob * A))) . m by A64;
then 1 + (Partial_Sums (Prob * A)) is divergent_to+infty by LIMFUNC1:def 4;
hence ( lim ((1 + (Partial_Sums (Prob * A))) ") = 0 & (1 + (Partial_Sums (Prob * A))) " is convergent ) by LIMFUNC1:34; :: thesis: verum
end;
Partial_Intersection (Complement (B ^\ n)) is non-ascending by PROB_3:27;
then A70: ( Prob * (Partial_Intersection (Complement (B ^\ n))) is convergent & (1 + (Partial_Sums (Prob * (B ^\ n)))) " is convergent ) by ;
A71: lim ((1 + (Partial_Sums (Prob * (B ^\ n)))) ") = 0 by ;
A72: for k being Nat holds 0 <= (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k A74: lim (Prob * (Partial_Intersection (Complement (B ^\ n)))) <= 0 by ;
Complement (B ^\ n) = () ^\ n
proof
for k being object st k in NAT holds
(Complement (B ^\ n)) . k = (() ^\ n) . k
proof
let k be object ; :: thesis: ( k in NAT implies (Complement (B ^\ n)) . k = (() ^\ n) . k )
assume k in NAT ; :: thesis: (Complement (B ^\ n)) . k = (() ^\ n) . k
then reconsider k = k as Nat ;
A75: (Complement (B ^\ n)) . k = ((B ^\ n) . k) ` by PROB_1:def 2;
((Complement B) ^\ n) . k = () . (k + n) by NAT_1:def 3;
then ((Complement B) ^\ n) . k = (B . (k + n)) ` by PROB_1:def 2;
hence (Complement (B ^\ n)) . k = (() ^\ n) . k by ; :: thesis: verum
end;
hence Complement (B ^\ n) = () ^\ n ; :: thesis: verum
end;
hence (Prob * ) . n = 0 by ; :: thesis: verum
end;
set B2 = seq_const 0;
A76: ex n being Nat st () . n = 0
proof
take 1 ; :: thesis: () . 1 = 0
thus (seq_const 0) . 1 = 0 ; :: thesis: verum
end;
A77: lim () = 0 by ;
A78: ( seq_const 0 is convergent & ex k being Nat st
for n being Nat st k <= n holds
() . n = (Prob * ) . n )
proof
ex k being Nat st
for n being Nat st k <= n holds
() . n = (Prob * ) . n
proof
A79: for n being Nat st n >= 0 holds
() . n = (Prob * ) . n
proof
let n be Nat; :: thesis: ( n >= 0 implies () . n = (Prob * ) . n )
assume n >= 0 ; :: thesis: () . n = (Prob * ) . n
( (seq_const 0) . n = 0 & (Prob * ) . n = 0 ) by A16;
hence (seq_const 0) . n = (Prob * ) . n ; :: thesis: verum
end;
take 0 ; :: thesis: for n being Nat st 0 <= n holds
() . n = (Prob * ) . n

thus for n being Nat st 0 <= n holds
() . n = (Prob * ) . n by A79; :: thesis: verum
end;
hence ( seq_const 0 is convergent & ex k being Nat st
for n being Nat st k <= n holds
() . n = (Prob * ) . n ) ; :: thesis: verum
end;
( Prob . () = 0 & (Prob . ()) + (Prob . ()) = 1 ) by ;
hence ( Prob . () = 0 & Prob . () = 1 ) ; :: thesis: verum
end;
hence ( Prob . () = 0 & Prob . () = 1 ) by A9, A10, A7, A8; :: thesis: verum
end;
hence ( ( Partial_Sums (Prob * A) is convergent implies ( Prob . () = 0 & Prob . () = 1 ) ) & ( A is_all_independent_wrt Prob & Partial_Sums (Prob * A) is divergent_to+infty implies ( Prob . () = 0 & Prob . () = 1 ) ) ) by A5, A1; :: thesis: verum