:: deftheorem defines are_Re-presentation_of MESFUN7C:def 15 :
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for F being Finite_Sep_Sequence of S
for a being FinSequence of COMPLEX 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 ) ) );