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 st
( 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 )
let P be Probability of Trivial-SigmaField Omega; :: thesis: for f being Function of Omega,REAL ex F being FinSequence of REAL st
( 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 )
let f be Function of Omega,REAL; :: thesis: ex F being FinSequence of REAL st
( 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 )
set Sigma = Trivial-SigmaField Omega;
set M = P2M P;
A1: P . Omega in REAL by XREAL_0:def 1;
then consider x being FinSequence of ExtREAL such that
A2: len x = card Omega and
A3: for n being Nat st n in dom x holds
x . n = (f . ((canFS Omega) . n)) * ((P2M P) . {((canFS Omega) . n)}) and
A4: Integral ((P2M P),f) = Sum x by Lm10, XXREAL_0:9;
A5: (P2M P) . Omega < +infty by A1, XXREAL_0:9;
A6: for n being Nat st n in dom (canFS Omega) holds
(P2M P) . {((canFS Omega) . n)} in REAL

proof

let n be Nat; :: thesis: ( n in dom (canFS Omega) implies (P2M P) . {((canFS Omega) . n)} in REAL )
assume n in dom (canFS Omega) ; :: thesis: (P2M P) . {((canFS Omega) . n)} in REAL
then (canFS Omega) . n in rng (canFS Omega) by FUNCT_1:3;
then A7: {((canFS Omega) . n)} c= Omega by ZFMISC_1:31;
Omega in Trivial-SigmaField Omega by MEASURE1:7;
hence (P2M P) . {((canFS Omega) . n)} in REAL by A5, A7, Lm7; :: thesis: verum

end;

now :: thesis: for y being object st y in rng x holds
y in REAL

let y be object ; :: thesis: ( y in rng x implies y in REAL )
assume y in rng x ; :: thesis: y in REAL
then consider n being Element of NAT such that
A8: n in dom x and
A9: y = x . n by PARTFUN1:3;
Seg (len x) = Seg (len (canFS Omega)) by A2, FINSEQ_1:93;
then dom x = Seg (len (canFS Omega)) by FINSEQ_1:def 3;
then n in dom (canFS Omega) by A8, FINSEQ_1:def 3;
then reconsider z = (P2M P) . {((canFS Omega) . n)} as Element of REAL by A6;
reconsider w = f . ((canFS Omega) . n) as Element of REAL by XREAL_0:def 1;
x . n = (f . ((canFS Omega) . n)) * ((P2M P) . {((canFS Omega) . n)}) by A3, A8
.= w * z by EXTREAL1:1 ;
hence y in REAL by A9; :: thesis: verum

end;

then rng x c= REAL ;
then reconsider F = x as FinSequence of REAL by FINSEQ_1:def 4;
take F ; :: thesis: ( 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 )
for n being Nat st n in dom F holds
F . n = (f . ((canFS Omega) . n)) * (P . {((canFS Omega) . n)})

proof

let n be Nat; :: thesis: ( n in dom F implies F . n = (f . ((canFS Omega) . n)) * (P . {((canFS Omega) . n)}) )
assume n in dom F ; :: thesis: F . n = (f . ((canFS Omega) . n)) * (P . {((canFS Omega) . n)})
then F . n = (f . ((canFS Omega) . n)) * ((P2M P) . {((canFS Omega) . n)}) by A3;
hence F . n = (f . ((canFS Omega) . n)) * (P . {((canFS Omega) . n)}) by EXTREAL1:1; :: thesis: verum

end;

hence ( 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 A2, A4, MESFUNC3:2; :: thesis: verum