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 A1: ( 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
A2: ( p1 is one-to-one & rng p1 = Y1 & setopfunc (Y1,DX,REAL,F,addreal) = Sum (Func_Seq (F,p1)) ) by Th9;
reconsider Y3 = Y2 \ Y1 as finite Subset of DX ;
consider p2 being FinSequence of DX such that
A3: ( p2 is one-to-one & rng p2 = Y3 & setopfunc (Y3,DX,REAL,F,addreal) = Sum (Func_Seq (F,p2)) ) by Th9;
now :: thesis: for i being Nat st i in dom (Func_Seq (F,p2)) holds
0 <= (Func_Seq (F,p2)) . i
let i be Nat; :: thesis: ( i in dom (Func_Seq (F,p2)) implies 0 <= (Func_Seq (F,p2)) . i )
assume A4: i in dom (Func_Seq (F,p2)) ; :: thesis: 0 <= (Func_Seq (F,p2)) . i
then A5: (Func_Seq (F,p2)) . i = F . (p2 . i) by FUNCT_1:12;
i in dom p2 by A4, FUNCT_1:11;
then A6: p2 . i in Y3 by A3, FUNCT_1:3;
Y3 c= Y2 by XBOOLE_1:36;
hence 0 <= (Func_Seq (F,p2)) . i by A5, A1, A6; :: thesis: verum
end;
then A7: 0 <= Sum (Func_Seq (F,p2)) by RVSUM_1:84;
reconsider p3 = p1 ^ p2 as FinSequence of DX ;
A8: rng p3 = (rng p1) \/ (rng p2) by FINSEQ_1:31
.= Y1 \/ Y2 by A3, A2, XBOOLE_1:39
.= Y2 by A1, XBOOLE_1:12 ;
rng p1 misses rng p2 by A2, A3, XBOOLE_1:79;
then p3 is one-to-one by A2, A3, FINSEQ_3:91;
then A9: setopfunc (Y2,DX,REAL,F,addreal) = Sum (Func_Seq (F,p3)) by A8, Th10;
A10: Func_Seq (F,p3) = (Func_Seq (F,p1)) ^ (Func_Seq (F,p2)) by Lm5;
(Sum (Func_Seq (F,p1))) + 0 <= (Sum (Func_Seq (F,p1))) + (Sum (Func_Seq (F,p2))) by A7, XREAL_1:6;
hence setopfunc (Y1,DX,REAL,F,addreal) <= setopfunc (Y2,DX,REAL,F,addreal) by A2, A10, A9, RVSUM_1:75; :: thesis: verum