let A be Preorder; :: thesis: for f being finite-support Function of A,REAL st f is nonnegative-yielding holds

(proj A) .: (support f) = support (eqSumOf f)

let f be finite-support Function of the carrier of A,REAL; :: thesis: ( f is nonnegative-yielding implies (proj A) .: (support f) = support (eqSumOf f) )

assume A1: f is nonnegative-yielding ; :: thesis: (proj A) .: (support f) = support (eqSumOf f)

for X being object st X in (proj A) .: (support f) holds

X in support (eqSumOf f)

hence (proj A) .: (support f) = support (eqSumOf f) by Th63; :: thesis: verum

(proj A) .: (support f) = support (eqSumOf f)

let f be finite-support Function of the carrier of A,REAL; :: thesis: ( f is nonnegative-yielding implies (proj A) .: (support f) = support (eqSumOf f) )

assume A1: f is nonnegative-yielding ; :: thesis: (proj A) .: (support f) = support (eqSumOf f)

for X being object st X in (proj A) .: (support f) holds

X in support (eqSumOf f)

proof

then
(proj A) .: (support f) c= support (eqSumOf f)
;
let X be object ; :: thesis: ( X in (proj A) .: (support f) implies X in support (eqSumOf f) )

assume A2: X in (proj A) .: (support f) ; :: thesis: X in support (eqSumOf f)

then consider x being object such that

A3: x in dom (proj A) and

A4: x in support f and

A5: X = (proj A) . x by FUNCT_1:def 6;

A6: X in the carrier of (QuotientOrder A) by A2, FUNCT_2:36, TARSKI:def 3;

reconsider Y = X as Element of the carrier of (QuotientOrder A) by A6;

set s = canFS (eqSupport (f,Y));

A7: rng (canFS (eqSupport (f,Y))) = eqSupport (f,Y) by FUNCT_2:def 3;

canFS (eqSupport (f,Y)) is FinSequence of the carrier of A by FINSEQ_2:24;

then reconsider fs = f * (canFS (eqSupport (f,Y))) as FinSequence of REAL by FINSEQ_2:32;

A8: ex k being Nat st

( k in dom fs & fs . k <> 0 )

Sum fs > 0 by A1, A8, Th7;

hence X in support (eqSumOf f) by PRE_POLY:def 7, A11; :: thesis: verum

end;assume A2: X in (proj A) .: (support f) ; :: thesis: X in support (eqSumOf f)

then consider x being object such that

A3: x in dom (proj A) and

A4: x in support f and

A5: X = (proj A) . x by FUNCT_1:def 6;

A6: X in the carrier of (QuotientOrder A) by A2, FUNCT_2:36, TARSKI:def 3;

reconsider Y = X as Element of the carrier of (QuotientOrder A) by A6;

set s = canFS (eqSupport (f,Y));

A7: rng (canFS (eqSupport (f,Y))) = eqSupport (f,Y) by FUNCT_2:def 3;

canFS (eqSupport (f,Y)) is FinSequence of the carrier of A by FINSEQ_2:24;

then reconsider fs = f * (canFS (eqSupport (f,Y))) as FinSequence of REAL by FINSEQ_2:32;

A8: ex k being Nat st

( k in dom fs & fs . k <> 0 )

proof

A11:
(eqSumOf f) . Y = Sum fs
by A6, Def16;
reconsider y = x as Element of A by A3;

X = Class ((EqRelOf A),y) by A5, Def8;

then y in Y by A3, EQREL_1:20;

then y in eqSupport (f,Y) by A4, XBOOLE_0:def 4;

then consider i being object such that

A9: i in dom (canFS (eqSupport (f,Y))) and

A10: (canFS (eqSupport (f,Y))) . i = y by A7, FUNCT_1:def 3;

reconsider i = i as Nat by A9;

take i ; :: thesis: ( i in dom fs & fs . i <> 0 )

thus i in dom fs by A4, A10, A9, FUNCT_1:11; :: thesis: fs . i <> 0

f . y <> 0 by A4, PRE_POLY:def 7;

hence fs . i <> 0 by A9, A10, FUNCT_1:13; :: thesis: verum

end;X = Class ((EqRelOf A),y) by A5, Def8;

then y in Y by A3, EQREL_1:20;

then y in eqSupport (f,Y) by A4, XBOOLE_0:def 4;

then consider i being object such that

A9: i in dom (canFS (eqSupport (f,Y))) and

A10: (canFS (eqSupport (f,Y))) . i = y by A7, FUNCT_1:def 3;

reconsider i = i as Nat by A9;

take i ; :: thesis: ( i in dom fs & fs . i <> 0 )

thus i in dom fs by A4, A10, A9, FUNCT_1:11; :: thesis: fs . i <> 0

f . y <> 0 by A4, PRE_POLY:def 7;

hence fs . i <> 0 by A9, A10, FUNCT_1:13; :: thesis: verum

Sum fs > 0 by A1, A8, Th7;

hence X in support (eqSumOf f) by PRE_POLY:def 7, A11; :: thesis: verum

hence (proj A) .: (support f) = support (eqSumOf f) by Th63; :: thesis: verum