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