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