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 BHSP_5:def 5, A1; :: thesis: verum