:: deftheorem Def11 defines Sum_Shift_Seq BOR_CANT:def 11 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma
for b₅ being Real_Sequence holds
( b₅ = Sum_Shift_Seq (Prob,A) iff for n being Nat holds b₅ . n = Sum (Prob * (A ^\ n)) );