:: by Christoph Schwarzweller and Andrzej Trybulec

::

:: Received April 14, 2000

:: Copyright (c) 2000-2016 Association of Mizar Users

Lm1: for X being set

for A being Subset of X

for O being Order of X holds

( O is_reflexive_in A & O is_antisymmetric_in A & O is_transitive_in A )

proof end;

Lm2: for X being set

for A being Subset of X

for O being Order of X st O is_connected_in X holds

O is_connected_in A

proof end;

Lm3: for X being set

for S being Subset of X

for R being Order of X st R is being_linear-order holds

R linearly_orders S

proof end;

theorem Th1: :: POLYNOM2:1

for L being non empty unital associative multMagma

for a being Element of L

for n, m being Element of NAT holds (power L) . (a,(n + m)) = ((power L) . (a,n)) * ((power L) . (a,m))

for a being Element of L

for n, m being Element of NAT holds (power L) . (a,(n + m)) = ((power L) . (a,n)) * ((power L) . (a,m))

proof end;

registration

ex b_{1} being non trivial doubleLoopStr st

( b_{1} is Abelian & b_{1} is right_zeroed & b_{1} is add-associative & b_{1} is right_complementable & b_{1} is well-unital & b_{1} is distributive & b_{1} is commutative & b_{1} is associative )
end;

cluster non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive for doubleLoopStr ;

existence ex b

( b

proof end;

::$CT

theorem Th2: :: POLYNOM2:3

for L being non empty right_zeroed left_zeroed addLoopStr

for p being FinSequence of the carrier of L

for i being Element of NAT st i in dom p & ( for i9 being Element of NAT st i9 in dom p & i9 <> i holds

p /. i9 = 0. L ) holds

Sum p = p /. i

for p being FinSequence of the carrier of L

for i being Element of NAT st i in dom p & ( for i9 being Element of NAT st i9 in dom p & i9 <> i holds

p /. i9 = 0. L ) holds

Sum p = p /. i

proof end;

theorem :: POLYNOM2:4

for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for p being FinSequence of the carrier of L st ex i being Element of NAT st

( i in dom p & p /. i = 0. L ) holds

Product p = 0. L

for p being FinSequence of the carrier of L st ex i being Element of NAT st

( i in dom p & p /. i = 0. L ) holds

Product p = 0. L

proof end;

theorem Th4: :: POLYNOM2:5

for L being non empty Abelian add-associative addLoopStr

for a being Element of L

for p, q being FinSequence of the carrier of L st len p = len q & ex i being Element of NAT st

( i in dom p & q /. i = a + (p /. i) & ( for i9 being Element of NAT st i9 in dom p & i9 <> i holds

q /. i9 = p /. i9 ) ) holds

Sum q = a + (Sum p)

for a being Element of L

for p, q being FinSequence of the carrier of L st len p = len q & ex i being Element of NAT st

( i in dom p & q /. i = a + (p /. i) & ( for i9 being Element of NAT st i9 in dom p & i9 <> i holds

q /. i9 = p /. i9 ) ) holds

Sum q = a + (Sum p)

proof end;

theorem Th5: :: POLYNOM2:6

for L being non empty associative commutative doubleLoopStr

for a being Element of L

for p, q being FinSequence of the carrier of L st len p = len q & ex i being Element of NAT st

( i in dom p & q /. i = a * (p /. i) & ( for i9 being Element of NAT st i9 in dom p & i9 <> i holds

q /. i9 = p /. i9 ) ) holds

Product q = a * (Product p)

for a being Element of L

for p, q being FinSequence of the carrier of L st len p = len q & ex i being Element of NAT st

( i in dom p & q /. i = a * (p /. i) & ( for i9 being Element of NAT st i9 in dom p & i9 <> i holds

q /. i9 = p /. i9 ) ) holds

Product q = a * (Product p)

proof end;

definition

let n be Ordinal;

let b be bag of n;

let L be non trivial well-unital doubleLoopStr ;

let x be Function of n,L;

ex b_{1} being Element of L ex y being FinSequence of the carrier of L st

( len y = len (SgmX ((RelIncl n),(support b))) & b_{1} = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds

y /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) ) )

for b_{1}, b_{2} being Element of L st ex y being FinSequence of the carrier of L st

( len y = len (SgmX ((RelIncl n),(support b))) & b_{1} = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds

y /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) ) ) & ex y being FinSequence of the carrier of L st

( len y = len (SgmX ((RelIncl n),(support b))) & b_{2} = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds

y /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) ) ) holds

b_{1} = b_{2}

end;
let b be bag of n;

let L be non trivial well-unital doubleLoopStr ;

let x be Function of n,L;

func eval (b,x) -> Element of L means :Def1: :: POLYNOM2:def 2

ex y being FinSequence of the carrier of L st

( len y = len (SgmX ((RelIncl n),(support b))) & it = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds

y /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) ) );

existence ex y being FinSequence of the carrier of L st

( len y = len (SgmX ((RelIncl n),(support b))) & it = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds

y /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) ) );

ex b

( len y = len (SgmX ((RelIncl n),(support b))) & b

y /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) ) )

proof end;

uniqueness for b

( len y = len (SgmX ((RelIncl n),(support b))) & b

y /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) ) ) & ex y being FinSequence of the carrier of L st

( len y = len (SgmX ((RelIncl n),(support b))) & b

y /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) ) ) holds

b

proof end;

:: deftheorem Def1 defines eval POLYNOM2:def 2 :

for n being Ordinal

for b being bag of n

for L being non trivial well-unital doubleLoopStr

for x being Function of n,L

for b_{5} being Element of L holds

( b_{5} = eval (b,x) iff ex y being FinSequence of the carrier of L st

( len y = len (SgmX ((RelIncl n),(support b))) & b_{5} = Product y & ( for i being Element of NAT st 1 <= i & i <= len y holds

y /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) ) ) );

for n being Ordinal

for b being bag of n

for L being non trivial well-unital doubleLoopStr

for x being Function of n,L

for b

( b

( len y = len (SgmX ((RelIncl n),(support b))) & b

y /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) ) ) );

::$CT 7

theorem Th6: :: POLYNOM2:14

for n being Ordinal

for L being non trivial well-unital doubleLoopStr

for x being Function of n,L holds eval ((EmptyBag n),x) = 1. L

for L being non trivial well-unital doubleLoopStr

for x being Function of n,L holds eval ((EmptyBag n),x) = 1. L

proof end;

theorem Th7: :: POLYNOM2:15

for n being Ordinal

for L being non trivial well-unital doubleLoopStr

for u being set

for b being bag of n st support b = {u} holds

for x being Function of n,L holds eval (b,x) = (power L) . ((x . u),(b . u))

for L being non trivial well-unital doubleLoopStr

for u being set

for b being bag of n st support b = {u} holds

for x being Function of n,L holds eval (b,x) = (power L) . ((x . u),(b . u))

proof end;

Lm4: for n being Ordinal

for L being non empty non trivial right_complementable associative commutative add-associative right_zeroed well-unital distributive doubleLoopStr

for b1, b2 being bag of n

for u being object st not u in support b1 & support b2 = (support b1) \/ {u} & ( for u9 being object st u9 <> u holds

b2 . u9 = b1 . u9 ) holds

for x being Function of n,L

for a being Element of L st a = (power L) . ((x . u),(b2 . u)) holds

eval (b2,x) = a * (eval (b1,x))

proof end;

Lm5: for n being Ordinal

for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for b1 being bag of n st ex u being set st support b1 = {u} holds

for b2 being bag of n

for x being Function of n,L holds eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x))

proof end;

theorem Th8: :: POLYNOM2:16

for n being Ordinal

for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for b1, b2 being bag of n

for x being Function of n,L holds eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x))

for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for b1, b2 being bag of n

for x being Function of n,L holds eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x))

proof end;

registration

let n be Ordinal;

let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p, q be Polynomial of n,L;

coherence

p - q is finite-Support

end;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;

let p, q be Polynomial of n,L;

coherence

p - q is finite-Support

proof end;

theorem Th9: :: POLYNOM2:17

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for n being Ordinal

for p being Polynomial of n,L st Support p = {} holds

p = 0_ (n,L)

for n being Ordinal

for p being Polynomial of n,L st Support p = {} holds

p = 0_ (n,L)

proof end;

registration

let n be Ordinal;

let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;

let p be Polynomial of n,L;

coherence

Support p is finite by POLYNOM1:def 5;

end;
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;

let p be Polynomial of n,L;

coherence

Support p is finite by POLYNOM1:def 5;

theorem Th10: :: POLYNOM2:18

for n being Ordinal

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of n,L holds BagOrder n linearly_orders Support p

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of n,L holds BagOrder n linearly_orders Support p

proof end;

definition

let n be Ordinal;

let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;

let p be Polynomial of n,L;

let x be Function of n,L;

ex b_{1} being Element of L ex y being FinSequence of the carrier of L st

( len y = len (SgmX ((BagOrder n),(Support p))) & b_{1} = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds

y /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) )

for b_{1}, b_{2} being Element of L st ex y being FinSequence of the carrier of L st

( len y = len (SgmX ((BagOrder n),(Support p))) & b_{1} = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds

y /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) & ex y being FinSequence of the carrier of L st

( len y = len (SgmX ((BagOrder n),(Support p))) & b_{2} = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds

y /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) holds

b_{1} = b_{2}

end;
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;

let p be Polynomial of n,L;

let x be Function of n,L;

func eval (p,x) -> Element of L means :Def2: :: POLYNOM2:def 4

ex y being FinSequence of the carrier of L st

( len y = len (SgmX ((BagOrder n),(Support p))) & it = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds

y /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) );

existence ex y being FinSequence of the carrier of L st

( len y = len (SgmX ((BagOrder n),(Support p))) & it = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds

y /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) );

ex b

( len y = len (SgmX ((BagOrder n),(Support p))) & b

y /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) )

proof end;

uniqueness for b

( len y = len (SgmX ((BagOrder n),(Support p))) & b

y /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) & ex y being FinSequence of the carrier of L st

( len y = len (SgmX ((BagOrder n),(Support p))) & b

y /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) holds

b

proof end;

:: deftheorem Def2 defines eval POLYNOM2:def 4 :

for n being Ordinal

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of n,L

for x being Function of n,L

for b_{5} being Element of L holds

( b_{5} = eval (p,x) iff ex y being FinSequence of the carrier of L st

( len y = len (SgmX ((BagOrder n),(Support p))) & b_{5} = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds

y /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) );

for n being Ordinal

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of n,L

for x being Function of n,L

for b

( b

( len y = len (SgmX ((BagOrder n),(Support p))) & b

y /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) );

theorem Th11: :: POLYNOM2:19

for n being Ordinal

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of n,L

for b being bag of n st Support p = {b} holds

for x being Function of n,L holds eval (p,x) = (p . b) * (eval (b,x))

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of n,L

for b being bag of n st Support p = {b} holds

for x being Function of n,L holds eval (p,x) = (p . b) * (eval (b,x))

proof end;

theorem Th12: :: POLYNOM2:20

for n being Ordinal

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for x being Function of n,L holds eval ((0_ (n,L)),x) = 0. L

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for x being Function of n,L holds eval ((0_ (n,L)),x) = 0. L

proof end;

theorem Th13: :: POLYNOM2:21

for n being Ordinal

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for x being Function of n,L holds eval ((1_ (n,L)),x) = 1. L

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for x being Function of n,L holds eval ((1_ (n,L)),x) = 1. L

proof end;

theorem Th14: :: POLYNOM2:22

for n being Ordinal

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of n,L

for x being Function of n,L holds eval ((- p),x) = - (eval (p,x))

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of n,L

for x being Function of n,L holds eval ((- p),x) = - (eval (p,x))

proof end;

Lm6: for n being Ordinal

for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for p, q being Polynomial of n,L

for x being Function of n,L

for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b9 being bag of n st b9 <> b holds

q . b9 = p . b9 ) holds

eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x)))

proof end;

Lm7: for n being Ordinal

for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for p being Polynomial of n,L st ex b being bag of n st Support p = {b} holds

for q being Polynomial of n,L

for x being Function of n,L holds eval ((p + q),x) = (eval (p,x)) + (eval (q,x))

proof end;

theorem Th15: :: POLYNOM2:23

for n being Ordinal

for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for p, q being Polynomial of n,L

for x being Function of n,L holds eval ((p + q),x) = (eval (p,x)) + (eval (q,x))

for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for p, q being Polynomial of n,L

for x being Function of n,L holds eval ((p + q),x) = (eval (p,x)) + (eval (q,x))

proof end;

theorem :: POLYNOM2:24

for n being Ordinal

for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for p, q being Polynomial of n,L

for x being Function of n,L holds eval ((p - q),x) = (eval (p,x)) - (eval (q,x))

for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for p, q being Polynomial of n,L

for x being Function of n,L holds eval ((p - q),x) = (eval (p,x)) - (eval (q,x))

proof end;

Lm8: for n being Ordinal

for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for p, q being Polynomial of n,L

for b1, b2 being bag of n st Support p = {b1} & Support q = {b2} holds

for x being Function of n,L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))

proof end;

Lm9: for n being Ordinal

for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for q being Polynomial of n,L st ex b being bag of n st Support q = {b} holds

for p being Polynomial of n,L

for x being Function of n,L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))

proof end;

theorem Th17: :: POLYNOM2:25

for n being Ordinal

for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for p, q being Polynomial of n,L

for x being Function of n,L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))

for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr

for p, q being Polynomial of n,L

for x being Function of n,L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))

proof end;

definition

let n be Ordinal;

let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;

let x be Function of n,L;

ex b_{1} being Function of (Polynom-Ring (n,L)),L st

for p being Polynomial of n,L holds b_{1} . p = eval (p,x)

for b_{1}, b_{2} being Function of (Polynom-Ring (n,L)),L st ( for p being Polynomial of n,L holds b_{1} . p = eval (p,x) ) & ( for p being Polynomial of n,L holds b_{2} . p = eval (p,x) ) holds

b_{1} = b_{2}

end;
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;

let x be Function of n,L;

func Polynom-Evaluation (n,L,x) -> Function of (Polynom-Ring (n,L)),L means :Def3: :: POLYNOM2:def 5

for p being Polynomial of n,L holds it . p = eval (p,x);

existence for p being Polynomial of n,L holds it . p = eval (p,x);

ex b

for p being Polynomial of n,L holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines Polynom-Evaluation POLYNOM2:def 5 :

for n being Ordinal

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for x being Function of n,L

for b_{4} being Function of (Polynom-Ring (n,L)),L holds

( b_{4} = Polynom-Evaluation (n,L,x) iff for p being Polynomial of n,L holds b_{4} . p = eval (p,x) );

for n being Ordinal

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for x being Function of n,L

for b

( b

registration

let n be Ordinal;

let L be non empty non trivial right_complementable associative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ;

coherence

Polynom-Ring (n,L) is well-unital ;

end;
let L be non empty non trivial right_complementable associative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ;

coherence

Polynom-Ring (n,L) is well-unital ;

registration

let n be Ordinal;

let L be non empty non trivial right_complementable associative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ;

let x be Function of n,L;

coherence

Polynom-Evaluation (n,L,x) is unity-preserving

end;
let L be non empty non trivial right_complementable associative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ;

let x be Function of n,L;

coherence

Polynom-Evaluation (n,L,x) is unity-preserving

proof end;

registration

let n be Ordinal;

let L be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ;

let x be Function of n,L;

coherence

Polynom-Evaluation (n,L,x) is additive

end;
let L be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ;

let x be Function of n,L;

coherence

Polynom-Evaluation (n,L,x) is additive

proof end;

registration

let n be Ordinal;

let L be non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ;

let x be Function of n,L;

coherence

Polynom-Evaluation (n,L,x) is multiplicative

end;
let L be non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ;

let x be Function of n,L;

coherence

Polynom-Evaluation (n,L,x) is multiplicative

proof end;

registration

let n be Ordinal;

let L be non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ;

let x be Function of n,L;

coherence

Polynom-Evaluation (n,L,x) is RingHomomorphism ;

end;
let L be non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ;

let x be Function of n,L;

coherence

Polynom-Evaluation (n,L,x) is RingHomomorphism ;