let DX be non empty set ; :: thesis: for F being Function of DX,REAL
for Y1, Y2 being finite Subset of DX st Y1 c= Y2 & ( for x being set st x in Y2 holds
0 <= F . x ) holds
setopfunc (Y1,DX,REAL,F,addreal) <= setopfunc (Y2,DX,REAL,F,addreal)
let F be Function of DX,REAL; :: thesis: for Y1, Y2 being finite Subset of DX st Y1 c= Y2 & ( for x being set st x in Y2 holds
0 <= F . x ) holds
setopfunc (Y1,DX,REAL,F,addreal) <= setopfunc (Y2,DX,REAL,F,addreal)
let Y1, Y2 be finite Subset of DX; :: thesis: ( Y1 c= Y2 & ( for x being set st x in Y2 holds
0 <= F . x ) implies setopfunc (Y1,DX,REAL,F,addreal) <= setopfunc (Y2,DX,REAL,F,addreal) )
assume AS: ( Y1 c= Y2 & ( for x being set st x in Y2 holds
0 <= F . x ) ) ; :: thesis: setopfunc (Y1,DX,REAL,F,addreal) <= setopfunc (Y2,DX,REAL,F,addreal)
consider p1 being FinSequence of DX such that
PP1: ( p1 is one-to-one & rng p1 = Y1 & setopfunc (Y1,DX,REAL,F,addreal) = Sum (Func_Seq (F,p1)) ) by LMXY092;
reconsider Y3 = Y2 \ Y1 as finite Subset of DX ;
consider p2 being FinSequence of DX such that
PP3: ( p2 is one-to-one & rng p2 = Y3 & setopfunc (Y3,DX,REAL,F,addreal) = Sum (Func_Seq (F,p2)) ) by LMXY092;

now

let i be Nat; :: thesis: ( i in dom (Func_Seq (F,p2)) implies 0 <= (Func_Seq (F,p2)) . i )
assume P11: i in dom (Func_Seq (F,p2)) ; :: thesis: 0 <= (Func_Seq (F,p2)) . i
then P2: (Func_Seq (F,p2)) . i = F . (p2 . i) by FUNCT_1:22;
i in dom p2 by P11, FUNCT_1:21;
then PP2: p2 . i in Y3 by PP3, FUNCT_1:12;
Y3 c= Y2 by XBOOLE_1:36;
hence 0 <= (Func_Seq (F,p2)) . i by P2, AS, PP2; :: thesis: verum

end;

then Q2: 0 <= Sum (Func_Seq (F,p2)) by RVSUM_1:114;
reconsider p3 = p1 ^ p2 as FinSequence of DX ;
PP6: rng p3 = (rng p1) \/ (rng p2) by FINSEQ_1:44
.= Y1 \/ Y2 by XBOOLE_1:39, PP3, PP1
.= Y2 by XBOOLE_1:12, AS ;
rng p1 misses rng p2 by XBOOLE_1:79, PP1, PP3;
then p3 is one-to-one by FINSEQ_3:98, PP1, PP3;
then PP7: setopfunc (Y2,DX,REAL,F,addreal) = Sum (Func_Seq (F,p3)) by PP6, LMXY092A;
QQQ: Func_Seq (F,p3) = (Func_Seq (F,p1)) ^ (Func_Seq (F,p2)) by LMXXX1;
(Sum (Func_Seq (F,p1))) + 0 <= (Sum (Func_Seq (F,p1))) + (Sum (Func_Seq (F,p2))) by Q2, XREAL_1:8;
hence setopfunc (Y1,DX,REAL,F,addreal) <= setopfunc (Y2,DX,REAL,F,addreal) by PP1, RVSUM_1:105, QQQ, PP7; :: thesis: verum