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 = (R_EAL (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 = (R_EAL (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 = (R_EAL (f . (s . n))) * (M . {(s . n)}) ) & Integral M,f = Sum x ) )
assume AS: 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 = (R_EAL (f . (s . n))) * (M . {(s . n)}) ) & Integral M,f = Sum x )
set Sigma = Trivial-SigmaField Omega;
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))) * (M . {((canFS Omega) . n)}) ) & Integral M,f = Sum x ) by AS, Lm9A;
set s = canFS Omega;
P3: rng (canFS Omega) = Omega by FUNCT_2:def 3;
P4: len (canFS Omega) = card Omega by UPROOTS:5;
reconsider s = canFS Omega as FinSequence of Omega ;
thus 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 = (R_EAL (f . (s . n))) * (M . {(s . n)}) ) & Integral M,f = Sum x ) by P1, P3, P4; :: thesis: verum