let Omega be non empty finite set ; :: thesis: for M being sigma_Measure of (Trivial-SigmaField Omega)
for f being Function of Omega,REAL st M . Omega < +infty holds
ex x being FinSequence of ExtREAL ex 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)) * (M . {(s . n)}) ) & Integral (M,f) = Sum x )
let M be sigma_Measure of (Trivial-SigmaField Omega); :: thesis: for f being Function of Omega,REAL st M . Omega < +infty holds
ex x being FinSequence of ExtREAL ex 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)) * (M . {(s . n)}) ) & Integral (M,f) = Sum x )
let f be Function of Omega,REAL; :: thesis: ( M . Omega < +infty implies ex x being FinSequence of ExtREAL ex 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)) * (M . {(s . n)}) ) & Integral (M,f) = Sum x ) )
set s = canFS Omega;
assume M . Omega < +infty ; :: thesis: ex x being FinSequence of ExtREAL ex 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)) * (M . {(s . n)}) ) & Integral (M,f) = Sum x )
then A1: ex x being FinSequence of ExtREAL st
( len x = card Omega & ( for n being Nat st n in dom x holds
x . n = (f . ((canFS Omega) . n)) * (M . {((canFS Omega) . n)}) ) & Integral (M,f) = Sum x ) by Lm10;
( rng (canFS Omega) = Omega & len (canFS Omega) = card Omega ) by FINSEQ_1:93, FUNCT_2:def 3;
hence ex x being FinSequence of ExtREAL ex 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)) * (M . {(s . n)}) ) & Integral (M,f) = Sum x ) by A1; :: thesis: verum