theorem :: RANDOM_1:5

for Omega being non empty finite set
for f being PartFunc of Omega,REAL ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex s being FinSequence of dom f st
( dom f = union (rng F) & dom F = dom s & s is one-to-one & rng s = dom f & len s = card (dom f) & ( for k being Nat st k in dom F holds
F . k = {(s . k)} ) & ( for n being Nat
for x, y being Element of Omega st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) )