:: deftheorem Def9 defines -Probability_sequence-like RANDOM_3:def 9 :
for D being non-empty ManySortedSet of NAT
for S being SigmaField_sequence of D
for M being ManySortedSet of NAT holds
( M is S -Probability_sequence-like iff for n being Nat holds M . n is Probability of S . n );