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