let Omega be non empty finite set ; :: thesis: for P being Probability of Trivial-SigmaField Omega
for f being Function of Omega,REAL
for x being FinSequence of REAL
for s being FinSequence of Omega st len x = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom x holds
x . n = (f . (s . n)) * (P . {(s . n)}) ) holds
Integral (P2M P),f = Sum x
let P be Probability of Trivial-SigmaField Omega; :: thesis: for f being Function of Omega,REAL
for x being FinSequence of REAL
for s being FinSequence of Omega st len x = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom x holds
x . n = (f . (s . n)) * (P . {(s . n)}) ) holds
Integral (P2M P),f = Sum x
let f be Function of Omega,REAL ; :: thesis: for x being FinSequence of REAL
for s being FinSequence of Omega st len x = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom x holds
x . n = (f . (s . n)) * (P . {(s . n)}) ) holds
Integral (P2M P),f = Sum x
let x be FinSequence of REAL ; :: thesis: for s being FinSequence of Omega st len x = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom x holds
x . n = (f . (s . n)) * (P . {(s . n)}) ) holds
Integral (P2M P),f = Sum x
let s be FinSequence of Omega; :: thesis: ( len x = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom x holds
x . n = (f . (s . n)) * (P . {(s . n)}) ) implies Integral (P2M P),f = Sum x )
assume that
AS: ( len x = card Omega & s is one-to-one & rng s = Omega & len s = card Omega ) and
ASt: for n being Nat st n in dom x holds
x . n = (f . (s . n)) * (P . {(s . n)}) ; :: thesis: Integral (P2M P),f = Sum x
set Sigma = Trivial-SigmaField Omega;
AA1: P . Omega in REAL ;
rng x c= ExtREAL by NUMBERS:31, XBOOLE_1:1;
then reconsider x1 = x as FinSequence of ExtREAL by FINSEQ_1:def 4;
set M = P2M P;

AA2: now

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

end;

Integral (P2M P),f = Sum x1 by AA1, AA2, AS, Lm9A3, XXREAL_0:9
.= Sum x by MESFUNC3:2 ;
hence Integral (P2M P),f = Sum x ; :: thesis: verum