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

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

hence
D eqSumOf f is nonnegative-yielding
by PARTFUN3:def 4; :: thesis: verum
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

hence 0 <= r by A3, A2, Def14; :: thesis: verum

end;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

then
0 <= Sum s
by RVSUM_1:84;
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;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

hence 0 <= r by A3, A2, Def14; :: thesis: verum