let A be non empty set ; :: thesis: for D being non empty a_partition of A

for f being finite-support Function of A,REAL st f is nonpositive-yielding holds

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

let D be non empty a_partition of A; :: thesis: for f being finite-support Function of A,REAL st f is nonpositive-yielding holds

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

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

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

reconsider PFP = PreorderFromPartition D as non empty Preorder ;

reconsider F = f as finite-support Function of PFP,REAL ;

reconsider E = D as a_partition of the carrier of PFP ;

D = the carrier of (QuotientOrder PFP) by Th51;

then A2: eqSumOf F = D eqSumOf f by Def15;

A3: proj PFP = proj E by Th48, Th51;

support (eqSumOf F) = (proj PFP) .: (support F) by A1, Th67;

hence (proj D) .: (support f) = support (D eqSumOf f) by A3, A2; :: thesis: verum

for f being finite-support Function of A,REAL st f is nonpositive-yielding holds

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

let D be non empty a_partition of A; :: thesis: for f being finite-support Function of A,REAL st f is nonpositive-yielding holds

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

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

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

reconsider PFP = PreorderFromPartition D as non empty Preorder ;

reconsider F = f as finite-support Function of PFP,REAL ;

reconsider E = D as a_partition of the carrier of PFP ;

D = the carrier of (QuotientOrder PFP) by Th51;

then A2: eqSumOf F = D eqSumOf f by Def15;

A3: proj PFP = proj E by Th48, Th51;

support (eqSumOf F) = (proj PFP) .: (support F) by A1, Th67;

hence (proj D) .: (support f) = support (D eqSumOf f) by A3, A2; :: thesis: verum