:: deftheorem defines are_Re-presentation_of MESFUN7C:def 14 :
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for F being Finite_Sep_Sequence of S
for a being FinSequence of REAL 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 set st x in F . n holds
f . x = a . n ) ) );