let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds Partial_Sums (P * ASeq) is non-decreasing

let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds Partial_Sums (P * ASeq) is non-decreasing

let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma holds Partial_Sums (P * ASeq) is non-decreasing

let P be Probability of Sigma; :: thesis: Partial_Sums (P * ASeq) is non-decreasing

for n being Nat holds (P * ASeq) . n >= 0 by Th4;

hence Partial_Sums (P * ASeq) is non-decreasing by SERIES_1:16; :: thesis: verum

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds Partial_Sums (P * ASeq) is non-decreasing

let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds Partial_Sums (P * ASeq) is non-decreasing

let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma holds Partial_Sums (P * ASeq) is non-decreasing

let P be Probability of Sigma; :: thesis: Partial_Sums (P * ASeq) is non-decreasing

for n being Nat holds (P * ASeq) . n >= 0 by Th4;

hence Partial_Sums (P * ASeq) is non-decreasing by SERIES_1:16; :: thesis: verum