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 = {}

consider a being Element of L such that

A3: p = {(EmptyBag {})} --> a by Lm1;

A4: p . (EmptyBag {}) = a by A3;

A5: dom p = {(EmptyBag {})} by A3;

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

then A2:
EmptyBag {} = {}
;
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;b in Bags {} by PRE_POLY:def 12;

hence b = {} by PRE_POLY:51, TARSKI:def 1; :: thesis: verum

consider a being Element of L such that

A3: p = {(EmptyBag {})} --> a by Lm1;

A4: p . (EmptyBag {}) = a by A3;

A5: dom p = {(EmptyBag {})} by A3;

now :: thesis: ( ( a = 0. L & eval (p,x) = a ) or ( a <> 0. L & eval (p,x) = a ) )end;

hence
eval (p,x) = p . (EmptyBag {})
by A3; :: thesis: verumper cases
( a = 0. L or a <> 0. L )
;

end;

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

Support p = {}

consider y being FinSequence of the carrier of L such that

A8: len y = len (SgmX ((BagOrder {}),(Support p))) 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 ((BagOrder {}),(Support p)))) /. i) * (eval (((SgmX ((BagOrder {}),(Support p))) /. i),x)) by POLYNOM2:def 4;

SgmX ((BagOrder {}),Sp) = {} by POLYNOM2:18, PRE_POLY:76;

then y = <*> the carrier of L by A8;

hence eval (p,x) = a by A6, A9, RLVECT_1:43; :: thesis: verum

end;proof

then reconsider Sp = Support p as empty Subset of (Bags {}) ;
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 A7, POLYNOM1:def 4;

hence contradiction by A1, A2, A4, A6; :: thesis: verum

end;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 A7, POLYNOM1:def 4;

hence contradiction by A1, A2, A4, A6; :: thesis: verum

consider y being FinSequence of the carrier of L such that

A8: len y = len (SgmX ((BagOrder {}),(Support p))) 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 ((BagOrder {}),(Support p)))) /. i) * (eval (((SgmX ((BagOrder {}),(Support p))) /. i),x)) by POLYNOM2:def 4;

SgmX ((BagOrder {}),Sp) = {} by POLYNOM2:18, PRE_POLY:76;

then y = <*> the carrier of L by A8;

hence eval (p,x) = a by A6, A9, RLVECT_1:43; :: thesis: verum

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

reconsider sp = Support p as finite Subset of (Bags {}) ;

set sg = SgmX ((BagOrder {}),sp);

A11: BagOrder {} linearly_orders sp by POLYNOM2:18;

A12: for u being object st u in Support p holds

u in {{}}

u in Support p

then A13: rng (SgmX ((BagOrder {}),sp)) = {{}} by A11, PRE_POLY:def 2;

then A14: {} in rng (SgmX ((BagOrder {}),sp)) by TARSKI:def 1;

then A15: 1 in dom (SgmX ((BagOrder {}),sp)) by FINSEQ_3:31;

then (SgmX ((BagOrder {}),sp)) . 1 in dom p by A2, A5, A13, FUNCT_1:3;

then 1 in dom (p * (SgmX ((BagOrder {}),sp))) by A15, FUNCT_1:11;

then A16: (p * (SgmX ((BagOrder {}),sp))) /. 1 = (p * (SgmX ((BagOrder {}),sp))) . 1 by PARTFUN1:def 6

.= p . ((SgmX ((BagOrder {}),sp)) . 1) by A15, FUNCT_1:13

.= a by A2, A3, A13, A15, FUNCOP_1:7, FUNCT_1:3 ;

A17: for u being object st u in dom (SgmX ((BagOrder {}),sp)) holds

u in {1}

u in dom (SgmX ((BagOrder {}),sp)) by A15, TARSKI:def 1;

then dom (SgmX ((BagOrder {}),sp)) = Seg 1 by A17, FINSEQ_1:2, TARSKI:2;

then A24: len (SgmX ((BagOrder {}),sp)) = 1 by FINSEQ_1:def 3;

consider y being FinSequence of the carrier of L such that

A25: len y = len (SgmX ((BagOrder {}),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 ((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 A25, FINSEQ_1:def 3 ;

then y . 1 = y /. 1 by A14, FINSEQ_3:31, PARTFUN1:def 6

.= ((p * (SgmX ((BagOrder {}),sp))) /. 1) * (eval (((SgmX ((BagOrder {}),sp)) /. 1),x)) by A24, A25, A27

.= ((p * (SgmX ((BagOrder {}),sp))) /. 1) * (eval ((EmptyBag {}),x)) by A1, A2

.= ((p * (SgmX ((BagOrder {}),sp))) /. 1) * (1. L) by POLYNOM2:14

.= a by A16 ;

then y = <*a*> by A24, A25, FINSEQ_1:40;

hence eval (p,x) = a by A26, RLVECT_1:44; :: thesis: verum

end;set sg = SgmX ((BagOrder {}),sp);

A11: BagOrder {} linearly_orders sp by POLYNOM2:18;

A12: for u being object st u in Support p holds

u in {{}}

proof

for u being object st u in {{}} holds
let u be object ; :: 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;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

u in Support p

proof

then
Support p = {{}}
by A12, TARSKI:2;
let u be object ; :: 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 A4, A10, POLYNOM1:def 4; :: thesis: verum

end;assume u in {{}} ; :: thesis: u in Support p

then u = EmptyBag {} by A2, TARSKI:def 1;

hence u in Support p by A4, A10, POLYNOM1:def 4; :: thesis: verum

then A13: rng (SgmX ((BagOrder {}),sp)) = {{}} by A11, PRE_POLY:def 2;

then A14: {} in rng (SgmX ((BagOrder {}),sp)) by TARSKI:def 1;

then A15: 1 in dom (SgmX ((BagOrder {}),sp)) by FINSEQ_3:31;

then (SgmX ((BagOrder {}),sp)) . 1 in dom p by A2, A5, A13, FUNCT_1:3;

then 1 in dom (p * (SgmX ((BagOrder {}),sp))) by A15, FUNCT_1:11;

then A16: (p * (SgmX ((BagOrder {}),sp))) /. 1 = (p * (SgmX ((BagOrder {}),sp))) . 1 by PARTFUN1:def 6

.= p . ((SgmX ((BagOrder {}),sp)) . 1) by A15, FUNCT_1:13

.= a by A2, A3, A13, A15, FUNCOP_1:7, FUNCT_1:3 ;

A17: for u being object st u in dom (SgmX ((BagOrder {}),sp)) holds

u in {1}

proof

for u being object st u in {1} holds
let u be object ; :: thesis: ( u in dom (SgmX ((BagOrder {}),sp)) implies u in {1} )

assume A18: u in dom (SgmX ((BagOrder {}),sp)) ; :: thesis: u in {1}

assume A19: not u in {1} ; :: thesis: contradiction

reconsider u = u as Element of NAT by A18;

(SgmX ((BagOrder {}),sp)) /. u = (SgmX ((BagOrder {}),sp)) . u by A18, PARTFUN1:def 6;

then A20: (SgmX ((BagOrder {}),sp)) /. u in rng (SgmX ((BagOrder {}),sp)) by A18, FUNCT_1:3;

A21: u <> 1 by A19, TARSKI:def 1;

A22: 1 < u

then (SgmX ((BagOrder {}),sp)) /. 1 in rng (SgmX ((BagOrder {}),sp)) by A15, FUNCT_1:3;

then (SgmX ((BagOrder {}),sp)) /. 1 = {} by A13, TARSKI:def 1

.= (SgmX ((BagOrder {}),sp)) /. u by A13, A20, TARSKI:def 1 ;

hence contradiction by A11, A15, A18, A22, PRE_POLY:def 2; :: thesis: verum

end;assume A18: u in dom (SgmX ((BagOrder {}),sp)) ; :: thesis: u in {1}

assume A19: not u in {1} ; :: thesis: contradiction

reconsider u = u as Element of NAT by A18;

(SgmX ((BagOrder {}),sp)) /. u = (SgmX ((BagOrder {}),sp)) . u by A18, PARTFUN1:def 6;

then A20: (SgmX ((BagOrder {}),sp)) /. u in rng (SgmX ((BagOrder {}),sp)) by A18, FUNCT_1:3;

A21: u <> 1 by A19, TARSKI:def 1;

A22: 1 < u

proof

(SgmX ((BagOrder {}),sp)) /. 1 = (SgmX ((BagOrder {}),sp)) . 1
by A14, A18, FINSEQ_3:31, PARTFUN1:def 6;
consider k being Nat such that

A23: dom (SgmX ((BagOrder {}),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 A18, A23;

hence 1 < u by A21, XXREAL_0:1; :: thesis: verum

end;A23: dom (SgmX ((BagOrder {}),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 A18, A23;

hence 1 < u by A21, XXREAL_0:1; :: thesis: verum

then (SgmX ((BagOrder {}),sp)) /. 1 in rng (SgmX ((BagOrder {}),sp)) by A15, FUNCT_1:3;

then (SgmX ((BagOrder {}),sp)) /. 1 = {} by A13, TARSKI:def 1

.= (SgmX ((BagOrder {}),sp)) /. u by A13, A20, TARSKI:def 1 ;

hence contradiction by A11, A15, A18, A22, PRE_POLY:def 2; :: thesis: verum

u in dom (SgmX ((BagOrder {}),sp)) by A15, TARSKI:def 1;

then dom (SgmX ((BagOrder {}),sp)) = Seg 1 by A17, FINSEQ_1:2, TARSKI:2;

then A24: len (SgmX ((BagOrder {}),sp)) = 1 by FINSEQ_1:def 3;

consider y being FinSequence of the carrier of L such that

A25: len y = len (SgmX ((BagOrder {}),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 ((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 A25, FINSEQ_1:def 3 ;

then y . 1 = y /. 1 by A14, FINSEQ_3:31, PARTFUN1:def 6

.= ((p * (SgmX ((BagOrder {}),sp))) /. 1) * (eval (((SgmX ((BagOrder {}),sp)) /. 1),x)) by A24, A25, A27

.= ((p * (SgmX ((BagOrder {}),sp))) /. 1) * (eval ((EmptyBag {}),x)) by A1, A2

.= ((p * (SgmX ((BagOrder {}),sp))) /. 1) * (1. L) by POLYNOM2:14

.= a by A16 ;

then y = <*a*> by A24, A25, FINSEQ_1:40;

hence eval (p,x) = a by A26, RLVECT_1:44; :: thesis: verum