let n be Ordinal; :: thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for m being Monomial of n,L
for x being Function of n,L holds eval (m,x) = () * (eval ((term m),x))

let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for m being Monomial of n,L
for x being Function of n,L holds eval (m,x) = () * (eval ((term m),x))

let m be Monomial of n,L; :: thesis: for x being Function of n,L holds eval (m,x) = () * (eval ((term m),x))
let x be Function of n,L; :: thesis: eval (m,x) = () * (eval ((term m),x))
consider y being FinSequence of the carrier of L such that
A1: len y = len (SgmX ((),())) and
A2: eval (m,x) = Sum y and
A3: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((m * (SgmX ((),()))) /. i) * (eval (((SgmX ((),())) /. i),x)) by POLYNOM2:def 4;
consider b being bag of n such that
A4: for b9 being bag of n st b9 <> b holds
m . b9 = 0. L by Def3;
now :: thesis: ( ( m . b <> 0. L & eval (m,x) = () * (eval ((term m),x)) ) or ( m . b = 0. L & eval (m,x) = () * (eval ((term m),x)) ) )
per cases ( m . b <> 0. L or m . b = 0. L ) ;
case A5: m . b <> 0. L ; :: thesis: eval (m,x) = () * (eval ((term m),x))
A6: for u being object st u in Support m holds
u in {b}
proof
let u be object ; :: thesis: ( u in Support m implies u in {b} )
assume A7: u in Support m ; :: thesis: u in {b}
assume A8: not u in {b} ; :: thesis: contradiction
reconsider u = u as Element of Bags n by A7;
u <> b by ;
then m . u = 0. L by A4;
hence contradiction by A7, POLYNOM1:def 4; :: thesis: verum
end;
A9: ( b in Bags n & dom m = Bags n ) by ;
reconsider sm = Support m as finite Subset of (Bags n) ;
set sg = SgmX ((),sm);
A10: BagOrder n linearly_orders sm by POLYNOM2:18;
for u being object st u in {b} holds
u in Support m
proof
let u be object ; :: thesis: ( u in {b} implies u in Support m )
assume A11: u in {b} ; :: thesis:
then u = b by TARSKI:def 1;
then reconsider u = u as Element of Bags n by PRE_POLY:def 12;
m . u <> 0. L by ;
hence u in Support m by POLYNOM1:def 4; :: thesis: verum
end;
then Support m = {b} by ;
then A12: rng (SgmX ((),sm)) = {b} by ;
then A13: b in rng (SgmX ((),sm)) by TARSKI:def 1;
then A14: 1 in dom (SgmX ((),sm)) by FINSEQ_3:31;
then A15: (SgmX ((),sm)) . 1 in rng (SgmX ((),sm)) by FUNCT_1:3;
then (SgmX ((),sm)) . 1 = b by ;
then 1 in dom (m * (SgmX ((),sm))) by ;
then A16: (m * (SgmX ((),sm))) /. 1 = (m * (SgmX ((),sm))) . 1 by PARTFUN1:def 6
.= m . ((SgmX ((),sm)) . 1) by
.= m . b by
.= coefficient m by ;
A17: for u being object st u in dom (SgmX ((),sm)) holds
u in {1}
proof
let u be object ; :: thesis: ( u in dom (SgmX ((),sm)) implies u in {1} )
assume A18: u in dom (SgmX ((),sm)) ; :: thesis: u in {1}
assume A19: not u in {1} ; :: thesis: contradiction
reconsider u = u as Element of NAT by A18;
(SgmX ((),sm)) /. u = (SgmX ((),sm)) . u by ;
then A20: (SgmX ((),sm)) /. u in rng (SgmX ((),sm)) by ;
A21: u <> 1 by ;
A22: 1 < u
proof
consider k being Nat such that
A23: dom (SgmX ((),sm)) = Seg k by FINSEQ_1:def 2;
Seg k = { l where l is Nat : ( 1 <= l & l <= k ) } by FINSEQ_1:def 1;
then ex m9 being Nat st
( m9 = u & 1 <= m9 & m9 <= k ) by ;
hence 1 < u by ; :: thesis: verum
end;
(SgmX ((),sm)) /. 1 = (SgmX ((),sm)) . 1 by ;
then (SgmX ((),sm)) /. 1 in rng (SgmX ((),sm)) by ;
then (SgmX ((),sm)) /. 1 = b by
.= (SgmX ((),sm)) /. u by ;
hence contradiction by A10, A14, A18, A22, PRE_POLY:def 2; :: thesis: verum
end;
for u being object st u in {1} holds
u in dom (SgmX ((),sm)) by ;
then A24: dom (SgmX ((),sm)) = Seg 1 by ;
then A25: 1 in dom (SgmX ((),sm)) by ;
(SgmX ((),sm)) /. 1 = (SgmX ((),sm)) . 1 by ;
then (SgmX ((),sm)) /. 1 in rng (SgmX ((),sm)) by ;
then A26: (SgmX ((),sm)) /. 1 = b by ;
A27: len (SgmX ((),sm)) = 1 by ;
dom y = Seg (len y) by FINSEQ_1:def 3
.= dom (SgmX ((),sm)) by ;
then y . 1 = y /. 1 by
.= ((m * (SgmX ((),sm))) /. 1) * (eval (b,x)) by A26, A1, A3, A27 ;
then y = <*(() * (eval (b,x)))*> by ;
hence eval (m,x) = () * (eval (b,x)) by
.= () * (eval ((term m),x)) by ;
:: thesis: verum
end;
case A28: m . b = 0. L ; :: thesis: eval (m,x) = () * (eval ((term m),x))
A29: Support m = {}
proof
assume Support m <> {} ; :: thesis: contradiction
then reconsider sm = Support m as non empty Subset of (Bags n) ;
set c = the Element of sm;
m . the Element of sm <> 0. L by POLYNOM1:def 4;
hence contradiction by A4, A28; :: thesis: verum
end;
then ( term m = EmptyBag n & m . () = 0. L ) by ;
then A30: (coefficient m) * (eval ((term m),x)) = 0. L ;
consider y being FinSequence of the carrier of L such that
A31: len y = len (SgmX ((),())) and
A32: eval (m,x) = Sum y and
for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((m * (SgmX ((),()))) /. i) * (eval (((SgmX ((),())) /. i),x)) by POLYNOM2:def 4;
BagOrder n linearly_orders Support m by POLYNOM2:18;
then rng (SgmX ((),())) = {} by ;
then SgmX ((),()) = {} by RELAT_1:41;
then y = <*> the carrier of L by A31;
hence eval (m,x) = () * (eval ((term m),x)) by ; :: thesis: verum
end;
end;
end;
hence eval (m,x) = () * (eval ((term m),x)) ; :: thesis: verum