theorem :: RANDOM_1:35

for Omega being non empty finite set
for X being Real-Valued-Random-Variable of (Trivial-SigmaField Omega) ex G being FinSequence of REAL ex 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) ) & expect (X,(Trivial-Probability Omega)) = (Sum G) / (card Omega) )