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
A1: ( len x = card Omega & s is one-to-one & rng s = Omega & len s = card Omega ) and
A2: 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 M = P2M P;
rng x c= ExtREAL by NUMBERS:31;
then reconsider x1 = x as FinSequence of ExtREAL by FINSEQ_1:def 4;
A3: for n being Nat st n in dom x1 holds
x1 . n = (f . (s . n)) * ((P2M P) . {(s . n)})

proof

let n be Nat; :: thesis: ( n in dom x1 implies x1 . n = (f . (s . n)) * ((P2M P) . {(s . n)}) )
assume n in dom x1 ; :: thesis: x1 . n = (f . (s . n)) * ((P2M P) . {(s . n)})
then x1 . n = (f . (s . n)) * (P . {(s . n)}) by A2;
hence x1 . n = (f . (s . n)) * ((P2M P) . {(s . n)}) by EXTREAL1:1; :: thesis: verum

end;

P . Omega in REAL by XREAL_0:def 1;
then Integral ((P2M P),f) = Sum x1 by A1, A3, Th10, XXREAL_0:9
.= Sum x by MESFUNC3:2 ;
hence Integral ((P2M P),f) = Sum x ; :: thesis: verum