for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )