for DX being non empty set
for F being Function of DX,REAL
for Y being finite Subset of DX ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p)) )