let A be Preorder; for f being finite-support Function of A,REAL st f is nonnegative-yielding holds
(proj A) .: (support f) = support (eqSumOf f)
let f be finite-support Function of the carrier of A,REAL; ( f is nonnegative-yielding implies (proj A) .: (support f) = support (eqSumOf f) )
assume A1:
f is nonnegative-yielding
; (proj A) .: (support f) = support (eqSumOf f)
for X being object st X in (proj A) .: (support f) holds
X in support (eqSumOf f)
proof
let X be
object ;
( X in (proj A) .: (support f) implies X in support (eqSumOf f) )
assume A2:
X in (proj A) .: (support f)
;
X in support (eqSumOf f)
then consider x being
object such that A3:
x in dom (proj A)
and A4:
x in support f
and A5:
X = (proj A) . x
by FUNCT_1:def 6;
A6:
X in the
carrier of
(QuotientOrder A)
by A2, FUNCT_2:36, TARSKI:def 3;
reconsider Y =
X as
Element of the
carrier of
(QuotientOrder A) by A6;
set s =
canFS (eqSupport (f,Y));
A7:
rng (canFS (eqSupport (f,Y))) = eqSupport (
f,
Y)
by FUNCT_2:def 3;
canFS (eqSupport (f,Y)) is
FinSequence of the
carrier of
A
by FINSEQ_2:24;
then reconsider fs =
f * (canFS (eqSupport (f,Y))) as
FinSequence of
REAL by FINSEQ_2:32;
A8:
ex
k being
Nat st
(
k in dom fs &
fs . k <> 0 )
proof
reconsider y =
x as
Element of
A by A3;
X = Class (
(EqRelOf A),
y)
by A5, Def8;
then
y in Y
by A3, EQREL_1:20;
then
y in eqSupport (
f,
Y)
by A4, XBOOLE_0:def 4;
then consider i being
object such that A9:
i in dom (canFS (eqSupport (f,Y)))
and A10:
(canFS (eqSupport (f,Y))) . i = y
by A7, FUNCT_1:def 3;
reconsider i =
i as
Nat by A9;
take
i
;
( i in dom fs & fs . i <> 0 )
thus
i in dom fs
by A4, A10, A9, FUNCT_1:11;
fs . i <> 0
f . y <> 0
by A4, PRE_POLY:def 7;
hence
fs . i <> 0
by A9, A10, FUNCT_1:13;
verum
end;
A11:
(eqSumOf f) . Y = Sum fs
by A6, Def16;
Sum fs > 0
by A1, A8, Th7;
hence
X in support (eqSumOf f)
by PRE_POLY:def 7, A11;
verum
end;
then
(proj A) .: (support f) c= support (eqSumOf f)
;
hence
(proj A) .: (support f) = support (eqSumOf f)
by Th63; verum