let Omega be non empty finite set ; :: thesis: for P being Probability of Trivial-SigmaField Omega
for f being Function of Omega,REAL 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 = (f . (s . n)) * (P . {(s . n)}) ) & Integral (P2M P),f = Sum F )
let P be Probability of Trivial-SigmaField Omega; :: thesis: for f being Function of Omega,REAL 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 = (f . (s . n)) * (P . {(s . n)}) ) & Integral (P2M P),f = Sum F )
let f be Function of Omega,REAL ; :: 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 = (f . (s . n)) * (P . {(s . n)}) ) & Integral (P2M P),f = Sum F )
set Sigma = Trivial-SigmaField Omega;
consider F being FinSequence of REAL such that
P1: ( len F = card Omega & ( for n being Nat st n in dom F holds
F . n = (f . ((canFS Omega) . n)) * (P . {((canFS Omega) . n)}) ) & Integral (P2M P),f = Sum F ) by Lm10A;
set s = canFS Omega;
P3: rng (canFS Omega) = Omega by FUNCT_2:def 3;
len (canFS Omega) = card Omega by UPROOTS:5;
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 = (f . (s . n)) * (P . {(s . n)}) ) & Integral (P2M P),f = Sum F ) by P1, P3; :: thesis: verum