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 . (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 ) ) )
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 . (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 ) ) )
let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma holds
( ( 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 ) ) )
let A be SetSequence of Sigma; :: thesis: ( ( 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 ) ) )
A1: ( Partial_Sums (Prob * A) is convergent implies Prob . (lim_inf (Complement A)) = 1 )

proof

assume A2: Partial_Sums (Prob * A) is convergent ; :: thesis: Prob . (lim_inf (Complement A)) = 1
A3: Prob . (lim_inf (Complement A)) = Prob . (@lim_inf (Complement A)) by Th15;
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 )

proof

let A be SetSequence of Sigma; :: thesis: ( Partial_Sums (Prob * A) is convergent implies ( Prob . (@lim_inf (Complement A)) = 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 . (@lim_inf (Complement A)) = 1 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )
( (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: verum

end;

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

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: ( Partial_Sums (Prob * A) is convergent implies Prob . (lim_sup A) = 0 )
assume A6: Partial_Sums (Prob * A) is convergent ; :: thesis: Prob . (lim_sup A) = 0
Prob . (lim_sup A) = Prob . (@lim_sup A) by Th15;
hence Prob . (lim_sup A) = 0 by A6, Th13; :: 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 . (lim_inf (Complement B)) = 0 & Prob . (lim_sup B) = 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 . (lim_inf (Complement B)) = 0 & Prob . (lim_sup B) = 1 ) )
assume that
A7: B is_all_independent_wrt Prob and
A8: Partial_Sums (Prob * B) is divergent_to+infty ; :: thesis: ( Prob . (lim_inf (Complement B)) = 0 & Prob . (lim_sup B) = 1 )
A9: Prob . (@lim_sup B) = Prob . (lim_sup B) by Th15;
A10: Prob . (@lim_inf (Complement B)) = Prob . (lim_inf (Complement B)) 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 . (@lim_inf (Complement B)) = 0 & Prob . (@lim_sup B) = 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 . (@lim_inf (Complement B)) = 0 & Prob . (@lim_sup B) = 1 ) )
assume that
A11: B is_all_independent_wrt Prob and
A12: Partial_Sums (Prob * B) is divergent_to+infty ; :: thesis: ( Prob . (@lim_inf (Complement B)) = 0 & Prob . (@lim_sup B) = 1 )
A13: for Q being SetSequence of Sigma holds Intersect_Shift_Seq Q is non-descending

proof

let Q be SetSequence of Sigma; :: thesis: Intersect_Shift_Seq Q is non-descending
inferior_setsequence Q = Intersect_Shift_Seq Q by Th11;
hence Intersect_Shift_Seq Q is non-descending ; :: thesis: verum

end;

A14: Intersect_Shift_Seq (Complement B) is non-descending by A13;
reconsider CB = Complement B as SetSequence of Sigma ;
A15: Prob . (@lim_inf CB) = lim (Prob * (Intersect_Shift_Seq (Complement B))) by A14, PROB_2:10;
A16: for n being Element of NAT holds (Prob * (Intersect_Shift_Seq (Complement B))) . n = 0

proof

let n be Element of NAT ; :: thesis: (Prob * (Intersect_Shift_Seq (Complement B))) . n = 0
dom (Prob * (Intersect_Shift_Seq (Complement B))) = NAT by FUNCT_2:def 1;
then A17: (Prob * (Intersect_Shift_Seq (Complement B))) . n = Prob . ((Intersect_Shift_Seq (Complement B)) . n) by FUNCT_1:12;
(Intersect_Shift_Seq (Complement B)) . n = Intersection ((Complement B) ^\ n) by Def12;
then A18: (Prob * (Intersect_Shift_Seq (Complement B))) . n = Prob . (Intersection (Partial_Intersection ((Complement B) ^\ n))) by A17, PROB_3:29;
Partial_Intersection ((Complement B) ^\ n) is non-ascending by PROB_3:27;
then A19: (Prob * (Intersect_Shift_Seq (Complement B))) . n = lim (Prob * (Partial_Intersection ((Complement B) ^\ n))) by A18, PROB_1:def 8;
A20: for k being Element of NAT holds (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k <= ((1 + (Partial_Sums (Prob * (B ^\ n)))) ") . k

proof

let k be Element of NAT ; :: thesis: (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k <= ((1 + (Partial_Sums (Prob * (B ^\ n)))) ") . k
A21: for k being Element of NAT holds B ^\ k is_all_independent_wrt Prob

proof

let k be Element of 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 Element of NAT holds (B ^\ k) . (e . n) = C . n ) ) holds
for n being Element of NAT holds (Partial_Product (Prob * C)) . n = Prob . ((Partial_Intersection C) . n)

proof

let C be SetSequence of Sigma; :: thesis: ( ex e being sequence of NAT st
( e is one-to-one & ( for n being Element of NAT holds (B ^\ k) . (e . n) = C . n ) ) implies for n being Element of NAT holds (Partial_Product (Prob * C)) . n = Prob . ((Partial_Intersection C) . n) )
given e being sequence of NAT such that A22: e is one-to-one and
A23: for n being Element of NAT holds (B ^\ k) . (e . n) = C . n ; :: thesis: for n being Element of NAT holds (Partial_Product (Prob * C)) . n = Prob . ((Partial_Intersection C) . n)
A24: B ^\ k = B * (Special_Function2 k)

proof

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

proof

let n be set ; :: thesis: ( n in NAT implies (B ^\ k) . n = (B * (Special_Function2 k)) . n )
assume n in NAT ; :: thesis: (B ^\ k) . n = (B * (Special_Function2 k)) . n
then reconsider n = n as Element of NAT ;
dom (B * (Special_Function2 k)) = NAT by FUNCT_2:def 1;
then A25: (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 A25, NAT_1:def 3; :: thesis: verum

end;

hence B ^\ k = B * (Special_Function2 k) by FUNCT_2:12; :: thesis: verum

end;

A26: for n being Element of NAT holds (B * (Special_Function2 k)) . (e . n) = B . (((Special_Function2 k) * e) . n)

proof

let n be Element of NAT ; :: thesis: (B * (Special_Function2 k)) . (e . n) = B . (((Special_Function2 k) * e) . n)
( 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: verum

end;

A27: for n being Element of NAT holds B . (((Special_Function2 k) * e) . n) = C . n

proof

let n be Element of NAT ; :: thesis: B . (((Special_Function2 k) * e) . n) = C . n
(B * (Special_Function2 k)) . (e . n) = C . n by A24, A23;
hence B . (((Special_Function2 k) * e) . n) = C . n by A26; :: thesis: verum

end;

(Special_Function2 k) * e is one-to-one by A22, FUNCT_1:24;
hence for n being Element of NAT holds (Partial_Product (Prob * C)) . n = Prob . ((Partial_Intersection C) . n) by A11, A27, Def8; :: thesis: verum

end;

hence B ^\ k is_all_independent_wrt Prob by Def8; :: thesis: verum

end;

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

proof

let A be SetSequence of Sigma; :: thesis: for n being Element of NAT holds (Partial_Product (Prob * (Complement A))) . n <= ((1 + (Partial_Sums (Prob * A))) . n) "
let n be Element of NAT ; :: thesis: (Partial_Product (Prob * (Complement A))) . n <= ((1 + (Partial_Sums (Prob * A))) . n) "
A29: (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 A30: (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

A31: for n being Element of NAT holds (Prob * A) . n >= 0

proof

let n be Element of NAT ; :: thesis: (Prob * A) . n >= 0
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;

A32: for n being Element of NAT holds (Partial_Sums (Prob * A)) . n >= 0

proof

let n be Element of NAT ; :: thesis: (Partial_Sums (Prob * A)) . n >= 0
defpred S₁[ Element of NAT ] means (Partial_Sums (Prob * A)) . $1 >= 0 ;
(Partial_Sums (Prob * A)) . 0 = (Prob * A) . 0 by SERIES_1:def 1;
then A33: S₁[ 0 ] by A31;
A34: 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 A35: S₁[k] ; :: thesis: S₁[k + 1]
A36: (Prob * A) . (k + 1) >= 0 by A31;
(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 A35, A36; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A33, A34);
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 A37: x >= 0 ; :: thesis: exp_R . (- x) <= 1 / (1 + x)

per cases ( x > 0 or x <= 0 ) ;

suppose A38: x > 0 ; :: thesis: exp_R . (- x) <= 1 / (1 + x)

A39: exp_R . (- x) >= 0 by SIN_COS:54;
set z = - x;
A40: (exp_R x) * (exp_R (- x)) = exp_R (x + (- x)) by SIN_COS:50;
(exp_R . (- x)) * (1 + x) <= 1 by Th2, A39, A40, SIN_COS:51, XREAL_1:64;
hence exp_R . (- x) <= 1 / (1 + x) by A38, XREAL_1:77; :: thesis: verum

end;

suppose x <= 0 ; :: thesis: exp_R . (- x) <= 1 / (1 + x)

then x = 0 by A37;
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 A32; :: thesis: verum

end;

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

end;

for A being SetSequence of Sigma
for n being Element of 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 Element of NAT holds 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = ((1 + (Partial_Sums (Prob * A))) . n) "
let n be Element of NAT ; :: thesis: 1 / (1 + ((Partial_Sums (Prob * A)) . n)) = ((1 + (Partial_Sums (Prob * A))) . n) "
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 * (Complement A))) . n <= ((1 + (Partial_Sums (Prob * A))) . n) " by A29; :: thesis: verum

end;

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 A21, Th10;
then (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k <= ((1 + (Partial_Sums (Prob * (B ^\ n)))) . k) " by A28;
hence (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k <= ((1 + (Partial_Sums (Prob * (B ^\ n)))) ") . k by VALUED_1:10; :: thesis: verum

end;

A41: 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

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

end;

suppose n <> 0 ; :: thesis: Partial_Sums (Prob * (B ^\ n)) is divergent_to+infty

then A42: n - 1 is Element of NAT by NAT_1:20;
consider y being Element of NAT such that
A43: y = n - 1 by A42;
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 Element of NAT st
for m being Element of NAT st q <= m holds
r < (Partial_Sums (Prob * (B ^\ n))) . m

proof

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

proof

let r be Real; :: thesis: ex q being Element of NAT st
for m being Element of NAT st q <= m holds
r < (Partial_Sums (Prob * (B ^\ n))) . m
A45: for m being Element of 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 Element of 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 Element of NAT by ORDINAL1:def 12;
defpred S₁[ Element of 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;
then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = ((Partial_Sums (Prob * B)) . n) + (- ((Partial_Sums (Prob * B)) . (n - 1))) by A43, FUNCOP_1:7;
then ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . n = ((Partial_Sums (Prob * B)) . n) - ((Partial_Sums (Prob * B)) . (n - 1)) ;
then A48: ((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 A42, SERIES_1:def 1;
dom (Prob * (B ^\ n)) = NAT by FUNCT_2:def 1;
then A49: (Prob * (B ^\ n)) . 0 = Prob . ((B ^\ n) . 0) by FUNCT_1:12;
A50: (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 A50, A49, A48, FUNCT_1:12;
hence S₁[ 0 ] by SERIES_1:def 1; :: thesis: verum

end;

A51: 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 A52: S₁[k] ; :: thesis: S₁[k + 1]
A53: 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 A53, 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))) + (- ((Partial_Sums (Prob * B)) . (n - 1))) by A43, FUNCOP_1:7;
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 A43, FUNCOP_1:7;
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 A54: ((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 A53, A52, VALUED_1:def 1;
(Prob * (B ^\ n)) . (((n + k) - n) + 1) = (Prob * B) . ((n + k) + 1)

proof

dom (Prob * (B ^\ n)) = NAT by FUNCT_2:def 1;
then A55: (Prob * (B ^\ n)) . (((n + k) - n) + 1) = Prob . ((B ^\ n) . (k + 1)) by FUNCT_1:12;
A56: (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 A56, A55, FUNCT_1:12; :: thesis: verum

end;

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

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A47, A51);
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;

A57: ex q being Element of NAT st
for m being Element of NAT st q + n <= m + n holds
r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n)

proof

consider q being Element of NAT such that
A58: for m being Element of NAT st q <= m holds
r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . m by A44, LIMFUNC1:def 4;
for m being Element of NAT st q + n <= m + n holds
r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n)

proof

let m be Element of 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 A58; :: thesis: verum

end;

hence ex q being Element of NAT st
for m being Element of NAT st q + n <= m + n holds
r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n) ; :: thesis: verum

end;

ex s being Element of NAT st
for m being Element of NAT st s <= m holds
r < (Partial_Sums (Prob * (B ^\ n))) . m

proof

consider q being Element of NAT such that
A59: for m being Element of NAT st q + n <= m + n holds
r < ((Partial_Sums (Prob * B)) + (NAT --> (- ((Partial_Sums (Prob * B)) . y)))) . (m + n) by A57;
take s = q + n; :: thesis: for m being Element of NAT st s <= m holds
r < (Partial_Sums (Prob * (B ^\ n))) . m
let m be Element of NAT ; :: thesis: ( s <= m implies r < (Partial_Sums (Prob * (B ^\ n))) . m )
assume A60: 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 A45, NAT_1:12;
hence r < (Partial_Sums (Prob * (B ^\ n))) . m by A60, A59, NAT_1:12; :: thesis: verum

end;

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

end;

hence ex q being Element of NAT st
for m being Element of 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;

A61: 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 ) )
A62: for A being SetSequence of Sigma st ( for r being Real ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < (Partial_Sums (Prob * A)) . m ) holds
for r being Real ex n being Element of NAT st
for m being Element of 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 Element of NAT st
for m being Element of NAT st n <= m holds
r < (Partial_Sums (Prob * A)) . m ) implies for r being Real ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < (1 + (Partial_Sums (Prob * A))) . m )
assume A63: for r being Real ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < (Partial_Sums (Prob * A)) . m ; :: thesis: for r being Real ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < (1 + (Partial_Sums (Prob * A))) . m
let r be Real; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < (1 + (Partial_Sums (Prob * A))) . m
consider n being Element of NAT such that
A64: for m being Element of NAT st n <= m holds
r < (Partial_Sums (Prob * A)) . m by A63;
take n ; :: thesis: for m being Element of NAT st n <= m holds
r < (1 + (Partial_Sums (Prob * A))) . m
for m being Element of NAT st n <= m holds
r < (1 + (Partial_Sums (Prob * A))) . m

proof

let m be Element of NAT ; :: thesis: ( n <= m implies r < (1 + (Partial_Sums (Prob * A))) . m )
assume n <= m ; :: thesis: r < (1 + (Partial_Sums (Prob * A))) . m
then A65: r < (Partial_Sums (Prob * A)) . m by A64;
A66: (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;
hence r < (1 + (Partial_Sums (Prob * A))) . m by A65, A66, XXREAL_0:2; :: thesis: verum

end;

hence for m being Element of 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 Element of NAT st
for m being Element of NAT st n <= m holds
r < (Partial_Sums (Prob * A)) . m by LIMFUNC1:def 4;
then for r being Real ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < (1 + (Partial_Sums (Prob * A))) . m by A62;
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 A67: ( Prob * (Partial_Intersection (Complement (B ^\ n))) is convergent & (1 + (Partial_Sums (Prob * (B ^\ n)))) " is convergent ) by A41, A61, PROB_1:def 8;
A68: lim ((1 + (Partial_Sums (Prob * (B ^\ n)))) ") = 0 by A41, A61;
A69: for k being Element of NAT holds 0 <= (Prob * (Partial_Intersection (Complement (B ^\ n)))) . k

proof

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

end;

A70: lim (Prob * (Partial_Intersection (Complement (B ^\ n)))) <= 0 by A67, A20, A68, SEQ_2:18;
Complement (B ^\ n) = (Complement B) ^\ n

proof

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

proof

let k be set ; :: thesis: ( k in NAT implies (Complement (B ^\ n)) . k = ((Complement B) ^\ n) . k )
assume k in NAT ; :: thesis: (Complement (B ^\ n)) . k = ((Complement B) ^\ n) . k
then reconsider k = k as Element of NAT ;
A71: (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 A71, NAT_1:def 3; :: thesis: verum

end;

hence Complement (B ^\ n) = (Complement B) ^\ n by FUNCT_2:12; :: thesis: verum

end;

hence (Prob * (Intersect_Shift_Seq (Complement B))) . n = 0 by A69, A67, A70, A19, SEQ_2:17; :: thesis: verum

end;

set B2 = NAT --> 0;
A72: ex n being Element of NAT st (NAT --> 0) . n = 0

proof

take 1 ; :: thesis: (NAT --> 0) . 1 = 0
thus (NAT --> 0) . 1 = 0 by FUNCOP_1:7; :: thesis: verum

end;

A73: lim (NAT --> 0) = 0 by A72, SEQ_4:25;
A74: ( NAT --> 0 is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
(NAT --> 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n )

proof

ex k being Element of NAT st
for n being Element of NAT st k <= n holds
(NAT --> 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n

proof

A75: for n being Element of NAT st n >= 0 holds
(NAT --> 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n

proof

let n be Element of NAT ; :: thesis: ( n >= 0 implies (NAT --> 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n )
assume n >= 0 ; :: thesis: (NAT --> 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n
( (NAT --> 0) . n = 0 & (Prob * (Intersect_Shift_Seq (Complement B))) . n = 0 ) by A16, FUNCOP_1:7;
hence (NAT --> 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n ; :: thesis: verum

end;

take 0 ; :: thesis: for n being Element of NAT st 0 <= n holds
(NAT --> 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n
thus for n being Element of NAT st 0 <= n holds
(NAT --> 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n by A75; :: thesis: verum

end;

hence ( NAT --> 0 is convergent & ex k being Element of NAT st
for n being Element of NAT st k <= n holds
(NAT --> 0) . n = (Prob * (Intersect_Shift_Seq (Complement B))) . n ) ; :: thesis: verum

end;

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

end;

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

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: verum