theorem :: RANDOM_1:34

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