let DX be non empty set ; :: thesis: for F being Function of DX,REAL
for Y being finite Subset of DX st ( for x being set st x in Y holds
0 <= F . x ) holds
0 <= setopfunc Y,DX,REAL ,F,addreal
let F be Function of DX,REAL ; :: thesis: for Y being finite Subset of DX st ( for x being set st x in Y holds
0 <= F . x ) holds
0 <= setopfunc Y,DX,REAL ,F,addreal
let Y be finite Subset of DX; :: thesis: ( ( for x being set st x in Y holds
0 <= F . x ) implies 0 <= setopfunc Y,DX,REAL ,F,addreal )
assume AS: for x being set st x in Y holds
0 <= F . x ; :: thesis: 0 <= setopfunc Y,DX,REAL ,F,addreal
consider p being FinSequence of DX such that
P1: ( p is one-to-one & rng p = Y & setopfunc Y,DX,REAL ,F,addreal = Sum (Func_Seq F,p) ) by LMXY092;

now

let i be Nat; :: thesis: ( i in dom (Func_Seq F,p) implies 0 <= (Func_Seq F,p) . i )
assume P11: i in dom (Func_Seq F,p) ; :: thesis: 0 <= (Func_Seq F,p) . i
then P2: (Func_Seq F,p) . i = F . (p . i) by FUNCT_1:22;
i in dom p by P11, FUNCT_1:21;
hence 0 <= (Func_Seq F,p) . i by P2, AS, P1, FUNCT_1:12; :: thesis: verum

end;

hence 0 <= setopfunc Y,DX,REAL ,F,addreal by P1, RVSUM_1:114; :: thesis: verum