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 Partial_Sums (Prob * A) is convergent holds

( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )

let Sigma be SigmaField of Omega; :: thesis: for Prob being Probability of Sigma

for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds

( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )

let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds

( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )

let A be SetSequence of Sigma; :: thesis: ( Partial_Sums (Prob * A) is convergent implies ( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent ) )

assume A1: Partial_Sums (Prob * A) is convergent ; :: thesis: ( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )

A2: Prob * A is summable by A1, SERIES_1:def 2;

A3: for n being Nat holds 0 <= (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n

A6: Partial_Intersection (Union_Shift_Seq A) is non-ascending by PROB_3:27;

A7: ( lim (Prob * (Partial_Intersection (Union_Shift_Seq A))) = Prob . (Intersection (Partial_Intersection (Union_Shift_Seq A))) & Prob * (Partial_Intersection (Union_Shift_Seq A)) is convergent ) by A6, 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

for n being Nat holds Prob * (A ^\ n) = (Prob * A) ^\ n

A39: ( Sum_Shift_Seq (Prob,A) is convergent implies lim (Prob * (Partial_Intersection (Union_Shift_Seq A))) <= lim (Sum_Shift_Seq (Prob,A)) )

( 0 = lim (Sum_Shift_Seq (Prob,A)) & Sum_Shift_Seq (Prob,A) is convergent )

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, PROB_2:def 1; :: thesis: verum

for Prob being Probability of Sigma

for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds

( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )

let Sigma be SigmaField of Omega; :: thesis: for Prob being Probability of Sigma

for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds

( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )

let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds

( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )

let A be SetSequence of Sigma; :: thesis: ( Partial_Sums (Prob * A) is convergent implies ( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent ) )

assume A1: Partial_Sums (Prob * A) is convergent ; :: thesis: ( Prob . (@lim_sup A) = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )

A2: Prob * A is summable by A1, SERIES_1:def 2;

A3: for n being Nat holds 0 <= (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n

proof

A5:
Intersection (Partial_Intersection (Union_Shift_Seq A)) = Intersection (Union_Shift_Seq A)
by PROB_3:29;
let n be Nat; :: thesis: 0 <= (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n

A4: dom (Prob * (Partial_Intersection (Union_Shift_Seq A))) = NAT by FUNCT_2:def 1;

n in NAT by ORDINAL1:def 12;

then (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n = Prob . ((Partial_Intersection (Union_Shift_Seq A)) . n) by A4, FUNCT_1:12;

hence 0 <= (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n by PROB_1:def 8; :: thesis: verum

end;A4: dom (Prob * (Partial_Intersection (Union_Shift_Seq A))) = NAT by FUNCT_2:def 1;

n in NAT by ORDINAL1:def 12;

then (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n = Prob . ((Partial_Intersection (Union_Shift_Seq A)) . n) by A4, FUNCT_1:12;

hence 0 <= (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n by PROB_1:def 8; :: thesis: verum

A6: Partial_Intersection (Union_Shift_Seq A) is non-ascending by PROB_3:27;

A7: ( lim (Prob * (Partial_Intersection (Union_Shift_Seq A))) = Prob . (Intersection (Partial_Intersection (Union_Shift_Seq A))) & Prob * (Partial_Intersection (Union_Shift_Seq A)) is convergent ) by A6, 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

A24:
for k being Nat holds Partial_Sums ((Prob * A) ^\ k) is convergent
let A be SetSequence of Sigma; :: thesis: for n, s being Nat holds (Prob * (Partial_Union (A ^\ s))) . n <= (Partial_Sums (Prob * (A ^\ s))) . n

let n, s be Nat; :: thesis: (Prob * (Partial_Union (A ^\ s))) . n <= (Partial_Sums (Prob * (A ^\ s))) . n

defpred S_{1}[ 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;

A10: dom (Prob * (A ^\ s)) = NAT by FUNCT_2:def 1;

A11: (Prob * (A ^\ s)) . 0 = Prob . ((A ^\ s) . 0) by A10, FUNCT_1:12;

A12: Prob . ((Partial_Union (A ^\ s)) . 0) = Prob . ((A ^\ s) . 0) by PROB_3:def 2;

A13: dom (Prob * (Partial_Union (A ^\ s))) = NAT by FUNCT_2:def 1;

A14: S_{1}[ 0 ]
by A13, A12, A11, A9, FUNCT_1:12;

A15: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A14, A15);

hence (Prob * (Partial_Union (A ^\ s))) . n <= (Partial_Sums (Prob * (A ^\ s))) . n ; :: thesis: verum

end;let n, s be Nat; :: thesis: (Prob * (Partial_Union (A ^\ s))) . n <= (Partial_Sums (Prob * (A ^\ s))) . n

defpred S

A9: (Partial_Sums (Prob * (A ^\ s))) . 0 = (Prob * (A ^\ s)) . 0 by SERIES_1:def 1;

A10: dom (Prob * (A ^\ s)) = NAT by FUNCT_2:def 1;

A11: (Prob * (A ^\ s)) . 0 = Prob . ((A ^\ s) . 0) by A10, FUNCT_1:12;

A12: Prob . ((Partial_Union (A ^\ s)) . 0) = Prob . ((A ^\ s) . 0) by PROB_3:def 2;

A13: dom (Prob * (Partial_Union (A ^\ s))) = NAT by FUNCT_2:def 1;

A14: S

A15: for k being Nat st S

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A16: (Prob * (Partial_Union (A ^\ s))) . k <= (Partial_Sums (Prob * (A ^\ s))) . k ; :: thesis: S_{1}[k + 1]

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;

k in NAT by ORDINAL1:def 12;

then 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;

dom (Prob * (Partial_Union (A ^\ s))) = NAT by FUNCT_2:def 1;

hence S_{1}[k + 1]
by A23, FUNCT_1:12; :: thesis: verum

end;assume A16: (Prob * (Partial_Union (A ^\ s))) . k <= (Partial_Sums (Prob * (A ^\ s))) . k ; :: thesis: S

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;

k in NAT by ORDINAL1:def 12;

then 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;

dom (Prob * (Partial_Union (A ^\ s))) = NAT by FUNCT_2:def 1;

hence S

hence (Prob * (Partial_Union (A ^\ s))) . n <= (Partial_Sums (Prob * (A ^\ s))) . n ; :: thesis: verum

proof

A25:
for A being SetSequence of Sigma
let k be Nat; :: thesis: Partial_Sums ((Prob * A) ^\ k) is convergent

(Prob * A) ^\ k is summable by A2, SERIES_1:12;

hence Partial_Sums ((Prob * A) ^\ k) is convergent by SERIES_1:def 2; :: thesis: verum

end;(Prob * A) ^\ k is summable by A2, SERIES_1:12;

hence Partial_Sums ((Prob * A) ^\ k) is convergent by SERIES_1:def 2; :: thesis: verum

for n being Nat holds Prob * (A ^\ n) = (Prob * A) ^\ n

proof

A28:
for n being Nat holds Partial_Sums (Prob * (A ^\ n)) is convergent
let A be SetSequence of Sigma; :: thesis: for n being Nat holds Prob * (A ^\ n) = (Prob * A) ^\ n

let n be Nat; :: thesis: Prob * (A ^\ n) = (Prob * A) ^\ n

for k being Element of NAT holds (Prob * (A ^\ n)) . k = ((Prob * A) ^\ n) . k

end;let n be Nat; :: thesis: Prob * (A ^\ n) = (Prob * A) ^\ n

for k being Element of NAT holds (Prob * (A ^\ n)) . k = ((Prob * A) ^\ n) . k

proof

hence
Prob * (A ^\ n) = (Prob * A) ^\ n
; :: thesis: verum
let k be Element of NAT ; :: thesis: (Prob * (A ^\ n)) . k = ((Prob * A) ^\ n) . k

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

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

proof

A29:
for n being Nat holds lim (Prob * (Partial_Union (A ^\ n))) <= lim (Partial_Sums (Prob * (A ^\ n)))
let n be Nat; :: thesis: Partial_Sums (Prob * (A ^\ n)) is convergent

Partial_Sums (Prob * (A ^\ n)) = Partial_Sums ((Prob * A) ^\ n) by A25;

hence Partial_Sums (Prob * (A ^\ n)) is convergent by A24; :: thesis: verum

end;Partial_Sums (Prob * (A ^\ n)) = Partial_Sums ((Prob * A) ^\ n) by A25;

hence Partial_Sums (Prob * (A ^\ n)) is convergent by A24; :: thesis: verum

proof

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

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

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

proof

A33:
for n being Nat holds Prob . (Union (A ^\ n)) <= Sum (Prob * (A ^\ n))
let n be Nat; :: thesis: Prob . (Union (A ^\ n)) <= lim (Partial_Sums (Prob * (A ^\ n)))

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

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

proof

A34:
for n being Nat holds (Prob * (Union_Shift_Seq A)) . n <= (Sum_Shift_Seq (Prob,A)) . n
let n be Nat; :: thesis: Prob . (Union (A ^\ n)) <= Sum (Prob * (A ^\ n))

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

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

proof

A38:
0 <= lim (Prob * (Partial_Intersection (Union_Shift_Seq A)))
by A7, A3, SEQ_2:17;
let n be Nat; :: thesis: (Prob * (Union_Shift_Seq A)) . n <= (Sum_Shift_Seq (Prob,A)) . n

A35: dom (Prob * (Union_Shift_Seq A)) = NAT by FUNCT_2:def 1;

n in NAT by ORDINAL1:def 12;

then A36: (Prob * (Union_Shift_Seq A)) . n = Prob . ((Union_Shift_Seq A) . n) by A35, FUNCT_1: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 * (Union_Shift_Seq A)) . n <= (Sum_Shift_Seq (Prob,A)) . n by Def7, A36, A37; :: thesis: verum

end;A35: dom (Prob * (Union_Shift_Seq A)) = NAT by FUNCT_2:def 1;

n in NAT by ORDINAL1:def 12;

then A36: (Prob * (Union_Shift_Seq A)) . n = Prob . ((Union_Shift_Seq A) . n) by A35, FUNCT_1: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 * (Union_Shift_Seq A)) . n <= (Sum_Shift_Seq (Prob,A)) . n by Def7, A36, A37; :: thesis: verum

A39: ( Sum_Shift_Seq (Prob,A) is convergent implies lim (Prob * (Partial_Intersection (Union_Shift_Seq A))) <= lim (Sum_Shift_Seq (Prob,A)) )

proof

A49:
for A being SetSequence of Sigma st Partial_Sums (Prob * A) is convergent holds
assume A40:
Sum_Shift_Seq (Prob,A) is convergent
; :: thesis: lim (Prob * (Partial_Intersection (Union_Shift_Seq A))) <= lim (Sum_Shift_Seq (Prob,A))

A41: for n being Nat holds (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n <= (Prob * (Union_Shift_Seq A)) . n

end;A41: for n being Nat holds (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n <= (Prob * (Union_Shift_Seq A)) . n

proof

lim (Prob * (Partial_Intersection (Union_Shift_Seq A))) <= lim (Sum_Shift_Seq (Prob,A))
let n be Nat; :: thesis: (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n <= (Prob * (Union_Shift_Seq A)) . n

A42: Prob . ((Partial_Intersection (Union_Shift_Seq A)) . n) <= Prob . ((Union_Shift_Seq A) . n) by PROB_1:34, PROB_3:23;

A43: dom (Prob * (Partial_Intersection (Union_Shift_Seq A))) = NAT by FUNCT_2:def 1;

A44: dom (Prob * (Union_Shift_Seq A)) = NAT by FUNCT_2:def 1;

A45: n in NAT by ORDINAL1:def 12;

(Prob * (Union_Shift_Seq A)) . n = Prob . ((Union_Shift_Seq A) . n) by A44, FUNCT_1:12, A45;

hence (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n <= (Prob * (Union_Shift_Seq A)) . n by A43, A42, FUNCT_1:12, A45; :: thesis: verum

end;A42: Prob . ((Partial_Intersection (Union_Shift_Seq A)) . n) <= Prob . ((Union_Shift_Seq A) . n) by PROB_1:34, PROB_3:23;

A43: dom (Prob * (Partial_Intersection (Union_Shift_Seq A))) = NAT by FUNCT_2:def 1;

A44: dom (Prob * (Union_Shift_Seq A)) = NAT by FUNCT_2:def 1;

A45: n in NAT by ORDINAL1:def 12;

(Prob * (Union_Shift_Seq A)) . n = Prob . ((Union_Shift_Seq A) . n) by A44, FUNCT_1:12, A45;

hence (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n <= (Prob * (Union_Shift_Seq A)) . n by A43, A42, FUNCT_1:12, A45; :: thesis: verum

proof

hence
lim (Prob * (Partial_Intersection (Union_Shift_Seq A))) <= lim (Sum_Shift_Seq (Prob,A))
; :: thesis: verum
A46:
for n being Nat holds (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n <= (Sum_Shift_Seq (Prob,A)) . n

end;proof

thus
lim (Prob * (Partial_Intersection (Union_Shift_Seq A))) <= lim (Sum_Shift_Seq (Prob,A))
by A7, A40, A46, SEQ_2:18; :: thesis: verum
let n be Nat; :: thesis: (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n <= (Sum_Shift_Seq (Prob,A)) . n

A47: (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n <= (Prob * (Union_Shift_Seq A)) . n by A41;

A48: (Prob * (Union_Shift_Seq A)) . n <= (Sum_Shift_Seq (Prob,A)) . n by A34;

thus (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n <= (Sum_Shift_Seq (Prob,A)) . n by A47, A48, XXREAL_0:2; :: thesis: verum

end;A47: (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n <= (Prob * (Union_Shift_Seq A)) . n by A41;

A48: (Prob * (Union_Shift_Seq A)) . n <= (Sum_Shift_Seq (Prob,A)) . n by A34;

thus (Prob * (Partial_Intersection (Union_Shift_Seq A))) . n <= (Sum_Shift_Seq (Prob,A)) . n by A47, A48, XXREAL_0:2; :: thesis: verum

( 0 = lim (Sum_Shift_Seq (Prob,A)) & Sum_Shift_Seq (Prob,A) is convergent )

proof

( lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )
by A1, A49;
let A be SetSequence of Sigma; :: thesis: ( Partial_Sums (Prob * A) is convergent implies ( 0 = lim (Sum_Shift_Seq (Prob,A)) & Sum_Shift_Seq (Prob,A) is convergent ) )

assume A50: Partial_Sums (Prob * A) is convergent ; :: thesis: ( 0 = lim (Sum_Shift_Seq (Prob,A)) & Sum_Shift_Seq (Prob,A) is convergent )

then A51: Prob * A is summable by SERIES_1:def 2;

A52: for n being Nat holds (Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))) = (Partial_Sums (Prob * A)) . n

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

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 )

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;

A73: Prob * A is summable by A50, SERIES_1:def 2;

A74: for n being Nat holds (NAT --> SP) . n = B . n

.= lim B by A82, SEQ_4:26 ;

A84: lim B = (lim ((Sum_Shift_Seq (Prob,A)) ^\ 1)) + (lim (Partial_Sums (Prob * A))) by A72, A70, SEQ_2:6;

Sum (Prob * A) = (lim ((Sum_Shift_Seq (Prob,A)) ^\ 1)) + (Sum (Prob * A)) by A83, A84, 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: verum

end;assume A50: Partial_Sums (Prob * A) is convergent ; :: thesis: ( 0 = lim (Sum_Shift_Seq (Prob,A)) & Sum_Shift_Seq (Prob,A) is convergent )

then A51: Prob * A is summable by SERIES_1:def 2;

A52: for n being Nat holds (Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))) = (Partial_Sums (Prob * A)) . n

proof

A53:
for n, m being Nat st n <= m holds
let n be Nat; :: thesis: (Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))) = (Partial_Sums (Prob * A)) . n

(Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))) = (((Partial_Sums (Prob * A)) . n) + (Sum ((Prob * A) ^\ (n + 1)))) - (Sum ((Prob * A) ^\ (n + 1))) by A51, SERIES_1:15;

hence (Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))) = (Partial_Sums (Prob * A)) . n ; :: thesis: verum

end;(Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))) = (((Partial_Sums (Prob * A)) . n) + (Sum ((Prob * A) ^\ (n + 1)))) - (Sum ((Prob * A) ^\ (n + 1))) by A51, SERIES_1:15;

hence (Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))) = (Partial_Sums (Prob * A)) . n ; :: thesis: verum

|.(((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

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

assume 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)).|

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;

A55: ((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;

A56: ((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n) = (Sum ((Prob * A) ^\ (n + 1))) - (Sum ((Prob * A) ^\ (m + 1))) by A55;

A57: for A being SetSequence of Sigma

for n being Element of NAT holds Prob * (A ^\ n) = (Prob * A) ^\ n

end;assume 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)).|

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;

A55: ((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;

A56: ((Partial_Sums (Prob * A)) . m) - ((Partial_Sums (Prob * A)) . n) = (Sum ((Prob * A) ^\ (n + 1))) - (Sum ((Prob * A) ^\ (m + 1))) by A55;

A57: for A being SetSequence of Sigma

for n being Element of NAT holds Prob * (A ^\ n) = (Prob * A) ^\ n

proof

A60:
for n being Nat holds ((Sum_Shift_Seq (Prob,A)) ^\ 1) . n = Sum ((Prob * A) ^\ (n + 1))
let A be SetSequence of Sigma; :: thesis: for n being Element of NAT holds Prob * (A ^\ n) = (Prob * A) ^\ n

let n be Element of NAT ; :: thesis: Prob * (A ^\ n) = (Prob * A) ^\ n

for k being Element of NAT holds (Prob * (A ^\ n)) . k = ((Prob * A) ^\ n) . k

end;let n be Element of NAT ; :: thesis: Prob * (A ^\ n) = (Prob * A) ^\ n

for k being Element of NAT holds (Prob * (A ^\ n)) . k = ((Prob * A) ^\ n) . k

proof

hence
Prob * (A ^\ n) = (Prob * A) ^\ n
; :: thesis: verum
let k be Element of NAT ; :: thesis: (Prob * (A ^\ n)) . k = ((Prob * A) ^\ n) . k

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

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

proof

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)).|
let n be Nat; :: thesis: ((Sum_Shift_Seq (Prob,A)) ^\ 1) . n = Sum ((Prob * A) ^\ (n + 1))

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

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

proof

|.((((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)).|
((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: verum

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

proof
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: verumper cases
( (((Sum_Shift_Seq (Prob,A)) ^\ 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 )
;

end;

suppose
(((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) = 0
; :: thesis: |.((((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)).|

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

end;suppose
0 < (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m)
; :: thesis: |.((((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)).|

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

end;|.((((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: verum

suppose A64:
(((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) < 0
; :: thesis: |.((((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) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m)).| = - ((((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . m))
by A64, 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: verum

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

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

A70:
( Partial_Sums (Prob * A) is convergent & (Sum_Shift_Seq (Prob,A)) ^\ 1 is convergent )
by A50, A65, SEQ_4:41;
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: 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

let sr be Real; :: thesis: ( 0 < sr implies 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 )

assume A67: 0 < sr ; :: thesis: 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

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: for m being Nat st n <= m holds

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

let m be Nat; :: thesis: ( n <= m implies |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| < sr )

assume A69: n <= m ; :: thesis: |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| < sr

|.(((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 A69, A53;

hence |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| < sr by A68, A69; :: thesis: verum

end;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: 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

let sr be Real; :: thesis: ( 0 < sr implies 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 )

assume A67: 0 < sr ; :: thesis: 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

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: for m being Nat st n <= m holds

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

let m be Nat; :: thesis: ( n <= m implies |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| < sr )

assume A69: n <= m ; :: thesis: |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| < sr

|.(((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 A69, A53;

hence |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| < sr by A68, A69; :: thesis: verum

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;

A73: Prob * A is summable by A50, SERIES_1:def 2;

A74: for n being Nat holds (NAT --> SP) . n = B . n

proof

A82:
lim (NAT --> SP) = lim B
let n be Nat; :: thesis: (NAT --> SP) . n = B . n

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

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 A73, SERIES_1:15;

then (NAT --> SP) . n = ((Partial_Sums (Prob * A)) . n) + (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) by A81, FUNCOP_1:7, A80;

hence (NAT --> SP) . n = B . n by A71, A72, VALUED_1:def 1, A80; :: thesis: verum

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

proof

A80:
n in NAT
by ORDINAL1:def 12;
let n be Nat; :: thesis: ((Sum_Shift_Seq (Prob,A)) ^\ 1) . n = Sum ((Prob * A) ^\ (n + 1))

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

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

end;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

(Sum_Shift_Seq (Prob,A)) . (n + 1) = Sum (Prob * (A ^\ (n + 1)))
by Def11;
let A be SetSequence of Sigma; :: thesis: for n being Element of NAT holds Prob * (A ^\ n) = (Prob * A) ^\ n

let n be Element of NAT ; :: thesis: Prob * (A ^\ n) = (Prob * A) ^\ n

for k being Element of NAT holds (Prob * (A ^\ n)) . k = ((Prob * A) ^\ n) . k

end;let n be Element of NAT ; :: thesis: Prob * (A ^\ n) = (Prob * A) ^\ n

for k being Element of NAT holds (Prob * (A ^\ n)) . k = ((Prob * A) ^\ n) . k

proof

hence
Prob * (A ^\ n) = (Prob * A) ^\ n
; :: thesis: verum
let k be Element of NAT ; :: thesis: (Prob * (A ^\ n)) . k = ((Prob * A) ^\ n) . k

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

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

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

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 A73, SERIES_1:15;

then (NAT --> SP) . n = ((Partial_Sums (Prob * A)) . n) + (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) by A81, FUNCOP_1:7, A80;

hence (NAT --> SP) . n = B . n by A71, A72, VALUED_1:def 1, A80; :: thesis: verum

proof

A83: Sum (Prob * A) =
(NAT --> SP) . 1
ex k being Nat st

for n being Nat st k <= n holds

(NAT --> SP) . n = B . n

end;for n being Nat st k <= n holds

(NAT --> SP) . n = B . n

proof

hence
lim (NAT --> SP) = lim B
by SEQ_4:19; :: thesis: verum
take
1
; :: thesis: for n being Nat st 1 <= n holds

(NAT --> SP) . n = B . n

thus for n being Nat st 1 <= n holds

(NAT --> SP) . n = B . n by A74; :: thesis: verum

end;(NAT --> SP) . n = B . n

thus for n being Nat st 1 <= n holds

(NAT --> SP) . n = B . n by A74; :: thesis: verum

.= lim B by A82, SEQ_4:26 ;

A84: lim B = (lim ((Sum_Shift_Seq (Prob,A)) ^\ 1)) + (lim (Partial_Sums (Prob * A))) by A72, A70, SEQ_2:6;

Sum (Prob * A) = (lim ((Sum_Shift_Seq (Prob,A)) ^\ 1)) + (Sum (Prob * A)) by A83, A84, 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: verum

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, PROB_2:def 1; :: thesis: verum