let A be Preorder; :: thesis: for f being finite-support Function of A,REAL st f is nonpositive-yielding holds
(proj A) .: (support f) = support (eqSumOf f)
let f be finite-support Function of the carrier of A,REAL; :: thesis: ( f is nonpositive-yielding implies (proj A) .: (support f) = support (eqSumOf f) )
assume A1: f is nonpositive-yielding ; :: thesis: (proj A) .: (support f) = support (eqSumOf f)
reconsider mf = - f as finite-support Function of the carrier of A,REAL ;
rng f c= COMPLEX by NUMBERS:11;
then reconsider fc = f as Function of (dom f),COMPLEX by FUNCT_2:2;
set esof = eqSumOf f;
rng (eqSumOf f) c= COMPLEX by NUMBERS:11;
then reconsider esofc = eqSumOf f as Function of (dom (eqSumOf f)),COMPLEX by FUNCT_2:2;
thus (proj A) .: (support f) = (proj A) .: (support fc)
.= (proj A) .: (support mf) by Th10
.= support (eqSumOf mf) by Th65, A1
.= support (- esofc) by Th55
.= support (eqSumOf f) by Th10 ; :: thesis: verum