let DX be 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)) )
let F be 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)) )
let Y be 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)) )
consider p being FinSequence of DX such that
A1:
( p is one-to-one & rng p = Y & setopfunc (Y,DX,REAL,F,addreal) = addreal "**" (Func_Seq (F,p)) )
by BHSP_5:def 5;
Sum (Func_Seq (F,p)) = addreal "**" (Func_Seq (F,p))
;
hence
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)) )
by A1; verum