theorem Th31: :: RANDOM_1:31

for Omega being non empty finite set
for P being Probability of Trivial-SigmaField Omega
for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega
for F being FinSequence of REAL
for s being FinSequence of Omega st len F = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom F holds
F . n = (X . (s . n)) * (P . {(s . n)}) ) holds
expect (X,P) = Sum F