let A be Preorder; :: thesis: 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; :: thesis: 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)

let f be finite-support Function of the carrier of A,REAL; :: thesis: 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

hence
support (eqSumOf f) c= (proj A) .: (support f)
; :: thesis: verum
let X be object ; :: thesis: ( X in support (eqSumOf f) implies X in (proj A) .: (support f) )

assume A1: X in support (eqSumOf f) ; :: thesis: X in (proj A) .: (support f)

ex x being object st

( x in dom (proj A) & x in support f & X = (proj A) . x )

end;assume A1: X in support (eqSumOf f) ; :: thesis: 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

hence
X in (proj A) .: (support f)
by FUNCT_1:def 6; :: thesis: verum
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 ; :: thesis: ( x in dom (proj A) & x in support f & X = (proj A) . x )

thus x in dom (proj A) by A3, A7; :: thesis: ( 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; :: thesis: 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 ; :: thesis: verum

end;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 ; :: thesis: ( x in dom (proj A) & x in support f & X = (proj A) . x )

thus x in dom (proj A) by A3, A7; :: thesis: ( 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; :: thesis: 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 ; :: thesis: verum