for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds P * FSeq is FinSequence of REAL