let A be set ; :: thesis: for D being a_partition of A
for f being nonnegative-yielding finite-support Function of A,REAL holds D eqSumOf f is nonnegative-yielding
let D be a_partition of A; :: thesis: for f being nonnegative-yielding finite-support Function of A,REAL holds D eqSumOf f is nonnegative-yielding
let f be nonnegative-yielding finite-support Function of A,REAL; :: thesis: D eqSumOf f is nonnegative-yielding
for r being Real st r in rng (D eqSumOf f) holds
0 <= r
proof
let r be Real; :: thesis: ( r in rng (D eqSumOf f) implies 0 <= r )
assume r in rng (D eqSumOf f) ; :: thesis: 0 <= r
then consider X being object such that
A2: X in dom (D eqSumOf f) and
A3: r = (D eqSumOf f) . X by FUNCT_1:def 3;
reconsider X = X as Element of D by A2;
set s = f * (canFS (eqSupport (f,X)));
rng (f * (canFS (eqSupport (f,X)))) c= REAL ;
then reconsider s = f * (canFS (eqSupport (f,X))) as FinSequence of REAL by FINSEQ_1:def 4;
for i being Nat st i in dom s holds
0 <= s . i
proof
let i be Nat; :: thesis: ( i in dom s implies 0 <= s . i )
assume i in dom s ; :: thesis: 0 <= s . i
then s . i in rng s by FUNCT_1:3;
hence 0 <= s . i by PARTFUN3:def 4; :: thesis: verum
end;
then 0 <= Sum s by RVSUM_1:84;
hence 0 <= r by A3, A2, Def14; :: thesis: verum
end;
hence D eqSumOf f is nonnegative-yielding by PARTFUN3:def 4; :: thesis: verum