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)
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
let P be Probability of Trivial-SigmaField Omega; :: thesis: 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
let X be Real-Valued-Random-Variable of (Trivial-SigmaField Omega); :: thesis: 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
let F be FinSequence of REAL ; :: thesis: 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
let s be FinSequence of Omega; :: thesis: ( 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)}) ) implies expect (X,P) = Sum F )
assume ( 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)}) ) ) ; :: thesis: expect (X,P) = Sum F
then Integral ((P2M P),X) = Sum F by Th12;
hence expect (X,P) = Sum F by Def4, Th30; :: thesis: verum