let DX be non empty set ; 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; 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; ( ( 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
; 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 for i being Nat st i in dom (Func_Seq (F,p)) holds
0 <= (Func_Seq (F,p)) . ilet i be
Nat;
( i in dom (Func_Seq (F,p)) implies 0 <= (Func_Seq (F,p)) . i )assume A3:
i in dom (Func_Seq (F,p))
;
0 <= (Func_Seq (F,p)) . ithen 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;
verum end;
hence
0 <= setopfunc (Y,DX,REAL,F,addreal)
by A2, RVSUM_1:84; verum