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 . ()

let p be Polynomial of {},L; :: thesis: for x being Function of {},L holds eval (p,x) = p . ()
let x be Function of {},L; :: thesis: eval (p,x) = p . ()
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 ; :: thesis: verum
end;
then A2: EmptyBag {} = {} ;
consider a being Element of L such that
A3: p = {()} --> a by Lm1;
A4: p . () = a by A3;
A5: dom p = {()} by A3;
now :: thesis: ( ( a = 0. L & eval (p,x) = a ) or ( a <> 0. L & eval (p,x) = a ) )
per cases ( a = 0. L or a <> 0. L ) ;
case A6: a = 0. L ; :: thesis: eval (p,x) = a
Support p = {}
proof
set u = the Element of Support p;
assume A7: 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 ;
hence contradiction by A1, A2, A4, A6; :: thesis: verum
end;
then reconsider Sp = Support p as empty Subset of () ;
consider y being FinSequence of the carrier of L such that
A8: len y = len (SgmX ((),())) and
A9: eval (p,x) = Sum y and
for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((),()))) /. i) * (eval (((SgmX ((),())) /. i),x)) by POLYNOM2:def 4;
SgmX ((),Sp) = {} by ;
then y = <*> the carrier of L by A8;
hence eval (p,x) = a by ; :: thesis: verum
end;
case A10: a <> 0. L ; :: thesis: eval (p,x) = a
reconsider sp = Support p as finite Subset of () ;
set sg = SgmX ((),sp);
A11: BagOrder {} linearly_orders sp by POLYNOM2:18;
A12: for u being object st u in Support p holds
u in
proof
let u be object ; :: thesis: ( u in Support p implies u in )
assume u in Support p ; :: thesis:
then reconsider u = u as Element of Bags {} ;
u = {} by A1;
hence u in by TARSKI:def 1; :: thesis: verum
end;
for u being object st u in holds
u in Support p
proof
let u be object ; :: thesis: ( u in implies u in Support p )
assume u in ; :: thesis:
then u = EmptyBag {} by ;
hence u in Support p by ; :: thesis: verum
end;
then Support p = by ;
then A13: rng (SgmX ((),sp)) = by ;
then A14: {} in rng (SgmX ((),sp)) by TARSKI:def 1;
then A15: 1 in dom (SgmX ((),sp)) by FINSEQ_3:31;
then (SgmX ((),sp)) . 1 in dom p by ;
then 1 in dom (p * (SgmX ((),sp))) by ;
then A16: (p * (SgmX ((),sp))) /. 1 = (p * (SgmX ((),sp))) . 1 by PARTFUN1:def 6
.= p . ((SgmX ((),sp)) . 1) by
.= a by ;
A17: for u being object st u in dom (SgmX ((),sp)) holds
u in {1}
proof
let u be object ; :: thesis: ( u in dom (SgmX ((),sp)) implies u in {1} )
assume A18: u in dom (SgmX ((),sp)) ; :: thesis: u in {1}
assume A19: not u in {1} ; :: thesis: contradiction
reconsider u = u as Element of NAT by A18;
(SgmX ((),sp)) /. u = (SgmX ((),sp)) . u by ;
then A20: (SgmX ((),sp)) /. u in rng (SgmX ((),sp)) by ;
A21: u <> 1 by ;
A22: 1 < u
proof
consider k being Nat such that
A23: dom (SgmX ((),sp)) = Seg k by FINSEQ_1:def 2;
Seg k = { m where m is Nat : ( 1 <= m & m <= 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 ((),sp)) /. 1 = (SgmX ((),sp)) . 1 by ;
then (SgmX ((),sp)) /. 1 in rng (SgmX ((),sp)) by ;
then (SgmX ((),sp)) /. 1 = {} by
.= (SgmX ((),sp)) /. u by ;
hence contradiction by A11, A15, A18, A22, PRE_POLY:def 2; :: thesis: verum
end;
for u being object st u in {1} holds
u in dom (SgmX ((),sp)) by ;
then dom (SgmX ((),sp)) = Seg 1 by ;
then A24: len (SgmX ((),sp)) = 1 by FINSEQ_1:def 3;
consider y being FinSequence of the carrier of L such that
A25: len y = len (SgmX ((),sp)) and
A26: Sum y = eval (p,x) and
A27: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((),sp))) /. i) * (eval (((SgmX ((),sp)) /. i),x)) by POLYNOM2:def 4;
dom y = Seg (len y) by FINSEQ_1:def 3
.= dom (SgmX ((),sp)) by ;
then y . 1 = y /. 1 by
.= ((p * (SgmX ((),sp))) /. 1) * (eval (((SgmX ((),sp)) /. 1),x)) by
.= ((p * (SgmX ((),sp))) /. 1) * (eval ((),x)) by A1, A2
.= ((p * (SgmX ((),sp))) /. 1) * (1. L) by POLYNOM2:14
.= a by A16 ;
then y = <*a*> by ;
hence eval (p,x) = a by ; :: thesis: verum
end;
end;
end;
hence eval (p,x) = p . () by A3; :: thesis: verum