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 holds support (D eqSumOf f) c= (proj D) .: (support f)

let D be non empty a_partition of A; :: thesis: for f being finite-support Function of A,REAL holds support (D eqSumOf f) c= (proj D) .: (support f)

let f be finite-support Function of A,REAL; :: thesis: support (D eqSumOf f) c= (proj D) .: (support 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 A1: eqSumOf F = D eqSumOf f by Def15;

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

support (eqSumOf F) c= (proj PFP) .: (support F) by Th63;

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

for f being finite-support Function of A,REAL holds support (D eqSumOf f) c= (proj D) .: (support f)

let D be non empty a_partition of A; :: thesis: for f being finite-support Function of A,REAL holds support (D eqSumOf f) c= (proj D) .: (support f)

let f be finite-support Function of A,REAL; :: thesis: support (D eqSumOf f) c= (proj D) .: (support 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 A1: eqSumOf F = D eqSumOf f by Def15;

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

support (eqSumOf F) c= (proj PFP) .: (support F) by Th63;

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