let DX be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: verum