for Omega being non empty finite set
for P being Probability of Trivial-SigmaField Omega
for Y being non empty finite Subset of Omega
for f being Function of Omega,REAL ex G being FinSequence of REAL ex s being FinSequence of Y st
( len G = card Y & s is one-to-one & rng s = Y & len s = card Y & ( for n being Nat st n in dom G holds
G . n = (f . (s . n)) * (P . {(s . n)}) ) & Integral ((P2M P),(f | Y)) = Sum G )