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;
PAA1: P . Omega in REAL ;
then AA1: (P2M P) . Omega < +infty by XXREAL_0:9;
consider x being FinSequence of ExtREAL such that
P1: ( len x = card Omega & ( for n being Nat st n in dom x holds
x . n = (R_EAL (f . ((canFS Omega) . n))) * ((P2M P) . {((canFS Omega) . n)}) ) & Integral (P2M P),f = Sum x ) by Lm9A, PAA1, XXREAL_0:9;
set M = P2M P;
CFSD: 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:12;
then B1: {((canFS Omega) . n)} c= Omega by ZFMISC_1:37;
Omega in Trivial-SigmaField Omega by MEASURE1:21;
hence (P2M P) . {((canFS Omega) . n)} in REAL by Lm9A2, B1, AA1; :: thesis: verum

end;

x is FinSequence of REAL

proof

now

let y be set ; :: 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
C71: ( n in dom x & y = x . n ) by PARTFUN1:26;
reconsider w = f . ((canFS Omega) . n) as Element of REAL ;
Seg (len x) = Seg (len (canFS Omega)) by P1, UPROOTS:5;
then dom x = Seg (len (canFS Omega)) by FINSEQ_1:def 3;
then n in dom (canFS Omega) by FINSEQ_1:def 3, C71;
then reconsider z = (P2M P) . {((canFS Omega) . n)} as Element of REAL by CFSD;
x . n = (R_EAL (f . ((canFS Omega) . n))) * ((P2M P) . {((canFS Omega) . n)}) by P1, C71
.= w * z by EXTREAL1:13 ;
hence y in REAL by C71; :: thesis: verum

end;

hence rng x c= REAL by TARSKI:def 3; :: according to FINSEQ_1:def 4 :: thesis: verum

end;

then reconsider F = x as FinSequence of REAL ;
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 )

P2: now

let n be Nat; :: thesis: ( n in dom F implies F . n = (f . ((canFS Omega) . n)) * (P . {((canFS Omega) . n)}) )
assume P21: n in dom F ; :: thesis: F . n = (f . ((canFS Omega) . n)) * (P . {((canFS Omega) . n)})
thus F . n = (R_EAL (f . ((canFS Omega) . n))) * ((P2M P) . {((canFS Omega) . n)}) by P21, P1
.= (f . ((canFS Omega) . n)) * (P . {((canFS Omega) . n)}) by EXTREAL1:13 ; :: thesis: verum

end;

thus ( 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 P1, P2, MESFUNC3:2; :: thesis: verum