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

for n, n1 being Nat holds (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . n <= ((Partial_Sums (Prob * A)) . ((n1 + 1) + n)) - ((Partial_Sums (Prob * A)) . n1)

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

for A being SetSequence of Sigma

for n, n1 being Nat holds (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . n <= ((Partial_Sums (Prob * A)) . ((n1 + 1) + n)) - ((Partial_Sums (Prob * A)) . n1)

let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma

for n, n1 being Nat holds (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . n <= ((Partial_Sums (Prob * A)) . ((n1 + 1) + n)) - ((Partial_Sums (Prob * A)) . n1)

let A be SetSequence of Sigma; :: thesis: for n, n1 being Nat holds (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . n <= ((Partial_Sums (Prob * A)) . ((n1 + 1) + n)) - ((Partial_Sums (Prob * A)) . n1)

let n, n1 be Nat; :: thesis: (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . n <= ((Partial_Sums (Prob * A)) . ((n1 + 1) + n)) - ((Partial_Sums (Prob * A)) . n1)

A1: dom (Prob * (A ^\ (n1 + 1))) = NAT by FUNCT_2:def 1;

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

defpred S_{1}[ Nat] means (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . $1 <= ((Partial_Sums (Prob * A)) . (($1 + n1) + 1)) - ((Partial_Sums (Prob * A)) . n1);

A3: ((Partial_Sums (Prob * A)) . (n1 + 1)) - ((Partial_Sums (Prob * A)) . n1) = (((Partial_Sums (Prob * A)) . n1) + ((Prob * A) . (n1 + 1))) - ((Partial_Sums (Prob * A)) . n1) by SERIES_1:def 1;

A4: Prob . ((A ^\ (n1 + 1)) . 0) = Prob . (A . ((n1 + 1) + 0)) by NAT_1:def 3;

A5: Prob . (A . (n1 + 1)) = (Prob * A) . (n1 + 1) by A2, FUNCT_1:12;

A6: (Prob * (A ^\ (n1 + 1))) . 0 = (Prob * A) . (n1 + 1) by A1, A4, A5, FUNCT_1:12;

A7: S_{1}[ 0 ]
by A6, A3, SERIES_1:def 1;

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

S_{1}[k + 1]
_{1}[n]
from NAT_1:sch 2(A7, A8);

then S_{1}[n]
;

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

for Prob being Probability of Sigma

for A being SetSequence of Sigma

for n, n1 being Nat holds (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . n <= ((Partial_Sums (Prob * A)) . ((n1 + 1) + n)) - ((Partial_Sums (Prob * A)) . n1)

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

for A being SetSequence of Sigma

for n, n1 being Nat holds (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . n <= ((Partial_Sums (Prob * A)) . ((n1 + 1) + n)) - ((Partial_Sums (Prob * A)) . n1)

let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma

for n, n1 being Nat holds (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . n <= ((Partial_Sums (Prob * A)) . ((n1 + 1) + n)) - ((Partial_Sums (Prob * A)) . n1)

let A be SetSequence of Sigma; :: thesis: for n, n1 being Nat holds (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . n <= ((Partial_Sums (Prob * A)) . ((n1 + 1) + n)) - ((Partial_Sums (Prob * A)) . n1)

let n, n1 be Nat; :: thesis: (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . n <= ((Partial_Sums (Prob * A)) . ((n1 + 1) + n)) - ((Partial_Sums (Prob * A)) . n1)

A1: dom (Prob * (A ^\ (n1 + 1))) = NAT by FUNCT_2:def 1;

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

defpred S

A3: ((Partial_Sums (Prob * A)) . (n1 + 1)) - ((Partial_Sums (Prob * A)) . n1) = (((Partial_Sums (Prob * A)) . n1) + ((Prob * A) . (n1 + 1))) - ((Partial_Sums (Prob * A)) . n1) by SERIES_1:def 1;

A4: Prob . ((A ^\ (n1 + 1)) . 0) = Prob . (A . ((n1 + 1) + 0)) by NAT_1:def 3;

A5: Prob . (A . (n1 + 1)) = (Prob * A) . (n1 + 1) by A2, FUNCT_1:12;

A6: (Prob * (A ^\ (n1 + 1))) . 0 = (Prob * A) . (n1 + 1) by A1, A4, A5, FUNCT_1:12;

A7: S

A8: for k being Nat st S

S

proof

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

assume A9: (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . k <= ((Partial_Sums (Prob * A)) . ((k + n1) + 1)) - ((Partial_Sums (Prob * A)) . n1) ; :: thesis: S_{1}[k + 1]

A10: ((Partial_Sums (Prob * (A ^\ (n1 + 1)))) . k) + ((Prob * (A ^\ (n1 + 1))) . (k + 1)) <= (((Partial_Sums (Prob * A)) . ((k + n1) + 1)) - ((Partial_Sums (Prob * A)) . n1)) + ((Prob * (A ^\ (n1 + 1))) . (k + 1)) by A9, XREAL_1:6;

A11: (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . (k + 1) <= (((Partial_Sums (Prob * A)) . ((k + n1) + 1)) - ((Partial_Sums (Prob * A)) . n1)) + ((Prob * (A ^\ (n1 + 1))) . (k + 1)) by A10, SERIES_1:def 1;

A12: ((Partial_Sums (Prob * (A ^\ (n1 + 1)))) . (k + 1)) + ((Partial_Sums (Prob * A)) . n1) <= ((((Partial_Sums (Prob * A)) . ((k + n1) + 1)) + ((Prob * (A ^\ (n1 + 1))) . (k + 1))) - ((Partial_Sums (Prob * A)) . n1)) + ((Partial_Sums (Prob * A)) . n1) by A11, XREAL_1:6;

A13: (((Partial_Sums (Prob * (A ^\ (n1 + 1)))) . (k + 1)) + ((Partial_Sums (Prob * A)) . n1)) - ((Partial_Sums (Prob * A)) . ((k + n1) + 1)) <= (((Prob * (A ^\ (n1 + 1))) . (k + 1)) + ((Partial_Sums (Prob * A)) . ((k + n1) + 1))) - ((Partial_Sums (Prob * A)) . ((k + n1) + 1)) by A12, XREAL_1:9;

A14: (A ^\ (n1 + 1)) . (k + 1) = A . ((n1 + 1) + (k + 1)) by NAT_1:def 3;

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

A16: dom (Prob * (A ^\ (n1 + 1))) = NAT by FUNCT_2:def 1;

A17: Prob . ((A ^\ (n1 + 1)) . (k + 1)) = (Prob * (A ^\ (n1 + 1))) . (k + 1) by A16, FUNCT_1:12;

A18: (((Partial_Sums (Prob * (A ^\ (n1 + 1)))) . (k + 1)) + ((Partial_Sums (Prob * A)) . n1)) - ((Partial_Sums (Prob * A)) . ((k + n1) + 1)) <= (Prob * A) . ((n1 + k) + 2) by A13, A17, A14, A15, FUNCT_1:12;

A19: ((((Partial_Sums (Prob * (A ^\ (n1 + 1)))) . (k + 1)) + ((Partial_Sums (Prob * A)) . n1)) - ((Partial_Sums (Prob * A)) . ((k + n1) + 1))) + ((Partial_Sums (Prob * A)) . ((k + n1) + 1)) <= ((Prob * A) . ((n1 + k) + 2)) + ((Partial_Sums (Prob * A)) . ((k + n1) + 1)) by A18, XREAL_1:6;

A20: (Partial_Sums (Prob * A)) . (((k + n1) + 1) + 1) = ((Partial_Sums (Prob * A)) . ((k + n1) + 1)) + ((Prob * A) . (((k + n1) + 1) + 1)) by SERIES_1:def 1;

(((Partial_Sums (Prob * (A ^\ (n1 + 1)))) . (k + 1)) + ((Partial_Sums (Prob * A)) . n1)) - ((Partial_Sums (Prob * A)) . n1) <= ((Partial_Sums (Prob * A)) . ((k + n1) + 2)) - ((Partial_Sums (Prob * A)) . n1) by A19, A20, XREAL_1:9;

hence S_{1}[k + 1]
; :: thesis: verum

end;assume A9: (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . k <= ((Partial_Sums (Prob * A)) . ((k + n1) + 1)) - ((Partial_Sums (Prob * A)) . n1) ; :: thesis: S

A10: ((Partial_Sums (Prob * (A ^\ (n1 + 1)))) . k) + ((Prob * (A ^\ (n1 + 1))) . (k + 1)) <= (((Partial_Sums (Prob * A)) . ((k + n1) + 1)) - ((Partial_Sums (Prob * A)) . n1)) + ((Prob * (A ^\ (n1 + 1))) . (k + 1)) by A9, XREAL_1:6;

A11: (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . (k + 1) <= (((Partial_Sums (Prob * A)) . ((k + n1) + 1)) - ((Partial_Sums (Prob * A)) . n1)) + ((Prob * (A ^\ (n1 + 1))) . (k + 1)) by A10, SERIES_1:def 1;

A12: ((Partial_Sums (Prob * (A ^\ (n1 + 1)))) . (k + 1)) + ((Partial_Sums (Prob * A)) . n1) <= ((((Partial_Sums (Prob * A)) . ((k + n1) + 1)) + ((Prob * (A ^\ (n1 + 1))) . (k + 1))) - ((Partial_Sums (Prob * A)) . n1)) + ((Partial_Sums (Prob * A)) . n1) by A11, XREAL_1:6;

A13: (((Partial_Sums (Prob * (A ^\ (n1 + 1)))) . (k + 1)) + ((Partial_Sums (Prob * A)) . n1)) - ((Partial_Sums (Prob * A)) . ((k + n1) + 1)) <= (((Prob * (A ^\ (n1 + 1))) . (k + 1)) + ((Partial_Sums (Prob * A)) . ((k + n1) + 1))) - ((Partial_Sums (Prob * A)) . ((k + n1) + 1)) by A12, XREAL_1:9;

A14: (A ^\ (n1 + 1)) . (k + 1) = A . ((n1 + 1) + (k + 1)) by NAT_1:def 3;

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

A16: dom (Prob * (A ^\ (n1 + 1))) = NAT by FUNCT_2:def 1;

A17: Prob . ((A ^\ (n1 + 1)) . (k + 1)) = (Prob * (A ^\ (n1 + 1))) . (k + 1) by A16, FUNCT_1:12;

A18: (((Partial_Sums (Prob * (A ^\ (n1 + 1)))) . (k + 1)) + ((Partial_Sums (Prob * A)) . n1)) - ((Partial_Sums (Prob * A)) . ((k + n1) + 1)) <= (Prob * A) . ((n1 + k) + 2) by A13, A17, A14, A15, FUNCT_1:12;

A19: ((((Partial_Sums (Prob * (A ^\ (n1 + 1)))) . (k + 1)) + ((Partial_Sums (Prob * A)) . n1)) - ((Partial_Sums (Prob * A)) . ((k + n1) + 1))) + ((Partial_Sums (Prob * A)) . ((k + n1) + 1)) <= ((Prob * A) . ((n1 + k) + 2)) + ((Partial_Sums (Prob * A)) . ((k + n1) + 1)) by A18, XREAL_1:6;

A20: (Partial_Sums (Prob * A)) . (((k + n1) + 1) + 1) = ((Partial_Sums (Prob * A)) . ((k + n1) + 1)) + ((Prob * A) . (((k + n1) + 1) + 1)) by SERIES_1:def 1;

(((Partial_Sums (Prob * (A ^\ (n1 + 1)))) . (k + 1)) + ((Partial_Sums (Prob * A)) . n1)) - ((Partial_Sums (Prob * A)) . n1) <= ((Partial_Sums (Prob * A)) . ((k + n1) + 2)) - ((Partial_Sums (Prob * A)) . n1) by A19, A20, XREAL_1:9;

hence S

then S

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