:: deftheorem defines are_Re-presentation_of MESFUNC3:def 1 :
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 holds
( F,a are_Re-presentation_of f iff ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being object st x in F . n holds
f . x = a . n ) ) );