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