let A be Preorder; for f being finite-support Function of A,REAL holds support (eqSumOf f) c= (proj A) .: (support f)
let f be finite-support Function of the carrier of A,REAL; support (eqSumOf f) c= (proj A) .: (support f)
for X being object st X in support (eqSumOf f) holds
X in (proj A) .: (support f)
proof
let X be
object ;
( X in support (eqSumOf f) implies X in (proj A) .: (support f) )
assume A1:
X in support (eqSumOf f)
;
X in (proj A) .: (support f)
ex
x being
object st
(
x in dom (proj A) &
x in support f &
X = (proj A) . x )
proof
X in dom (eqSumOf f)
by A1;
then A2:
X in the
carrier of
(QuotientOrder A)
;
A3:
dom (proj A) = the
carrier of
A
by A2, FUNCT_2:def 1;
reconsider Y =
X as
Element of
(QuotientOrder A) by A2;
set s =
canFS (eqSupport (f,Y));
A4:
rng (canFS (eqSupport (f,Y))) c= eqSupport (
f,
Y)
by FINSEQ_1:def 4;
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;
(eqSumOf f) . Y <> 0
by A1, PRE_POLY:def 7;
then
Sum fs <> 0
by A2, Def16;
then consider i being
Nat such that A5:
i in dom fs
and A6:
fs . i <> 0
by Th6;
A7:
(
i in dom (canFS (eqSupport (f,Y))) &
(canFS (eqSupport (f,Y))) . i in dom f )
by A5, FUNCT_1:11;
then reconsider x =
(canFS (eqSupport (f,Y))) . i as
Element of
A ;
take
x
;
( x in dom (proj A) & x in support f & X = (proj A) . x )
thus
x in dom (proj A)
by A3, A7;
( x in support f & X = (proj A) . x )
f . x <> 0
by A6, A7, FUNCT_1:13;
hence
x in support f
by PRE_POLY:def 7;
X = (proj A) . x
x in eqSupport (
f,
Y)
by A7, A4, FUNCT_1:3;
then A8:
x in Y
by XBOOLE_1:17, TARSKI:def 3;
X in Class (EqRelOf A)
by A2, Def7;
then consider y being
object such that A9:
y in the
carrier of
A
and A10:
X = Class (
(EqRelOf A),
y)
by EQREL_1:def 3;
A11:
x in Class (
(EqRelOf A),
y)
by A8, A10;
thus (proj A) . x =
Class (
(EqRelOf A),
x)
by Def8
.=
X
by A10, A9, A11, EQREL_1:23
;
verum
end;
hence
X in (proj A) .: (support f)
by FUNCT_1:def 6;
verum
end;
hence
support (eqSumOf f) c= (proj A) .: (support f)
; verum