let Omega be non empty finite set ; :: thesis: for P being Probability of Trivial-SigmaField Omega
for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega ex F being FinSequence of REAL ex 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)}) ) & expect X,P = Sum F )
let P be Probability of Trivial-SigmaField Omega; :: thesis: for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega ex F being FinSequence of REAL ex 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)}) ) & expect X,P = Sum F )
let X be Real-Valued-Random-Variable of Trivial-SigmaField Omega; :: thesis: ex F being FinSequence of REAL ex 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)}) ) & expect X,P = Sum F )
set M = P2M P;
P1: X is_integrable_on P by LMTX3;
ex F being FinSequence of REAL ex 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)}) ) & Integral (P2M P),X = Sum F ) by LMTX2;
hence ex F being FinSequence of REAL ex 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)}) ) & expect X,P = Sum F ) by def2, P1; :: thesis: verum