let Omega be non empty set ; 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; 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; 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; 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; (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 S1[ 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:
S1[ 0 ]
by A6, A3, SERIES_1:def 1;
A8:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A9:
(Partial_Sums (Prob * (A ^\ (n1 + 1)))) . k <= ((Partial_Sums (Prob * A)) . ((k + n1) + 1)) - ((Partial_Sums (Prob * A)) . n1)
;
S1[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
S1[
k + 1]
;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A7, A8);
then
S1[n]
;
hence
(Partial_Sums (Prob * (A ^\ (n1 + 1)))) . n <= ((Partial_Sums (Prob * A)) . ((n1 + 1) + n)) - ((Partial_Sums (Prob * A)) . n1)
; verum