:: POLYNOM2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

scheme :: POLYNOM2:sch 1
SeqExD{ F1() -> non empty set , F2() -> Nat, P1[ set , set ] } :
ex p being FinSequence of F1() st
( dom p = Seg F2() & ( for k being Nat st k in Seg F2() holds
P1[k,p /. k] ) )
provided
A1: for k being Nat st k in Seg F2() holds
ex x being Element of F1() st P1[k,x]
proof end;

scheme :: POLYNOM2:sch 2
FinRecExD2{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Nat, P1[ set , set , set ] } :
ex p being FinSequence of F1() st
( len p = F3() & ( p /. 1 = F2() or F3() = 0 ) & ( for n being Nat st 1 <= n & n <= F3() - 1 holds
P1[n,p /. n,p /. (n + 1)] ) )
provided
A1: for n being Nat st 1 <= n & n <= F3() - 1 holds
for x being Element of F1() ex y being Element of F1() st P1[n,x,y]
proof end;

scheme :: POLYNOM2:sch 3
FinRecUnD2{ F1() -> set , F2() -> Element of F1(), F3() -> Nat, F4() -> FinSequence of F1(), F5() -> FinSequence of F1(), P1[ set , set , set ] } :
F4() = F5()
provided
A1: for n being Nat st 1 <= n & n <= F3() - 1 holds
for x, y1, y2 being Element of F1() st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2 and
A2: ( len F4() = F3() & ( F4() /. 1 = F2() or F3() = 0 ) & ( for n being Nat st 1 <= n & n <= F3() - 1 holds
P1[n,F4() /. n,F4() /. (n + 1)] ) ) and
A3: ( len F5() = F3() & ( F5() /. 1 = F2() or F3() = 0 ) & ( for n being Nat st 1 <= n & n <= F3() - 1 holds
P1[n,F5() /. n,F5() /. (n + 1)] ) )
proof end;

scheme :: POLYNOM2:sch 4
FinInd{ F1() -> Nat, F2() -> Nat, P1[ Nat] } :
for i being Nat st F1() <= i & i <= F2() holds
P1[i]
provided
A1: P1[F1()] and
A2: for j being Nat st F1() <= j & j < F2() & P1[j] holds
P1[j + 1]
proof end;

scheme :: POLYNOM2:sch 5
FinInd2{ F1() -> Nat, F2() -> Nat, P1[ Nat] } :
for i being Nat st F1() <= i & i <= F2() holds
P1[i]
provided
A1: P1[F1()] and
A2: for j being Nat st F1() <= j & j < F2() & ( for j' being Nat st F1() <= j' & j' <= j holds
P1[j'] ) holds
P1[j + 1]
proof end;

scheme :: POLYNOM2:sch 6
IndFinSeq{ F1() -> set , F2() -> FinSequence of F1(), P1[ set ] } :
for i being Nat st 1 <= i & i <= len F2() holds
P1[F2() . i]
provided
A1: P1[F2() . 1] and
A2: for i being Nat st 1 <= i & i < len F2() & P1[F2() . i] holds
P1[F2() . (i + 1)]
proof end;

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_linear-order holds
R linearly_orders S
proof end;

theorem :: POLYNOM2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: POLYNOM2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital associative HGrStr
for a being Element of L
for n, m being Nat holds (power L) . a,(n + m) = ((power L) . a,n) * ((power L) . a,m)
proof end;

registration
cluster non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive non trivial doubleLoopStr ;
existence
ex b1 being non empty doubleLoopStr st
( b1 is Abelian & b1 is right_zeroed & b1 is add-associative & b1 is right_complementable & b1 is unital & b1 is distributive & b1 is commutative & b1 is associative & not b1 is trivial )
proof end;
end;

theorem :: POLYNOM2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th4: :: POLYNOM2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for k being Nat st k in dom p holds
for i being Nat st 1 <= i & i <= k holds
i in dom p
proof end;

Lm4: for X being set
for A being finite Subset of X
for a being Element of X
for R being Order of X st R linearly_orders {a} \/ A holds
R linearly_orders A
proof end;

theorem Th5: :: POLYNOM2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty right_zeroed left_zeroed LoopStr
for p being FinSequence of the carrier of L
for i being Nat st i in dom p & ( for i' being Nat st i' in dom p & i' <> i holds
p /. i' = 0. L ) holds
Sum p = p /. i
proof end;

theorem :: POLYNOM2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr
for p being FinSequence of the carrier of L st ex i being Nat st
( i in dom p & p /. i = 0. L ) holds
Product p = 0. L
proof end;

theorem Th7: :: POLYNOM2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty Abelian add-associative LoopStr
for a being Element of L
for p, q being FinSequence of the carrier of L st len p = len q & ex i being Nat st
( i in dom p & q /. i = a + (p /. i) & ( for i' being Nat st i' in dom p & i' <> i holds
q /. i' = p /. i' ) ) holds
Sum q = a + (Sum p)
proof end;

theorem Th8: :: POLYNOM2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Nat st
( i in dom p & q /. i = a * (p /. i) & ( for i' being Nat st i' in dom p & i' <> i holds
q /. i' = p /. i' ) ) holds
Product q = a * (Product p)
proof end;

theorem Th9: :: POLYNOM2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being empty Subset of X
for R being Order of X st R linearly_orders A holds
SgmX R,A = {}
proof end;

theorem Th10: :: POLYNOM2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
for i, j being Nat st i in dom (SgmX R,A) & j in dom (SgmX R,A) & (SgmX R,A) /. i = (SgmX R,A) /. j holds
i = j
proof end;

Lm5: for D being set
for p being FinSequence of D st dom p <> {} holds
1 in dom p
proof end;

theorem Th11: :: POLYNOM2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being finite Subset of X
for a being Element of X st not a in A holds
for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Nat st k in dom (SgmX R,B) & (SgmX R,B) /. k = a holds
for i being Nat st 1 <= i & i <= k - 1 holds
(SgmX R,B) /. i = (SgmX R,A) /. i
proof end;

theorem Th12: :: POLYNOM2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being finite Subset of X
for a being Element of X st not a in A holds
for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Nat st k in dom (SgmX R,B) & (SgmX R,B) /. k = a holds
for i being Nat st k <= i & i <= len (SgmX R,A) holds
(SgmX R,B) /. (i + 1) = (SgmX R,A) /. i
proof end;

theorem Th13: :: POLYNOM2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for A being finite Subset of X
for a being Element of X st not a in A holds
for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Nat st k + 1 in dom (SgmX R,B) & (SgmX R,B) /. (k + 1) = a holds
SgmX R,B = Ins (SgmX R,A),k,a
proof end;

theorem Th14: :: POLYNOM2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for b being bag of X st support b = {} holds
b = EmptyBag X
proof end;

Lm6: for X being set
for b being bag of X holds b is PartFunc of X, NAT
proof end;

definition
let X be set ;
let b be bag of X;
attr b is empty means :Def1: :: POLYNOM2:def 1
b = EmptyBag X;
end;

:: deftheorem Def1 defines empty POLYNOM2:def 1 :
for X being set
for b being bag of X holds
( b is empty iff b = EmptyBag X );

registration
let X be non empty set ;
cluster non empty M28(X);
existence
not for b1 being bag of X holds b1 is empty
proof end;
end;

definition
let X be set ;
let b be bag of X;
:: original: support
redefine func support b -> finite Subset of X;
coherence
support b is finite Subset of X
proof end;
end;

theorem Th15: :: POLYNOM2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for b being bag of n holds RelIncl n linearly_orders support b
proof end;

definition
let X be set ;
let x be FinSequence of X;
let b be bag of X;
:: original: *
redefine func b * x -> PartFunc of NAT , NAT ;
coherence
x * b is PartFunc of NAT , NAT
proof end;
end;

definition
let n be Ordinal;
let b be bag of n;
let L be non empty unital non trivial doubleLoopStr ;
let x be Function of n,L;
func eval b,x -> Element of L means :Def2: :: 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 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 b1 being Element of L ex y being FinSequence of the carrier of L st
( len y = len (SgmX (RelIncl n),(support b)) & b1 = Product y & ( for i being 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) ) )
proof end;
uniqueness
for b1, b2 being Element of L st ex y being FinSequence of the carrier of L st
( len y = len (SgmX (RelIncl n),(support b)) & b1 = Product y & ( for i being 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)) & b2 = Product y & ( for i being 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
b1 = b2
proof end;
end;

:: deftheorem Def2 defines eval POLYNOM2:def 2 :
for n being Ordinal
for b being bag of n
for L being non empty unital non trivial doubleLoopStr
for x being Function of n,L
for b5 being Element of L holds
( b5 = eval b,x iff ex y being FinSequence of the carrier of L st
( len y = len (SgmX (RelIncl n),(support b)) & b5 = Product y & ( for i being 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) ) ) );

Lm7: for X being set holds support (EmptyBag X) = {}
proof end;

theorem Th16: :: POLYNOM2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being non empty unital non trivial doubleLoopStr
for x being Function of n,L holds eval (EmptyBag n),x = 1. L
proof end;

theorem Th17: :: POLYNOM2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being non empty unital non trivial 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;

Lm8: for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable unital associative commutative distributive non trivial doubleLoopStr
for b1, b2 being bag of n
for u being set st not u in support b1 & support b2 = (support b1) \/ {u} & ( for u' being set st u' <> u holds
b2 . u' = b1 . u' ) 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;

Lm9: for n being Ordinal
for L being non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive non trivial 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 Th18: :: POLYNOM2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive non trivial 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 add-associative right_zeroed right_complementable LoopStr ;
let p, q be Polynomial of n,L;
cluster p - q -> finite-Support ;
coherence
p - q is finite-Support
proof end;
end;

theorem Th19: :: POLYNOM2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
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 empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr ;
let p be Polynomial of n,L;
cluster Support p -> finite ;
coherence
Support p is finite
by POLYNOM1:def 10;
end;

theorem Th20: :: POLYNOM2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for p being Polynomial of n,L holds BagOrder n linearly_orders Support p
proof end;

definition
let n be Ordinal;
let b be Element of Bags n;
func b @ -> bag of n equals :: POLYNOM2:def 3
b;
correctness
coherence
b is bag of n
;
;
end;

:: deftheorem defines @ POLYNOM2:def 3 :
for n being Ordinal
for b being Element of Bags n holds b @ = b;

definition
let n be Ordinal;
let L be non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr ;
let p be Polynomial of n,L;
let x be Function of n,L;
func eval p,x -> Element of L means :Def4: :: 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 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 b1 being Element of L ex y being FinSequence of the carrier of L st
( len y = len (SgmX (BagOrder n),(Support p)) & b1 = Sum y & ( for i being 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) ) )
proof end;
uniqueness
for b1, b2 being Element of L st ex y being FinSequence of the carrier of L st
( len y = len (SgmX (BagOrder n),(Support p)) & b1 = Sum y & ( for i being 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)) & b2 = Sum y & ( for i being 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
b1 = b2
proof end;
end;

:: deftheorem Def4 defines eval POLYNOM2:def 4 :
for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for p being Polynomial of n,L
for x being Function of n,L
for b5 being Element of L holds
( b5 = eval p,x iff ex y being FinSequence of the carrier of L st
( len y = len (SgmX (BagOrder n),(Support p)) & b5 = Sum y & ( for i being 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) ) ) );

theorem Th21: :: POLYNOM2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable unital distributive non trivial 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 Th22: :: POLYNOM2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for x being Function of n,L holds eval (0_ n,L),x = 0. L
proof end;

theorem Th23: :: POLYNOM2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for x being Function of n,L holds eval (1_ n,L),x = 1. L
proof end;

theorem Th24: :: POLYNOM2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for p being Polynomial of n,L
for x being Function of n,L holds eval (- p),x = - (eval p,x)
proof end;

Lm10: for n being Ordinal
for L being non empty Abelian add-associative right_zeroed right_complementable unital distributive non trivial 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 b' being bag of n st b' <> b holds
q . b' = p . b' ) holds
eval q,x = (eval p,x) + ((q . b) * (eval b,x))
proof end;

Lm11: for n being Ordinal
for L being non empty Abelian add-associative right_zeroed right_complementable unital distributive non trivial 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 Th25: :: POLYNOM2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being non empty Abelian add-associative right_zeroed right_complementable unital distributive non trivial 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:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being non empty Abelian add-associative right_zeroed right_complementable unital distributive non trivial 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;

Lm12: for n being Ordinal
for L being non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive non trivial 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;

Lm13: for n being Ordinal
for L being non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive non trivial 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 Th27: :: POLYNOM2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Ordinal
for L being non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive non trivial 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 empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr ;
let x be Function of n,L;
func Polynom-Evaluation n,L,x -> Function of (Polynom-Ring n,L),L means :Def5: :: POLYNOM2:def 5
for p being Polynomial of n,L holds it . p = eval p,x;
existence
ex b1 being Function of (Polynom-Ring n,L),L st
for p being Polynomial of n,L holds b1 . p = eval p,x
proof end;
uniqueness
for b1, b2 being Function of (Polynom-Ring n,L),L st ( for p being Polynomial of n,L holds b1 . p = eval p,x ) & ( for p being Polynomial of n,L holds b2 . p = eval p,x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Polynom-Evaluation POLYNOM2:def 5 :
for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for x being Function of n,L
for b4 being Function of (Polynom-Ring n,L),L holds
( b4 = Polynom-Evaluation n,L,x iff for p being Polynomial of n,L holds b4 . p = eval p,x );

registration
let n be Ordinal;
let L be non empty Abelian add-associative right_zeroed right_complementable unital associative distributive non trivial doubleLoopStr ;
cluster Polynom-Ring n,L -> unital ;
coherence
Polynom-Ring n,L is unital
;
end;

registration
let n be Ordinal;
let L be non empty Abelian add-associative right_zeroed right_complementable unital associative distributive non trivial doubleLoopStr ;
let x be Function of n,L;
cluster Polynom-Evaluation n,L,x -> unity-preserving ;
coherence
Polynom-Evaluation n,L,x is unity-preserving
proof end;
end;

registration
let n be Ordinal;
let L be non empty Abelian add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr ;
let x be Function of n,L;
cluster Polynom-Evaluation n,L,x -> additive ;
coherence
Polynom-Evaluation n,L,x is additive
proof end;
end;

registration
let n be Ordinal;
let L be non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive non trivial doubleLoopStr ;
let x be Function of n,L;
cluster Polynom-Evaluation n,L,x -> additive unity-preserving multiplicative ;
coherence
Polynom-Evaluation n,L,x is multiplicative
proof end;
end;

registration
let n be Ordinal;
let L be non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive non trivial doubleLoopStr ;
let x be Function of n,L;
cluster Polynom-Evaluation n,L,x -> RingHomomorphism additive unity-preserving multiplicative ;
coherence
Polynom-Evaluation n,L,x is RingHomomorphism
proof end;
end;