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:
assume A1: Partial_Sums (Prob * A) is convergent ; :: thesis:
then A2: Prob * A is summable by SERIES_1:def 2;
A3: for n being Nat holds 0 <= (Prob * (Partial_Intersection (superior_setsequence A))) . n

let n be Nat; :: thesis:
dom (Prob * (Partial_Intersection (superior_setsequence A))) = NAT by FUNCT_2:def 1;
then (Prob * (Partial_Intersection (superior_setsequence A))) . n = Prob . ((Partial_Intersection (superior_setsequence A)) . n) by FUNCT_1:12, ORDINAL1:def 12;
hence 0 <= (Prob * (Partial_Intersection (superior_setsequence A))) . n by PROB_1:def 8; :: thesis:

end;

A5: Intersection (Partial_Intersection (superior_setsequence A)) = Intersection (superior_setsequence A) by PROB_3:29;
Partial_Intersection (superior_setsequence A) is non-ascending by PROB_3:27;
then A7: ( lim (Prob * (Partial_Intersection (superior_setsequence A))) = Prob . (Intersection (Partial_Intersection (superior_setsequence A))) & Prob * (Partial_Intersection (superior_setsequence A)) is convergent ) by PROB_1:def 8;
A8: for A being SetSequence of Sigma
for n, s being Nat holds (Prob * (Partial_Union (A ^\ s))) . n <= (Partial_Sums (Prob * (A ^\ s))) . n

proof

let A be SetSequence of Sigma; :: thesis:
let n, s be Nat; :: thesis:
defpred S₁[ set ] means (Prob * (Partial_Union (A ^\ s))) . $1 <= (Partial_Sums (Prob * (A ^\ s))) . $1;
A9: (Partial_Sums (Prob * (A ^\ s))) . 0 = (Prob * (A ^\ s)) . 0 by SERIES_1:def 1;
dom (Prob * (A ^\ s)) = NAT by FUNCT_2:def 1;
then A11: (Prob * (A ^\ s)) . 0 = Prob . ((A ^\ s) . 0) by FUNCT_1:12;
A12: Prob . ((Partial_Union (A ^\ s)) . 0) = Prob . ((A ^\ s) . 0) by PROB_3:def 2;
dom (Prob * (Partial_Union (A ^\ s))) = NAT by FUNCT_2:def 1;
then A14: S₁[ 0 ] by A12, A11, A9, FUNCT_1:12;
A15: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A16: (Prob * (Partial_Union (A ^\ s))) . k <= (Partial_Sums (Prob * (A ^\ s))) . k ; :: thesis:
A17: dom (Prob * (Partial_Union (A ^\ s))) = NAT by FUNCT_2:def 1;
A18: Prob . (((Partial_Union (A ^\ s)) . k) \/ ((A ^\ s) . (k + 1))) <= (Prob . ((Partial_Union (A ^\ s)) . k)) + (Prob . ((A ^\ s) . (k + 1))) by PROB_1:39;
dom (Prob * (A ^\ s)) = NAT by FUNCT_2:def 1;
then A19: (Prob * (A ^\ s)) . (k + 1) = Prob . ((A ^\ s) . (k + 1)) by FUNCT_1:12;
A20: ( Prob . ((Partial_Union (A ^\ s)) . (k + 1)) <= (Prob . ((Partial_Union (A ^\ s)) . k)) + ((Prob * (A ^\ s)) . (k + 1)) implies (Prob . ((Partial_Union (A ^\ s)) . (k + 1))) - (Prob . ((Partial_Union (A ^\ s)) . k)) <= (Prob * (A ^\ s)) . (k + 1) ) by XREAL_1:20;
A21: ( (Prob . ((Partial_Union (A ^\ s)) . (k + 1))) - ((Prob * (A ^\ s)) . (k + 1)) <= Prob . ((Partial_Union (A ^\ s)) . k) & Prob . ((Partial_Union (A ^\ s)) . k) <= (Partial_Sums (Prob * (A ^\ s))) . k implies (Prob . ((Partial_Union (A ^\ s)) . (k + 1))) - ((Prob * (A ^\ s)) . (k + 1)) <= (Partial_Sums (Prob * (A ^\ s))) . k ) by XXREAL_0:2;
A22: ( (Prob . ((Partial_Union (A ^\ s)) . (k + 1))) - ((Prob * (A ^\ s)) . (k + 1)) <= (Partial_Sums (Prob * (A ^\ s))) . k implies Prob . ((Partial_Union (A ^\ s)) . (k + 1)) <= ((Partial_Sums (Prob * (A ^\ s))) . k) + ((Prob * (A ^\ s)) . (k + 1)) ) by XREAL_1:20;
A23: Prob . ((Partial_Union (A ^\ s)) . (k + 1)) <= (Partial_Sums (Prob * (A ^\ s))) . (k + 1) by A18, A19, A20, A17, A16, A21, A22, FUNCT_1:12, PROB_3:def 2, SERIES_1:def 1, XREAL_1:12, ORDINAL1:def 12;
dom (Prob * (Partial_Union (A ^\ s))) = NAT by FUNCT_2:def 1;
hence S₁[k + 1] by A23, FUNCT_1:12; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A14, A15);
hence (Prob * (Partial_Union (A ^\ s))) . n <= (Partial_Sums (Prob * (A ^\ s))) . n ; :: thesis:

end;

A24: for k being Nat holds Partial_Sums ((Prob * A) ^\ k) is convergent

proof

let k be Nat; :: thesis:
(Prob * A) ^\ k is summable by A2, SERIES_1:12;
hence Partial_Sums ((Prob * A) ^\ k) is convergent by SERIES_1:def 2; :: thesis:

end;

A25: for A being SetSequence of Sigma
for n being Nat holds Prob * (A ^\ n) = (Prob * A) ^\ n

proof

let A be SetSequence of Sigma; :: thesis:
let n be Nat; :: thesis:
for k being Element of NAT holds (Prob * (A ^\ n)) . k = ((Prob * A) ^\ n) . k

proof

let k be Element of NAT ; :: thesis:
dom (Prob * (A ^\ n)) = NAT by FUNCT_2:def 1;
then A26: (Prob * (A ^\ n)) . k = Prob . ((A ^\ n) . k) by FUNCT_1:12;
dom (Prob * A) = NAT by FUNCT_2:def 1;
then A27: Prob . (A . (n + k)) = (Prob * A) . (n + k) by FUNCT_1:12;
(Prob * A) . (k + n) = ((Prob * A) ^\ n) . k by NAT_1:def 3;
hence (Prob * (A ^\ n)) . k = ((Prob * A) ^\ n) . k by A26, A27, NAT_1:def 3; :: thesis:

end;

hence Prob * (A ^\ n) = (Prob * A) ^\ n ; :: thesis:

end;

A28: for n being Nat holds Partial_Sums (Prob * (A ^\ n)) is convergent

proof

let n be Nat; :: thesis:
Partial_Sums (Prob * (A ^\ n)) = Partial_Sums ((Prob * A) ^\ n) by A25;
hence Partial_Sums (Prob * (A ^\ n)) is convergent by A24; :: thesis:

end;

A29: for n being Nat holds lim (Prob * (Partial_Union (A ^\ n))) <= lim (Partial_Sums (Prob * (A ^\ n)))

proof

let n be Nat; :: thesis:
A30: for k being Nat holds (Prob * (Partial_Union (A ^\ n))) . k <= (Partial_Sums (Prob * (A ^\ n))) . k by A8;
A31: Prob * (Partial_Union (A ^\ n)) is convergent by PROB_3:41;
Partial_Sums (Prob * (A ^\ n)) is convergent by A28;
hence lim (Prob * (Partial_Union (A ^\ n))) <= lim (Partial_Sums (Prob * (A ^\ n))) by A31, A30, SEQ_2:18; :: thesis:

end;

A32: for n being Nat holds Prob . (Union (A ^\ n)) <= lim (Partial_Sums (Prob * (A ^\ n)))

proof

let n be Nat; :: thesis:
lim (Prob * (Partial_Union (A ^\ n))) <= lim (Partial_Sums (Prob * (A ^\ n))) by A29;
hence Prob . (Union (A ^\ n)) <= lim (Partial_Sums (Prob * (A ^\ n))) by PROB_3:41; :: thesis:

end;

A33: for n being Nat holds Prob . (Union (A ^\ n)) <= Sum (Prob * (A ^\ n))

proof

let n be Nat; :: thesis:
lim (Partial_Sums (Prob * (A ^\ n))) = Sum (Prob * (A ^\ n)) by SERIES_1:def 3;
hence Prob . (Union (A ^\ n)) <= Sum (Prob * (A ^\ n)) by A32; :: thesis:

end;

A34: for n being Nat holds (Prob * (superior_setsequence A)) . n <= (Sum_Shift_Seq (Prob,A)) . n

proof

let n be Nat; :: thesis:
dom (Prob * (superior_setsequence A)) = NAT by FUNCT_2:def 1;
then A36: (Prob * (superior_setsequence A)) . n = Prob . ((superior_setsequence A) . n) by FUNCT_1:12, ORDINAL1:def 12;
A37: Prob . (Union (A ^\ n)) <= Sum (Prob * (A ^\ n)) by A33;
Sum (Prob * (A ^\ n)) = (Sum_Shift_Seq (Prob,A)) . n by Def11;
hence (Prob * (superior_setsequence A)) . n <= (Sum_Shift_Seq (Prob,A)) . n by Def7, A36, A37; :: thesis:

end;

A38: 0 <= lim (Prob * (Partial_Intersection (superior_setsequence A))) by A7, A3, SEQ_2:17;
A39: ( Sum_Shift_Seq (Prob,A) is convergent implies lim (Prob * (Partial_Intersection (superior_setsequence A))) <= lim (Sum_Shift_Seq (Prob,A)) )

proof

assume A40: Sum_Shift_Seq (Prob,A) is convergent ; :: thesis:
A41: for n being Nat holds (Prob * (Partial_Intersection (superior_setsequence A))) . n <= (Prob * (superior_setsequence A)) . n

proof

end;

lim (Prob * (Partial_Intersection (superior_setsequence A))) <= lim (Sum_Shift_Seq (Prob,A))

proof

for n being Nat holds (Prob * (Partial_Intersection (superior_setsequence A))) . n <= (Sum_Shift_Seq (Prob,A)) . n

proof

let n be Nat; :: thesis:
A47: (Prob * (Partial_Intersection (superior_setsequence A))) . n <= (Prob * (superior_setsequence A)) . n by A41;
(Prob * (superior_setsequence A)) . n <= (Sum_Shift_Seq (Prob,A)) . n by A34;
hence (Prob * (Partial_Intersection (superior_setsequence A))) . n <= (Sum_Shift_Seq (Prob,A)) . n by A47, XXREAL_0:2; :: thesis:

end;

hence lim (Prob * (Partial_Intersection (superior_setsequence A))) <= lim (Sum_Shift_Seq (Prob,A)) by A7, A40, SEQ_2:18; :: thesis:

end;

hence lim (Prob * (Partial_Intersection (superior_setsequence A))) <= lim (Sum_Shift_Seq (Prob,A)) ; :: thesis:

end;

for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds
( 0 = lim (Sum_Shift_Seq (Prob,A)) & Sum_Shift_Seq (Prob,A) is convergent )

proof

let A be SetSequence of Sigma; :: thesis:
assume A50: Partial_Sums (Prob * A) is convergent ; :: thesis:
A52: for n being Nat holds (Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))) = (Partial_Sums (Prob * A)) . n

proof

let n be Nat; :: thesis:
(Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))) = (((Partial_Sums (Prob * A)) . n) + (Sum ((Prob * A) ^\ (n + 1)))) - (Sum ((Prob * A) ^\ (n + 1))) by A50, SERIES_1:15, SERIES_1:def 2;
hence (Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))) = (Partial_Sums (Prob * A)) . n ; :: thesis:

end;

A53: for n, m being Nat holds |.(((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)).| = |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).|

proof

let n, m be Nat; :: thesis:
A54: ((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n) = ((Partial_Sums (Prob * A)) . m) - ((Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1)))) by A52;
((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n) = ((Sum (Prob * A)) - (Sum ((Prob * A) ^\ (m + 1)))) - ((Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1)))) by A52, A54;
then A56: ((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n) = (Sum ((Prob * A) ^\ (n + 1))) - (Sum ((Prob * A) ^\ (m + 1))) ;
A57: for A being SetSequence of Sigma
for n being Element of NAT holds Prob * (A ^\ n) = (Prob * A) ^\ n

proof

let A be SetSequence of Sigma; :: thesis:
let n be Element of NAT ; :: thesis:
for k being Element of NAT holds (Prob * (A ^\ n)) . k = ((Prob * A) ^\ n) . k

proof

let k be Element of NAT ; :: thesis:
dom (Prob * (A ^\ n)) = NAT by FUNCT_2:def 1;
then A58: (Prob * (A ^\ n)) . k = Prob . ((A ^\ n) . k) by FUNCT_1:12;
dom (Prob * A) = NAT by FUNCT_2:def 1;
then A59: Prob . (A . (n + k)) = (Prob * A) . (n + k) by FUNCT_1:12;
(Prob * A) . (k + n) = ((Prob * A) ^\ n) . k by NAT_1:def 3;
hence (Prob * (A ^\ n)) . k = ((Prob * A) ^\ n) . k by A58, A59, NAT_1:def 3; :: thesis:

end;

hence Prob * (A ^\ n) = (Prob * A) ^\ n ; :: thesis:

end;

A60: for n being Nat holds ((Sum_Shift_Seq (Prob,A)) ^\ 1) . n = Sum ((Prob * A) ^\ (n + 1))

proof

let n be Nat; :: thesis:
A61: ((Sum_Shift_Seq (Prob,A)) ^\ 1) . n = (Sum_Shift_Seq (Prob,A)) . (n + 1) by NAT_1:def 3;
(Sum_Shift_Seq (Prob,A)) . (n + 1) = Sum (Prob * (A ^\ (n + 1))) by Def11;
hence ((Sum_Shift_Seq (Prob,A)) ^\ 1) . n = Sum ((Prob * A) ^\ (n + 1)) by A57, A61; :: thesis:

end;

A62: |.(((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)).| = |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m)).|

proof

((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n) = (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (Sum ((Prob * A) ^\ (m + 1))) by A56, A60;
hence |.(((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)).| = |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m)).| by A60; :: thesis:

end;

|.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m)).| = |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).|

proof

per cases ) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) = 0 or 0 < (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) or (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) < 0 ) ;

suppose (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) = 0 ; :: thesis:

hence |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m)).| = |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| ; :: thesis:

end;

suppose 0 < (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) ; :: thesis:

then A63: - 0 > - ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m)) ;
|.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| = - ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)) by A63, ABSVALUE:def 1;
hence |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m)).| = |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| ; :: thesis:

end;

suppose (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) < 0 ; :: thesis:

then |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m)).| = - ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m)) by ABSVALUE:def 1;
hence |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m)).| = |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| ; :: thesis:

end;

hence |.(((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)).| = |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| by A62; :: thesis:

end;

A65: ( ( for sr being Real st 0 < sr holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)).| < sr ) implies for sr being Real st 0 < sr holds
ex n being Nat st
for m being Nat st n <= m holds
|.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| < sr )

proof

assume A66: for sr being Real st 0 < sr holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)).| < sr ; :: thesis:
let sr be Real; :: thesis:
assume A67: 0 < sr ; :: thesis:
consider n being Nat such that
A68: for m being Nat st n <= m holds
|.(((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)).| < sr by A66, A67;
take n ; :: thesis:
let m be Nat; :: thesis:
assume A69: n <= m ; :: thesis:
|.(((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n)).| = |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| by A53;
hence |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| < sr by A68, A69; :: thesis:

end;

A70: ( Partial_Sums (Prob * A) is convergent & (Sum_Shift_Seq (Prob,A)) ^\ 1 is convergent ) by A50, A65, SEQ_4:41;
A71: dom (((Sum_Shift_Seq (Prob,A)) ^\ 1) + (Partial_Sums (Prob * A))) = NAT by FUNCT_2:def 1;
consider B being Real_Sequence such that
A72: B = ((Sum_Shift_Seq (Prob,A)) ^\ 1) + (Partial_Sums (Prob * A)) ;
reconsider SP = Sum (Prob * A) as Element of REAL by XREAL_0:def 1;
set B1 = NAT --> SP;
A74: for n being Nat holds (NAT --> SP) . n = B . n

proof

let n be Nat; :: thesis:
A75: for n being Nat holds ((Sum_Shift_Seq (Prob,A)) ^\ 1) . n = Sum ((Prob * A) ^\ (n + 1))

proof

let n be Nat; :: thesis:
A76: ((Sum_Shift_Seq (Prob,A)) ^\ 1) . n = (Sum_Shift_Seq (Prob,A)) . (n + 1) by NAT_1:def 3;
A77: for A being SetSequence of Sigma
for n being Element of NAT holds Prob * (A ^\ n) = (Prob * A) ^\ n

proof

let A be SetSequence of Sigma; :: thesis:
let n be Element of NAT ; :: thesis:
for k being Element of NAT holds (Prob * (A ^\ n)) . k = ((Prob * A) ^\ n) . k

proof

let k be Element of NAT ; :: thesis:
dom (Prob * (A ^\ n)) = NAT by FUNCT_2:def 1;
then A78: (Prob * (A ^\ n)) . k = Prob . ((A ^\ n) . k) by FUNCT_1:12;
dom (Prob * A) = NAT by FUNCT_2:def 1;
then A79: Prob . (A . (n + k)) = (Prob * A) . (n + k) by FUNCT_1:12;
(Prob * A) . (k + n) = ((Prob * A) ^\ n) . k by NAT_1:def 3;
hence (Prob * (A ^\ n)) . k = ((Prob * A) ^\ n) . k by A78, A79, NAT_1:def 3; :: thesis:

end;

hence Prob * (A ^\ n) = (Prob * A) ^\ n ; :: thesis:

end;

(Sum_Shift_Seq (Prob,A)) . (n + 1) = Sum (Prob * (A ^\ (n + 1))) by Def11;
hence ((Sum_Shift_Seq (Prob,A)) ^\ 1) . n = Sum ((Prob * A) ^\ (n + 1)) by A76, A77; :: thesis:

end;

A81: ((Sum_Shift_Seq (Prob,A)) ^\ 1) . n = Sum ((Prob * A) ^\ (n + 1)) by A75;
Sum (Prob * A) = ((Partial_Sums (Prob * A)) . n) + (Sum ((Prob * A) ^\ (n + 1))) by A50, SERIES_1:15, SERIES_1:def 2;
then (NAT --> SP) . n = ((Partial_Sums (Prob * A)) . n) + (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) by A81, FUNCOP_1:7, ORDINAL1:def 12;
hence (NAT --> SP) . n = B . n by A71, A72, VALUED_1:def 1, ORDINAL1:def 12; :: thesis:

end;

A82: lim (NAT --> SP) = lim B

proof

ex k being Nat st
for n being Nat st k <= n holds
(NAT --> SP) . n = B . n

proof

take 1 ; :: thesis:
thus for n being Nat st 1 <= n holds
(NAT --> SP) . n = B . n by A74; :: thesis:

end;

hence lim (NAT --> SP) = lim B by SEQ_4:19; :: thesis:

end;

A83: Sum (Prob * A) = (NAT --> SP) . 1
.= lim B by A82, SEQ_4:26 ;
lim B = (lim ((Sum_Shift_Seq (Prob,A)) ^\ 1)) + (lim (Partial_Sums (Prob * A))) by A72, A70, SEQ_2:6;
then Sum (Prob * A) = (lim ((Sum_Shift_Seq (Prob,A)) ^\ 1)) + (Sum (Prob * A)) by A83, SERIES_1:def 3;
hence ( 0 = lim (Sum_Shift_Seq (Prob,A)) & Sum_Shift_Seq (Prob,A) is convergent ) by A70, SEQ_4:21, SEQ_4:22; :: thesis:

end;

hence ( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent ) by A5, A7, A38, A39, A1; :: thesis: