theorem Th12: :: RANDOM_1:12

for Omega being non empty finite set
for P being Probability of Trivial-SigmaField Omega
for f being Function of Omega,REAL
for x being FinSequence of REAL
for s being FinSequence of Omega st len x = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom x holds
x . n = (f . (s . n)) * (P . {(s . n)}) ) holds
Integral ((P2M P),f) = Sum x