for Omega being set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Function of Sigma,REAL holds P * ASeq is Real_Sequence