set n = {} ;
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of {},L
for x being Function of {},L holds eval (p,x) = p . (EmptyBag {})
let p be Polynomial of {},L; :: thesis: for x being Function of {},L holds eval (p,x) = p . (EmptyBag {})
let x be Function of {},L; :: thesis: eval (p,x) = p . (EmptyBag {})
A1: for b being bag of {} holds b = {}

proof

let b be bag of {} ; :: thesis: b = {}
b in Bags {} by PRE_POLY:def 12;
hence b = {} by PRE_POLY:51, TARSKI:def 1; :: thesis: verum

end;

then A2: EmptyBag {} = {} ;
consider a being Element of L such that
A3: p = {(EmptyBag {})} --> a by Lm1;
A4: EmptyBag {} in {(EmptyBag {})} by TARSKI:def 1;
then A5: p . (EmptyBag {}) = a by A3, FUNCOP_1:7;
A6: dom p = {(EmptyBag {})} by A3, FUNCOP_1:13;

now

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

case A7: a = 0. L ; :: thesis: eval (p,x) = a

Support p = {}

proof

set u = the Element of Support p;
assume A8: Support p <> {} ; :: thesis: contradiction
then the Element of Support p in Support p ;
then reconsider u = the Element of Support p as Element of Bags {} ;
p . u <> 0. L by A8, POLYNOM1:def 3;
hence contradiction by A1, A2, A5, A7; :: thesis: verum

end;

then reconsider Sp = Support p as empty Subset of (Bags {}) ;
consider y being FinSequence of the carrier of L such that
A9: len y = len (SgmX ((BagOrder {}),(Support p))) and
A10: eval (p,x) = Sum y and
for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((BagOrder {}),(Support p)))) /. i) * (eval ((((SgmX ((BagOrder {}),(Support p))) /. i) @),x)) by POLYNOM2:def 4;
SgmX ((BagOrder {}),Sp) = {} by POLYNOM2:7, POLYNOM2:18;
then y = <*> the carrier of L by A9;
hence eval (p,x) = a by A7, A10, RLVECT_1:43; :: thesis: verum

end;

case A11: a <> 0. L ; :: thesis: eval (p,x) = a

reconsider sp = Support p as finite Subset of (Bags {}) ;
set sg = SgmX ((BagOrder {}),sp);
A12: BagOrder {} linearly_orders sp by POLYNOM2:18;
A13: for u being set st u in Support p holds
u in {{}}

proof

let u be set ; :: thesis: ( u in Support p implies u in {{}} )
assume u in Support p ; :: thesis: u in {{}}
then reconsider u = u as Element of Bags {} ;
u = {} by A1;
hence u in {{}} by TARSKI:def 1; :: thesis: verum

end;

for u being set st u in {{}} holds
u in Support p

proof

let u be set ; :: thesis: ( u in {{}} implies u in Support p )
assume u in {{}} ; :: thesis: u in Support p
then u = EmptyBag {} by A2, TARSKI:def 1;
hence u in Support p by A5, A11, POLYNOM1:def 3; :: thesis: verum

end;

then Support p = {{}} by A13, TARSKI:1;
then A14: rng (SgmX ((BagOrder {}),sp)) = {{}} by A12, PRE_POLY:def 2;
then A15: {} in rng (SgmX ((BagOrder {}),sp)) by TARSKI:def 1;
then A16: 1 in dom (SgmX ((BagOrder {}),sp)) by FINSEQ_3:31;
then (SgmX ((BagOrder {}),sp)) . 1 in dom p by A2, A6, A14, FUNCT_1:3;
then 1 in dom (p * (SgmX ((BagOrder {}),sp))) by A16, FUNCT_1:11;
then A17: (p * (SgmX ((BagOrder {}),sp))) /. 1 = (p * (SgmX ((BagOrder {}),sp))) . 1 by PARTFUN1:def 6
.= p . ((SgmX ((BagOrder {}),sp)) . 1) by A16, FUNCT_1:13
.= a by A2, A3, A14, A16, FUNCOP_1:7, FUNCT_1:3 ;
A18: for u being set st u in dom (SgmX ((BagOrder {}),sp)) holds
u in {1}

proof

let u be set ; :: thesis: ( u in dom (SgmX ((BagOrder {}),sp)) implies u in {1} )
assume A19: u in dom (SgmX ((BagOrder {}),sp)) ; :: thesis: u in {1}
assume A20: not u in {1} ; :: thesis: contradiction
reconsider u = u as Element of NAT by A19;
(SgmX ((BagOrder {}),sp)) /. u = (SgmX ((BagOrder {}),sp)) . u by A19, PARTFUN1:def 6;
then A21: (SgmX ((BagOrder {}),sp)) /. u in rng (SgmX ((BagOrder {}),sp)) by A19, FUNCT_1:3;
A22: u <> 1 by A20, TARSKI:def 1;
A23: 1 < u

proof

consider k being Nat such that
A24: dom (SgmX ((BagOrder {}),sp)) = 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 ex m9 being Element of NAT st
( m9 = u & 1 <= m9 & m9 <= k ) by A19, A24;
hence 1 < u by A22, XXREAL_0:1; :: thesis: verum

end;

(SgmX ((BagOrder {}),sp)) /. 1 = (SgmX ((BagOrder {}),sp)) . 1 by A15, A19, FINSEQ_3:31, PARTFUN1:def 6;
then (SgmX ((BagOrder {}),sp)) /. 1 in rng (SgmX ((BagOrder {}),sp)) by A16, FUNCT_1:3;
then (SgmX ((BagOrder {}),sp)) /. 1 = {} by A14, TARSKI:def 1
.= (SgmX ((BagOrder {}),sp)) /. u by A14, A21, TARSKI:def 1 ;
hence contradiction by A12, A16, A19, A23, PRE_POLY:def 2; :: thesis: verum

end;

for u being set st u in {1} holds
u in dom (SgmX ((BagOrder {}),sp)) by A16, TARSKI:def 1;
then dom (SgmX ((BagOrder {}),sp)) = Seg 1 by A18, FINSEQ_1:2, TARSKI:1;
then A25: len (SgmX ((BagOrder {}),sp)) = 1 by FINSEQ_1:def 3;
consider y being FinSequence of the carrier of L such that
A26: len y = len (SgmX ((BagOrder {}),sp)) and
A27: Sum y = eval (p,x) and
A28: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((BagOrder {}),sp))) /. i) * (eval ((((SgmX ((BagOrder {}),sp)) /. i) @),x)) by POLYNOM2:def 4;
dom y = Seg (len y) by FINSEQ_1:def 3
.= dom (SgmX ((BagOrder {}),sp)) by A26, FINSEQ_1:def 3 ;
then y . 1 = y /. 1 by A15, FINSEQ_3:31, PARTFUN1:def 6
.= ((p * (SgmX ((BagOrder {}),sp))) /. 1) * (eval ((((SgmX ((BagOrder {}),sp)) /. 1) @),x)) by A25, A26, A28
.= ((p * (SgmX ((BagOrder {}),sp))) /. 1) * (eval ((EmptyBag {}),x)) by A1, A2
.= ((p * (SgmX ((BagOrder {}),sp))) /. 1) * (1. L) by POLYNOM2:14
.= a by A17, VECTSP_1:def 4 ;
then y = <*a*> by A25, A26, FINSEQ_1:40;
hence eval (p,x) = a by A27, RLVECT_1:44; :: thesis: verum

end;

end;

end;

hence eval (p,x) = p . (EmptyBag {}) by A3, A4, FUNCOP_1:7; :: thesis: verum