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 A1: 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
A2: ( p is one-to-one & rng p = Y & setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p)) ) by Th9;
now :: thesis: for i being Nat st i in dom (Func_Seq (F,p)) holds
0 <= (Func_Seq (F,p)) . i
let i be Nat; :: thesis: ( i in dom (Func_Seq (F,p)) implies 0 <= (Func_Seq (F,p)) . i )
assume A3: i in dom (Func_Seq (F,p)) ; :: thesis: 0 <= (Func_Seq (F,p)) . i
then A4: (Func_Seq (F,p)) . i = F . (p . i) by FUNCT_1:12;
i in dom p by A3, FUNCT_1:11;
hence 0 <= (Func_Seq (F,p)) . i by A4, A1, A2, FUNCT_1:3; :: thesis: verum
end;
hence 0 <= setopfunc (Y,DX,REAL,F,addreal) by A2, RVSUM_1:84; :: thesis: verum