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) )
dom F = DX by FUNCT_2:def 1;
then consider p being FinSequence of DX such that
A2: ( 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 A2; :: thesis: verum