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

now

per cases ;

case A3: m . b <> 0. L ; :: thesis:

A4: for u being set st u in Support m holds
u in {b}

proof

let u be set ; :: thesis:
assume A5: u in Support m ; :: thesis:
assume A6: not u in {b} ; :: thesis:
reconsider u = u as Element of Bags n by A5;
u <> b by A6, TARSKI:def 1;
then m . u = 0. L by A2;
hence contradiction by A5, POLYNOM1:def 9; :: thesis:

end;

for u being set st u in {b} holds
u in Support m

proof

let u be set ; :: thesis:
assume A7: u in {b} ; :: thesis:
then u = b by TARSKI:def 1;
then reconsider u = u as Element of Bags n by POLYNOM1:def 14;
m . u <> 0. L by A3, A7, TARSKI:def 1;
hence u in Support m by POLYNOM1:def 9; :: thesis:

end;

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

proof

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

proof

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

end;

( (SgmX (BagOrder n),sm) /. 1 = (SgmX (BagOrder n),sm) . 1 & (SgmX (BagOrder n),sm) /. u = (SgmX (BagOrder n),sm) . u ) by A11, A14, FINSEQ_3:33, PARTFUN1:def 8;
then A20: ( (SgmX (BagOrder n),sm) /. 1 in rng (SgmX (BagOrder n),sm) & (SgmX (BagOrder n),sm) /. u in rng (SgmX (BagOrder n),sm) ) by A12, A14, FUNCT_1:12;
then (SgmX (BagOrder n),sm) /. 1 = b by A10, TARSKI:def 1
.= (SgmX (BagOrder n),sm) /. u by A10, A20, TARSKI:def 1 ;
hence contradiction by A9, A12, A14, A17, TRIANG_1:def 2; :: thesis:

end;

then A21: dom (SgmX (BagOrder n),sm) = Seg 1 by A13, FINSEQ_1:4, TARSKI:2;
then A22: len (SgmX (BagOrder n),sm) = 1 by FINSEQ_1:def 3;
A23: 1 in dom (SgmX (BagOrder n),sm) by A21, FINSEQ_1:4, TARSKI:def 1;
(SgmX (BagOrder n),sm) /. 1 = (SgmX (BagOrder n),sm) . 1 by A12, PARTFUN1:def 8;
then (SgmX (BagOrder n),sm) /. 1 in rng (SgmX (BagOrder n),sm) by A23, FUNCT_1:12;
then A24: (SgmX (BagOrder n),sm) /. 1 = b by A10, TARSKI:def 1;
A25: (SgmX (BagOrder n),sm) . 1 in rng (SgmX (BagOrder n),sm) by A12, FUNCT_1:12;
then A26: (SgmX (BagOrder n),sm) . 1 = b by A10, TARSKI:def 1;
A27: b in Bags n by POLYNOM1:def 14;
dom m = Bags n by FUNCT_2:def 1;
then 1 in dom (m * (SgmX (BagOrder n),sm)) by A12, A26, A27, FUNCT_1:21;
then A28: (m * (SgmX (BagOrder n),sm)) /. 1 = (m * (SgmX (BagOrder n),sm)) . 1 by PARTFUN1:def 8
.= m . ((SgmX (BagOrder n),sm) . 1) by A12, FUNCT_1:23
.= m . b by A10, A25, TARSKI:def 1
.= coefficient m by A3, Def6 ;
dom y = Seg (len y) by FINSEQ_1:def 3
.= dom (SgmX (BagOrder n),sm) by A1, FINSEQ_1:def 3 ;
then y . 1 = y /. 1 by A23, PARTFUN1:def 8
.= ((m * (SgmX (BagOrder n),sm)) /. 1) * (eval (((SgmX (BagOrder n),sm) /. 1) @ ),x) by A1, A22
.= ((m * (SgmX (BagOrder n),sm)) /. 1) * (eval b,x) by A24, POLYNOM2:def 3 ;
then y = <*((coefficient m) * (eval b,x))*> by A1, A22, A28, FINSEQ_1:57;
hence eval m,x = (coefficient m) * (eval b,x) by A1, RLVECT_1:61
.= (coefficient m) * (eval (term m),x) by A3, Def6 ;
:: thesis:

end;

case A29: m . b = 0. L ; :: thesis:

A30: Support m = {}

proof

assume Support m <> {} ; :: thesis:
then reconsider sm = Support m as non empty Subset of (Bags n) ;
consider c being Element of sm;
c in Support m ;
then m . c <> 0. L by POLYNOM1:def 9;
hence contradiction by A2, A29; :: thesis:

end;

then A31: term m = EmptyBag n by Def6;
m . (EmptyBag n) = 0. L by A30, POLYNOM1:def 9;
then A32: (coefficient m) * (eval (term m),x) = 0. L by A31, VECTSP_1:39;
consider y being FinSequence of the carrier of L such that
A33: ( len y = len (SgmX (BagOrder n),(Support m)) & eval m,x = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((m * (SgmX (BagOrder n),(Support m))) /. i) * (eval (((SgmX (BagOrder n),(Support m)) /. i) @ ),x) ) ) by POLYNOM2:def 4;
BagOrder n linearly_orders Support m by POLYNOM2:20;
then rng (SgmX (BagOrder n),(Support m)) = {} by A30, TRIANG_1:def 2;
then SgmX (BagOrder n),(Support m) = {} by RELAT_1:64;
then len y = 0 by A33;
then y = <*> the carrier of L ;
hence eval m,x = (coefficient m) * (eval (term m),x) by A32, A33, RLVECT_1:60; :: thesis:

end;

hence eval m,x = (coefficient m) * (eval (term m),x) ; :: thesis: