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 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; :: thesis: ( 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) ; :: thesis: 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] ; :: thesis: 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) ; :: thesis: verum