let Omega be non empty set ; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
let Prob be Probability of Sigma; :: thesis:
let A be SetSequence of Sigma; :: thesis:
A1: ( Partial_Sums (Prob * A) is convergent implies Prob . (lim_inf (Complement A)) = 1 )

assume A2: Partial_Sums (Prob * A) is convergent ; :: thesis:
A3: Prob . (lim_inf (Complement A)) = Prob . (@lim_inf (Complement A)) by Lemma;
for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds
( Prob . (@lim_inf (Complement A)) = 1 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )

let A be SetSequence of Sigma; :: thesis:
assume A4: Partial_Sums (Prob * A) is convergent ; :: thesis:
( (Prob . (@lim_sup A)) + (Prob . (@lim_inf (Complement A))) = 0 + (Prob . (@lim_inf (Complement A))) & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent ) by A4, Th13;
hence ( Prob . (@lim_inf (Complement A)) = 1 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent ) by Th15; :: thesis:

end;

hence Prob . (lim_inf (Complement A)) = 1 by A2, A3; :: thesis:

end;

A5: for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds
Prob . (lim_sup A) = 0

proof

let A be SetSequence of Sigma; :: thesis:
assume A6: Partial_Sums (Prob * A) is convergent ; :: thesis:
Prob . (lim_sup A) = Prob . (@lim_sup A) ;
hence Prob . (lim_sup A) = 0 by A6, Th13; :: thesis:

end;

for B being SetSequence of Sigma st B is_all_independent_wrt Prob & Partial_Sums (Prob * B) is divergent_to+infty holds
( Prob . (lim_inf (Complement B)) = 0 & Prob . (lim_sup B) = 1 )

proof

let B be SetSequence of Sigma; :: thesis:
assume that
A7: B is_all_independent_wrt Prob and
A8: Partial_Sums (Prob * B) is divergent_to+infty ; :: thesis:
A9: Prob . (@lim_sup B) = Prob . (lim_sup B) ;
A10: Prob . (@lim_inf (Complement B)) = Prob . (lim_inf (Complement B)) by Lemma;
for B being SetSequence of Sigma st B is_all_independent_wrt Prob & Partial_Sums (Prob * B) is divergent_to+infty holds
( Prob . (@lim_inf (Complement B)) = 0 & Prob . (@lim_sup B) = 1 )

proof

let B be SetSequence of Sigma; :: thesis:
assume that
A11: B is_all_independent_wrt Prob and
A12: Partial_Sums (Prob * B) is divergent_to+infty ; :: thesis:
reconsider CB = Complement B as SetSequence of Sigma ;
A15: Prob . (@lim_inf CB) = lim (Prob * (inferior_setsequence (Complement B))) by PROB_2:10;
A16: for n being Nat holds (Prob * (inferior_setsequence (Complement B))) . n = 0

proof

let n be Nat; :: thesis:
dom (Prob * (inferior_setsequence (Complement B))) = NAT by FUNCT_2:def 1;
then A18: (Prob * (inferior_setsequence (Complement B))) . n = Prob . ((inferior_setsequence (Complement B)) . n) by FUNCT_1:12, ORDINAL1:def 12;
(inferior_setsequence (Complement B)) . n = Intersection ((Complement B) ^\ n) by Def9;
then A19: (Prob * (inferior_setsequence (Complement B))) . n = Prob . (Intersection (Partial_Intersection ((Complement B) ^\ n))) by A18, PROB_3:29;
Partial_Intersection ((Complement B) ^\ n) is non-ascending by PROB_3:27;
then A20: (Prob * (inferior_setsequence (Complement B))) . n = lim (Prob * (Partial_Intersection ((Complement B) ^\ n))) by A19, PROB_1:def 8;
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:
A22: for k being Nat holds B ^\ k is_all_independent_wrt Prob

proof

let k be Nat; :: thesis:
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 . ((Partial_Intersection C) . n)

proof

let C be SetSequence of Sigma; :: thesis:
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:
A25: B ^\ k = B * (Special_Function2 k)

proof

for n being object st n in NAT holds
(B ^\ k) . n = (B * (Special_Function2 k)) . n

proof

let n be object ; :: thesis:
assume n in NAT ; :: thesis:
then reconsider n = n as Element of NAT ;
dom (B * (Special_Function2 k)) = NAT by FUNCT_2:def 1;
then A26: (B * (Special_Function2 k)) . n = B . ((Special_Function2 k) . n) by FUNCT_1:12;
(Special_Function2 k) . n = n + k by Def3;
hence (B ^\ k) . n = (B * (Special_Function2 k)) . n by A26, NAT_1:def 3; :: thesis:

end;

hence B ^\ k = B * (Special_Function2 k) ; :: thesis:

end;

A27: for n being Nat holds (B * (Special_Function2 k)) . (e . n) = B . (((Special_Function2 k) * e) . n)

proof

let n be Nat; :: thesis:
reconsider n = n as Element of NAT by ORDINAL1:def 12;
( dom (B * (Special_Function2 k)) = NAT & dom ((Special_Function2 k) * e) = NAT ) by FUNCT_2:def 1;
then ( (B * (Special_Function2 k)) . (e . n) = B . ((Special_Function2 k) . (e . n)) & ((Special_Function2 k) * e) . n = (Special_Function2 k) . (e . n) ) by FUNCT_1:12;
hence (B * (Special_Function2 k)) . (e . n) = B . (((Special_Function2 k) * e) . n) ; :: thesis:

end;

A28: for n being Nat holds B . (((Special_Function2 k) * e) . n) = C . n

proof

let n be Nat; :: thesis:
(B * (Special_Function2 k)) . (e . n) = C . n by A25, A24;
hence B . (((Special_Function2 k) * e) . n) = C . n by A27; :: thesis:

end;

(Special_Function2 k) * e is one-to-one by A23, FUNCT_1:24;
hence for n being Nat holds (Partial_Product (Prob * C)) . n = Prob . ((Partial_Intersection C) . n) by A11, A28; :: thesis:

end;

hence B ^\ k is_all_independent_wrt Prob by Def6; :: thesis:

end;

A29: for A being SetSequence of Sigma
for n being Nat holds (Partial_Product (Prob * (Complement A))) . n <= ((1 + (Partial_Sums (Prob * A))) . n) "

proof

let A be SetSequence of Sigma; :: thesis:
let n be Nat; :: thesis:
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A30: (Partial_Product (Prob * (Complement A))) . n <= 1 / (1 + ((Partial_Sums (Prob * A)) . n))

proof

(Partial_Product (Prob * (Complement A))) . n <= (Partial_Product (JSum (Prob * A))) . n by Th4;
then A31: (Partial_Product (Prob * (Complement A))) . 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:
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:

end;

A33: for n being Nat holds (Partial_Sums (Prob * A)) . n >= 0

proof

let n be Nat; :: thesis:
defpred S₁[ Nat] means (Partial_Sums (Prob * A)) . $1 >= 0 ;
(Partial_Sums (Prob * A)) . 0 = (Prob * A) . 0 by SERIES_1:def 1;
then A34: S₁[ 0 ] by A32;
A35: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A36: S₁[k] ; :: thesis:
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 S₁[k + 1] by A36, A37; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A34, A35);
hence (Partial_Sums (Prob * A)) . n >= 0 ; :: thesis:

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:
assume A38: x >= 0 ; :: thesis:

per cases ;

suppose A39: x > 0 ; :: thesis:

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 Th2, A40, A41, SIN_COS:51, XREAL_1:64;
hence exp_R . (- x) <= 1 / (1 + x) by A39, XREAL_1:77; :: thesis:

end;

suppose x <= 0 ; :: thesis:

then x = 0 by A38;
hence exp_R . (- x) <= 1 / (1 + x) by SIN_COS:51; :: thesis:

end;

hence exp_R . (- ((Partial_Sums (Prob * A)) . n)) <= 1 / (1 + ((Partial_Sums (Prob * A)) . n)) by A33; :: thesis:

end;

hence (Partial_Product (Prob * (Complement A))) . n <= 1 / (1 + ((Partial_Sums (Prob * A)) . n)) by A31, XXREAL_0:2; :: thesis:

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:
let n be Nat; :: thesis:
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:

end;

hence (Partial_Product (Prob * (Complement A))) . n <= ((1 + (Partial_Sums (Prob * A))) . n) " by A30; :: thesis:

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 A22, Th10;
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:

end;

A42: Partial_Sums (Prob * (B ^\ n)) is divergent_to+infty

proof

per cases ;

suppose n = 0 ; :: thesis:

hence Partial_Sums (Prob * (B ^\ n)) is divergent_to+infty by A12, NAT_1:47; :: thesis:

end;

suppose n <> 0 ; :: thesis:

then reconsider y = n - 1 as Element of NAT by NAT_1:20;
set B2 = NAT --> (- ((Partial_Sums (Prob * B)) . y));
A44: (Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y))) is divergent_to+infty by A12, LIMFUNC1:18;
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:
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:
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:
assume n <= m ; :: thesis:
then consider knat being Nat such that
A46: m = n + knat by NAT_1:10;
reconsider knat = knat as Nat ;
defpred S₁[ Nat] means ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (n + $1) = (Partial_Sums (Prob * (B ^\ n))) . ((n + $1) - n);
A47: S₁[ 0 ]

proof

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 VALUED_1:def 1, ORDINAL1:def 12;
then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = ((Partial_Sums (Prob * B)) . n) + (- ((Partial_Sums (Prob * B)) . (n - 1))) by FUNCOP_1:7, ORDINAL1:def 12;
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 A51, A50, A49, FUNCT_1:12, ORDINAL1:def 12;
hence S₁[ 0 ] by SERIES_1:def 1; :: thesis:

end;

A52: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A54: S₁[k] ; :: thesis:
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 A55, VALUED_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))) + ((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))) + ((NAT --> (- ((Partial_Sums (Prob * B)) . y))) . (n + k)) by FUNCOP_1:7, ORDINAL1:def 12;
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 A55, A54, VALUED_1:def 1, ORDINAL1:def 12;
(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 A58, A57, FUNCT_1:12; :: thesis:

end;

hence S₁[k + 1] by A56, SERIES_1:def 1; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A47, A52);
hence ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . m = (Partial_Sums (Prob * (B ^\ n))) . (m - n) by A46; :: thesis:

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 A44, LIMFUNC1:def 4;
take q ; :: thesis:
let m be Nat; :: thesis:
assume q + n <= m + n ; :: thesis:
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:

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:
let m be Nat; :: thesis:
assume A62: s <= m ; :: thesis:
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 A45, NAT_1:12;
hence r < (Partial_Sums (Prob * (B ^\ n))) . m by A62, A61, NAT_1:12; :: thesis:

end;

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

end;

hence Partial_Sums (Prob * (B ^\ n)) is divergent_to+infty by LIMFUNC1:def 4; :: thesis:

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:
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:
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:
let r be Real; :: thesis:
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

proof

let m be Nat; :: thesis:
A67: m in NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis:
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 VALUED_1:2, A67;
hence r < (1 + (Partial_Sums (Prob * A))) . m by A68, A69, XXREAL_0:2; :: thesis:

end;

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

end;

assume Partial_Sums (Prob * A) is divergent_to+infty ; :: thesis:
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:

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 A42, A63, PROB_1:def 8;
A71: lim ((1 + (Partial_Sums (Prob * (B ^\ n)))) ") = 0 by A42, A63;
A72: for k being Nat holds 0 <= (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k

proof

let k be Nat; :: thesis:
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, ORDINAL1:def 12;
hence 0 <= (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k by PROB_1:def 8; :: thesis:

end;

A74: lim (Prob * (Partial_Intersection (Complement (B ^\ n)))) <= 0 by A70, A21, A71, SEQ_2:18;
Complement (B ^\ n) = (Complement B) ^\ n

proof

for k being object st k in NAT holds
(Complement (B ^\ n)) . k = ((Complement B) ^\ n) . k

proof

let k be object ; :: thesis:
assume k in NAT ; :: thesis:
then reconsider k = k as Nat ;
A75: (Complement (B ^\ n)) . k = ((B ^\ n) . k) ` by PROB_1:def 2;
((Complement B) ^\ n) . k = (Complement B) . (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 = ((Complement B) ^\ n) . k by A75, NAT_1:def 3; :: thesis:

end;

hence Complement (B ^\ n) = (Complement B) ^\ n ; :: thesis:

end;

hence (Prob * (inferior_setsequence (Complement B))) . n = 0 by A72, A70, A74, A20, SEQ_2:17; :: thesis:

end;

set B2 = seq_const 0;
ex n being Nat st (seq_const 0) . n = 0

proof

take 1 ; :: thesis:
thus (seq_const 0) . 1 = 0 ; :: thesis:

end;

then A77: lim (seq_const 0) = 0 by SEQ_4:25;
A78: ( seq_const 0 is convergent & ex k being Nat st
for n being Nat st k <= n holds
(seq_const 0) . n = (Prob * (inferior_setsequence (Complement B))) . n )

proof

ex k being Nat st
for n being Nat st k <= n holds
(seq_const 0) . n = (Prob * (inferior_setsequence (Complement B))) . n

proof

take 0 ; :: thesis:
thus for n being Nat st 0 <= n holds
(seq_const 0) . n = (Prob * (inferior_setsequence (Complement B))) . n by A16; :: thesis:

end;

hence ( seq_const 0 is convergent & ex k being Nat st
for n being Nat st k <= n holds
(seq_const 0) . n = (Prob * (inferior_setsequence (Complement B))) . n ) ; :: thesis:

end;

( Prob . (@lim_inf (Complement B)) = 0 & (Prob . (@lim_inf (Complement B))) + (Prob . (@lim_sup B)) = 1 ) by A15, A78, A77, Th15, SEQ_4:19;
hence ( Prob . (@lim_inf (Complement B)) = 0 & Prob . (@lim_sup B) = 1 ) ; :: thesis:

end;

hence ( Prob . (lim_inf (Complement B)) = 0 & Prob . (lim_sup B) = 1 ) by A9, A10, A7, A8; :: thesis:

end;

hence ( ( Partial_Sums (Prob * A) is convergent implies ( Prob . (lim_sup A) = 0 & Prob . (lim_inf (Complement A)) = 1 ) ) & ( A is_all_independent_wrt Prob & Partial_Sums (Prob * A) is divergent_to+infty implies ( Prob . (lim_inf (Complement A)) = 0 & Prob . (lim_sup A) = 1 ) ) ) by A5, A1; :: thesis: