let n be Ordinal; :: thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for c being ConstPoly of n,L
for x being Function of n,L holds eval c,x = coefficient c
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for c being ConstPoly of n,L
for x being Function of n,L holds eval c,x = coefficient c
let c be ConstPoly of n,L; :: thesis: for x being Function of n,L holds eval c,x = coefficient c
let x be Function of n,L; :: thesis: eval c,x = coefficient c
consider y being FinSequence of the carrier of L such that
A1: ( len y = len (SgmX (BagOrder n),(Support c)) & eval c,x = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((c * (SgmX (BagOrder n),(Support c))) /. i) * (eval (((SgmX (BagOrder n),(Support c)) /. i) @ ),x) ) ) by POLYNOM2:def 4;

now

per cases ( coefficient c = 0. L or coefficient c <> 0. L ) ;

case A2: coefficient c = 0. L ; :: thesis: eval c,x = coefficient c

Support c = {}

proof

assume A3: Support c <> {} ; :: thesis: contradiction
consider u being Element of Support c;
u in Support c by A3;
then reconsider u = u as Element of Bags n ;
c . u <> 0. L by A3, POLYNOM1:def 9;
then u <> EmptyBag n by A2, Lm2;
then c . u = 0. L by Def8;
hence contradiction by A3, POLYNOM1:def 9; :: thesis: verum

end;

then reconsider Sc = Support c as empty Subset of (Bags n) ;
SgmX (BagOrder n),Sc = {} by POLYNOM2:9, POLYNOM2:20;
then len y = 0 by A1;
then y = <*> the carrier of L ;
hence eval c,x = coefficient c by A1, A2, RLVECT_1:60; :: thesis: verum

end;

case A4: coefficient c <> 0. L ; :: thesis: eval c,x = coefficient c

A5: for u being set st u in Support c holds
u in {(EmptyBag n)}

proof

let u be set ; :: thesis: ( u in Support c implies u in {(EmptyBag n)} )
assume A6: u in Support c ; :: thesis: u in {(EmptyBag n)}
assume A7: not u in {(EmptyBag n)} ; :: thesis: contradiction
reconsider u = u as Element of Bags n by A6;
u <> EmptyBag n by A7, TARSKI:def 1;
then c . u = 0. L by Def8;
hence contradiction by A6, POLYNOM1:def 9; :: thesis: verum

end;

for u being set st u in {(EmptyBag n)} holds
u in Support c

proof

let u be set ; :: thesis: ( u in {(EmptyBag n)} implies u in Support c )
assume A8: u in {(EmptyBag n)} ; :: thesis: u in Support c
then A9: u = EmptyBag n by TARSKI:def 1;
reconsider u = u as Element of Bags n by A8;
c . u <> 0. L by A4, A9, Lm2;
hence u in Support c by POLYNOM1:def 9; :: thesis: verum

end;

then A10: Support c = {(EmptyBag n)} by A5, TARSKI:2;
reconsider sc = Support c as finite Subset of (Bags n) ;
set sg = SgmX (BagOrder n),sc;
A11: BagOrder n linearly_orders sc by POLYNOM2:20;
then A12: ( rng (SgmX (BagOrder n),sc) = {(EmptyBag n)} & ( for l, m being Nat st l in dom (SgmX (BagOrder n),sc) & m in dom (SgmX (BagOrder n),sc) & l < m holds
( (SgmX (BagOrder n),sc) /. l <> (SgmX (BagOrder n),sc) /. m & [((SgmX (BagOrder n),sc) /. l),((SgmX (BagOrder n),sc) /. m)] in BagOrder n ) ) ) by A10, TRIANG_1:def 2;
then A13: EmptyBag n in rng (SgmX (BagOrder n),sc) by TARSKI:def 1;
then A14: 1 in dom (SgmX (BagOrder n),sc) by FINSEQ_3:33;
then A15: for u being set st u in {1} holds
u in dom (SgmX (BagOrder n),sc) by TARSKI:def 1;
for u being set st u in dom (SgmX (BagOrder n),sc) holds
u in {1}

proof

let u be set ; :: thesis: ( u in dom (SgmX (BagOrder n),sc) implies u in {1} )
assume A16: u in dom (SgmX (BagOrder n),sc) ; :: thesis: u in {1}
assume A17: not u in {1} ; :: thesis: contradiction
reconsider u = u as Element of NAT by A16;
A18: u <> 1 by A17, TARSKI:def 1;
A19: 1 < u

proof

consider k being Nat such that
A20: dom (SgmX (BagOrder n),sc) = Seg k by FINSEQ_1:def 2;
Seg k = { m where m is Element of NAT : ( 1 <= m & m <= k ) } by FINSEQ_1:def 1;
then consider m' being Element of NAT such that
A21: ( m' = u & 1 <= m' & m' <= k ) by A16, A20;
thus 1 < u by A18, A21, XXREAL_0:1; :: thesis: verum

end;

( (SgmX (BagOrder n),sc) /. 1 = (SgmX (BagOrder n),sc) . 1 & (SgmX (BagOrder n),sc) /. u = (SgmX (BagOrder n),sc) . u ) by A13, A16, FINSEQ_3:33, PARTFUN1:def 8;
then A22: ( (SgmX (BagOrder n),sc) /. 1 in rng (SgmX (BagOrder n),sc) & (SgmX (BagOrder n),sc) /. u in rng (SgmX (BagOrder n),sc) ) by A14, A16, FUNCT_1:12;
then (SgmX (BagOrder n),sc) /. 1 = EmptyBag n by A12, TARSKI:def 1
.= (SgmX (BagOrder n),sc) /. u by A12, A22, TARSKI:def 1 ;
hence contradiction by A11, A14, A16, A19, TRIANG_1:def 2; :: thesis: verum

end;

then A23: dom (SgmX (BagOrder n),sc) = Seg 1 by A15, FINSEQ_1:4, TARSKI:2;
then A24: len (SgmX (BagOrder n),sc) = 1 by FINSEQ_1:def 3;
A25: 1 in dom (SgmX (BagOrder n),sc) by A23, FINSEQ_1:4, TARSKI:def 1;
(SgmX (BagOrder n),sc) /. 1 = (SgmX (BagOrder n),sc) . 1 by A14, PARTFUN1:def 8;
then (SgmX (BagOrder n),sc) /. 1 in rng (SgmX (BagOrder n),sc) by A25, FUNCT_1:12;
then A26: (SgmX (BagOrder n),sc) /. 1 = EmptyBag n by A12, TARSKI:def 1;
A27: (SgmX (BagOrder n),sc) . 1 in rng (SgmX (BagOrder n),sc) by A14, FUNCT_1:12;
dom c = Bags n by FUNCT_2:def 1;
then 1 in dom (c * (SgmX (BagOrder n),sc)) by A12, A14, A27, FUNCT_1:21;
then A28: (c * (SgmX (BagOrder n),sc)) /. 1 = (c * (SgmX (BagOrder n),sc)) . 1 by PARTFUN1:def 8
.= c . ((SgmX (BagOrder n),sc) . 1) by A14, FUNCT_1:23
.= c . (EmptyBag n) by A12, A27, TARSKI:def 1
.= coefficient c by Lm2 ;
dom y = Seg (len y) by FINSEQ_1:def 3
.= dom (SgmX (BagOrder n),sc) by A1, FINSEQ_1:def 3 ;
then y . 1 = y /. 1 by A25, PARTFUN1:def 8
.= ((c * (SgmX (BagOrder n),sc)) /. 1) * (eval (((SgmX (BagOrder n),sc) /. 1) @ ),x) by A1, A24
.= (coefficient c) * (eval (EmptyBag n),x) by A26, A28, POLYNOM2:def 3
.= (coefficient c) * (1. L) by POLYNOM2:16
.= coefficient c by VECTSP_1:def 16 ;
then y = <*(coefficient c)*> by A1, A24, FINSEQ_1:57;
hence eval c,x = coefficient c by A1, RLVECT_1:61; :: thesis: verum

end;

end;

end;

hence eval c,x = coefficient c ; :: thesis: verum