theorem Th10: :: RANDOM_2:10

for DX being non empty set
for F being Function of DX,REAL
for Y being finite Subset of DX
for p being FinSequence of DX st p is one-to-one & rng p = Y holds
setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p)) by BHSP_5:def 5;