let DX be non empty set ; :: thesis: 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))
let F be Function of DX,REAL; :: thesis: 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))
let Y be finite Subset of DX; :: thesis: 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))
let p be FinSequence of DX; :: thesis: ( p is one-to-one & rng p = Y implies setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p)) )
assume A1: ( p is one-to-one & rng p = Y ) ; :: thesis: setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p))
dom F = DX by FUNCT_2:def 1;
hence setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p)) by A1, BHSP_5:def 5; :: thesis: verum