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