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 . () = 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 . () = 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 . () = 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 . () = 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 . () = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent )
A2: Prob * A is summable by ;
A3: for n being Nat holds 0 <= (Prob * ) . n
proof
let n be Nat; :: thesis: 0 <= (Prob * ) . n
A4: dom (Prob * ) = NAT by FUNCT_2:def 1;
n in NAT by ORDINAL1:def 12;
then (Prob * ) . n = Prob . () by ;
hence 0 <= (Prob * ) . n by PROB_1:def 8; :: thesis: verum
end;
A5: Intersection = Intersection () by PROB_3:29;
A6: Partial_Intersection () is non-ascending by PROB_3:27;
A7: ( lim (Prob * ) = Prob . & Prob * is convergent ) by ;
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: 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 S1[ 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 ;
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: S1[ 0 ] by ;
A15: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A16: (Prob * (Partial_Union (A ^\ s))) . k <= (Partial_Sums (Prob * (A ^\ s))) . k ; :: thesis: S1[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 ;
dom (Prob * (Partial_Union (A ^\ s))) = NAT by FUNCT_2:def 1;
hence S1[k + 1] by ; :: thesis: verum
end;
for k being Nat holds S1[k] from hence (Prob * (Partial_Union (A ^\ s))) . n <= (Partial_Sums (Prob * (A ^\ s))) . n ; :: thesis: verum
end;
A24: for k being Nat holds Partial_Sums ((Prob * A) ^\ k) is convergent
proof
let k be Nat; :: thesis: Partial_Sums ((Prob * A) ^\ k) is convergent
(Prob * A) ^\ k is summable by ;
hence Partial_Sums ((Prob * A) ^\ k) is convergent by SERIES_1:def 2; :: thesis: verum
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: 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
proof
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 ; :: thesis: verum
end;
hence Prob * (A ^\ n) = (Prob * A) ^\ n ; :: thesis: verum
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)) 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;
A29: for n being Nat holds lim (Prob * (Partial_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)))
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 ; :: thesis: verum
end;
A32: for n being Nat holds Prob . (Union (A ^\ n)) <= lim (Partial_Sums (Prob * (A ^\ n)))
proof
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;
A33: for n being Nat holds Prob . (Union (A ^\ n)) <= Sum (Prob * (A ^\ n))
proof
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;
A34: for n being Nat holds (Prob * ()) . n <= (Sum_Shift_Seq (Prob,A)) . n
proof
let n be Nat; :: thesis: (Prob * ()) . n <= (Sum_Shift_Seq (Prob,A)) . n
A35: dom (Prob * ()) = NAT by FUNCT_2:def 1;
n in NAT by ORDINAL1:def 12;
then A36: (Prob * ()) . n = Prob . (() . n) by ;
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 * ()) . n <= (Sum_Shift_Seq (Prob,A)) . n by ; :: thesis: verum
end;
A38: 0 <= lim (Prob * ) by ;
A39: ( Sum_Shift_Seq (Prob,A) is convergent implies lim (Prob * ) <= lim (Sum_Shift_Seq (Prob,A)) )
proof
assume A40: Sum_Shift_Seq (Prob,A) is convergent ; :: thesis: lim (Prob * ) <= lim (Sum_Shift_Seq (Prob,A))
A41: for n being Nat holds (Prob * ) . n <= (Prob * ()) . n
proof
let n be Nat; :: thesis: (Prob * ) . n <= (Prob * ()) . n
A42: Prob . () <= Prob . (() . n) by ;
A43: dom (Prob * ) = NAT by FUNCT_2:def 1;
A44: dom (Prob * ()) = NAT by FUNCT_2:def 1;
A45: n in NAT by ORDINAL1:def 12;
(Prob * ()) . n = Prob . (() . n) by ;
hence (Prob * ) . n <= (Prob * ()) . n by ; :: thesis: verum
end;
lim (Prob * ) <= lim (Sum_Shift_Seq (Prob,A))
proof
A46: for n being Nat holds (Prob * ) . n <= (Sum_Shift_Seq (Prob,A)) . n
proof
let n be Nat; :: thesis: (Prob * ) . n <= (Sum_Shift_Seq (Prob,A)) . n
A47: (Prob * ) . n <= (Prob * ()) . n by A41;
A48: (Prob * ()) . n <= (Sum_Shift_Seq (Prob,A)) . n by A34;
thus (Prob * ) . n <= (Sum_Shift_Seq (Prob,A)) . n by ; :: thesis: verum
end;
thus lim (Prob * ) <= lim (Sum_Shift_Seq (Prob,A)) by ; :: thesis: verum
end;
hence lim (Prob * ) <= lim (Sum_Shift_Seq (Prob,A)) ; :: thesis: verum
end;
A49: 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: ( 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
proof
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 ;
hence (Sum (Prob * A)) - (Sum ((Prob * A) ^\ (n + 1))) = (Partial_Sums (Prob * A)) . n ; :: thesis: verum
end;
A53: for n, m being Nat st n <= m 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: ( 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 ;
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
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
proof
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 ; :: thesis: verum
end;
hence Prob * (A ^\ n) = (Prob * A) ^\ n ; :: thesis: verum
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: ((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 ; :: thesis: verum
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 ;
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;
|.((((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 ( (((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 ) ;
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 ;
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 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 ;
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;
end;
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: verum
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: 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 ;
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 ;
hence |.((((Sum_Shift_Seq (Prob,A)) ^\ 1) . m) - (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n)).| < sr by ; :: thesis: verum
end;
A70: ( Partial_Sums (Prob * A) is convergent & (Sum_Shift_Seq (Prob,A)) ^\ 1 is convergent ) by ;
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 ;
A74: for n being Nat holds (NAT --> SP) . n = B . n
proof
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))
proof
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
proof
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
proof
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 ; :: thesis: verum
end;
hence Prob * (A ^\ n) = (Prob * A) ^\ n ; :: thesis: verum
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 ; :: thesis: verum
end;
A80: n in NAT by ORDINAL1:def 12;
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 ;
then (NAT --> SP) . n = ((Partial_Sums (Prob * A)) . n) + (((Sum_Shift_Seq (Prob,A)) ^\ 1) . n) by ;
hence (NAT --> SP) . n = B . n by ; :: thesis: verum
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: 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;
hence lim (NAT --> SP) = lim B by SEQ_4:19; :: thesis: verum
end;
A83: Sum (Prob * A) = (NAT --> SP) . 1
.= lim B by ;
A84: lim B = (lim ((Sum_Shift_Seq (Prob,A)) ^\ 1)) + (lim (Partial_Sums (Prob * A))) by ;
Sum (Prob * A) = (lim ((Sum_Shift_Seq (Prob,A)) ^\ 1)) + (Sum (Prob * A)) by ;
hence ( 0 = lim (Sum_Shift_Seq (Prob,A)) & Sum_Shift_Seq (Prob,A) is convergent ) by ; :: thesis: verum
end;
( lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent ) by ;
hence ( Prob . () = 0 & lim (Sum_Shift_Seq (Prob,A)) = 0 & Sum_Shift_Seq (Prob,A) is convergent ) by ; :: thesis: verum