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 n1, n being Element of 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 n1, n being Element of 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 n1, n being Element of 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 n1, n being Element of NAT holds (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . n <= ((Partial_Sums (Prob * A)) . ((n1 + 1) + n)) - ((Partial_Sums (Prob * A)) . n1)
let n1, n be Element of 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₁[ Element of 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₁[ 0 ] by A6, A3, SERIES_1:def 1;
A8: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[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₁[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₁[k + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A7, A8);
then S₁[n] ;
hence (Partial_Sums (Prob * (A ^\ (n1 + 1)))) . n <= ((Partial_Sums (Prob * A)) . ((n1 + 1) + n)) - ((Partial_Sums (Prob * A)) . n1) ; :: thesis: verum