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

(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