theorem Th9: :: RANDOM_1:9

for Omega being non empty finite set
for M being sigma_Measure of (Trivial-SigmaField Omega)
for f being Function of Omega,REAL
for x being FinSequence of ExtREAL
for s being FinSequence of Omega st s is one-to-one & rng s = Omega holds
ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex a being FinSequence of REAL st
( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( 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 ) )