:: The Ring of Polynomials
:: by Robert Milewski
::
:: Received April 17, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users

theorem Th1: :: POLYNOM3:1

for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being FinSequence of the carrier of L st ( for i being Element of NAT st i in dom p holds
p . i = 0. L ) holds
Sum p = 0. L

proof end;

theorem Th2: :: POLYNOM3:2

for V being non empty Abelian add-associative right_zeroed addLoopStr
for p being FinSequence of the carrier of V holds Sum p = Sum (Rev p)

proof end;

theorem Th3: :: POLYNOM3:3

for p being FinSequence of REAL holds Sum p = Sum (Rev p)

proof end;

theorem Th4: :: POLYNOM3:4

for p being FinSequence of NAT
for i being Element of NAT st i in dom p holds
Sum p >= p . i

proof end;

definition

let D be non empty set ;
let i be Element of NAT ;
let p be FinSequence of D;
:: original: Del
redefine func Del (p,i) -> FinSequence of D;
coherence
Del (p,i) is FinSequence of D by FINSEQ_3:105;

end;

definition

let D be non empty set ;
let a, b be Element of D;
:: original: <*
redefine func <*a,b*> -> Element of 2 -tuples_on D;
coherence
<*a,b*> is Element of 2 -tuples_on D by FINSEQ_2:101;

end;

definition

let D be non empty set ;
let k, n be Element of NAT ;
let p be Element of k -tuples_on D;
let q be Element of n -tuples_on D;
:: original: ^
redefine func p ^ q -> Element of (k + n) -tuples_on D;
coherence
p ^ q is Element of (k + n) -tuples_on D

proof end;

end;

definition

let D be non empty set ;
let k, n be Nat;
let p be FinSequence of k -tuples_on D;
let q be FinSequence of n -tuples_on D;
:: original: ^^
redefine func p ^^ q -> Element of ((k + n) -tuples_on D) * ;
coherence
p ^^ q is Element of ((k + n) -tuples_on D) *

proof end;

end;

scheme :: POLYNOM3:sch 1
SeqOfSeqLambdaD{ F₁() -> non empty set , F₂() -> Element of NAT , F₃( Nat) -> Element of NAT , F₄( set , set ) -> Element of F₁() } :

ex p being FinSequence of F₁() * st
( len p = F₂() & ( for k being Element of NAT st k in Seg F₂() holds
( len (p /. k) = F₃(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F₄(k,n) ) ) ) )

proof end;

definition

let n be Nat;
let p, q be Element of n -tuples_on NAT;

pred p < q means :: POLYNOM3:def 1
ex i being Element of NAT st
( i in Seg n & p . i < q . i & ( for k being Nat st 1 <= k & k < i holds
p . k = q . k ) );

asymmetry
for p, q being Element of n -tuples_on NAT st ex i being Element of NAT st
( i in Seg n & p . i < q . i & ( for k being Nat st 1 <= k & k < i holds
p . k = q . k ) ) holds
for i being Element of NAT holds
( not i in Seg n or not q . i < p . i or ex k being Nat st
( 1 <= k & k < i & not q . k = p . k ) )

proof end;

end;

:: deftheorem defines < POLYNOM3:def 1 :
for n being Nat
for p, q being Element of n -tuples_on NAT holds
( p < q iff ex i being Element of NAT st
( i in Seg n & p . i < q . i & ( for k being Nat st 1 <= k & k < i holds
p . k = q . k ) ) );

notation

let n be Element of NAT ;
let p, q be Element of n -tuples_on NAT;
synonym q > p for p < q;

end;

definition

let n be Element of NAT ;
let p, q be Element of n -tuples_on NAT;

pred p <= q means :: POLYNOM3:def 2
( p < q or p = q );

reflexivity
for p being Element of n -tuples_on NAT holds
( p < p or p = p ) ;

end;

:: deftheorem defines <= POLYNOM3:def 2 :
for n being Element of NAT
for p, q being Element of n -tuples_on NAT holds
( p <= q iff ( p < q or p = q ) );

notation

let n be Element of NAT ;
let p, q be Element of n -tuples_on NAT;
synonym q >= p for p <= q;

end;

theorem Th5: :: POLYNOM3:5

for n being Element of NAT
for p, q, r being Element of n -tuples_on NAT holds
( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) )

proof end;

theorem Th6: :: POLYNOM3:6

for n being Nat
for p, q being Element of n -tuples_on NAT st p <> q holds
ex i being Element of NAT st
( i in Seg n & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds
p . k = q . k ) )

proof end;

theorem Th7: :: POLYNOM3:7

for n being Element of NAT
for p, q being Element of n -tuples_on NAT holds
( p <= q or p > q )

proof end;

definition

let n be Element of NAT ;

func TuplesOrder n -> Order of (n -tuples_on NAT) means :Def3: :: POLYNOM3:def 3
for p, q being Element of n -tuples_on NAT holds
( [p,q] in it iff p <= q );

existence
ex b₁ being Order of (n -tuples_on NAT) st
for p, q being Element of n -tuples_on NAT holds
( [p,q] in b₁ iff p <= q )

proof end;

uniqueness
for b₁, b₂ being Order of (n -tuples_on NAT) st ( for p, q being Element of n -tuples_on NAT holds
( [p,q] in b₁ iff p <= q ) ) & ( for p, q being Element of n -tuples_on NAT holds
( [p,q] in b₂ iff p <= q ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines TuplesOrder POLYNOM3:def 3 :
for n being Element of NAT
for b₂ being Order of (n -tuples_on NAT) holds
( b₂ = TuplesOrder n iff for p, q being Element of n -tuples_on NAT holds
( [p,q] in b₂ iff p <= q ) );

registration

let n be Element of NAT ;

cluster TuplesOrder n -> being_linear-order ;

coherence
TuplesOrder n is being_linear-order

proof end;

end;

definition

let i be non zero Element of NAT ;
let n be Element of NAT ;

func Decomp (n,i) -> FinSequence of i -tuples_on NAT means :Def4: :: POLYNOM3:def 4
ex A being finite Subset of (i -tuples_on NAT) st
( it = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) );

existence
ex b₁ being FinSequence of i -tuples_on NAT ex A being finite Subset of (i -tuples_on NAT) st
( b₁ = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of i -tuples_on NAT st ex A being finite Subset of (i -tuples_on NAT) st
( b₁ = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) & ex A being finite Subset of (i -tuples_on NAT) st
( b₂ = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Decomp POLYNOM3:def 4 :
for i being non zero Element of NAT
for n being Element of NAT
for b₃ being FinSequence of i -tuples_on NAT holds
( b₃ = Decomp (n,i) iff ex A being finite Subset of (i -tuples_on NAT) st
( b₃ = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) );

registration

let i be non zero Element of NAT ;
let n be Element of NAT ;

cluster Decomp (n,i) -> one-to-one non empty FinSequence-yielding ;

coherence
( not Decomp (n,i) is empty & Decomp (n,i) is one-to-one & Decomp (n,i) is FinSequence-yielding )

proof end;

end;

theorem Th8: :: POLYNOM3:8

for n being Element of NAT holds len (Decomp (n,1)) = 1

proof end;

theorem Th9: :: POLYNOM3:9

for n being Element of NAT holds len (Decomp (n,2)) = n + 1

proof end;

theorem :: POLYNOM3:10

for n being Element of NAT holds Decomp (n,1) = <*<*n*>*>

proof end;

theorem Th11: :: POLYNOM3:11

for i, j, n, k1, k2 being Element of NAT st (Decomp (n,2)) . i = <*k1,(n -' k1)*> & (Decomp (n,2)) . j = <*k2,(n -' k2)*> holds
( i < j iff k1 < k2 )

proof end;

theorem Th12: :: POLYNOM3:12

for i, n, k1, k2 being Element of NAT st (Decomp (n,2)) . i = <*k1,(n -' k1)*> & (Decomp (n,2)) . (i + 1) = <*k2,(n -' k2)*> holds
k2 = k1 + 1

proof end;

theorem Th13: :: POLYNOM3:13

for n being Element of NAT holds (Decomp (n,2)) . 1 = <*0,n*>

proof end;

theorem Th14: :: POLYNOM3:14

for n, i being Element of NAT st i in Seg (n + 1) holds
(Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*>

proof end;

definition

let L be non empty multMagma ;
let p, q, r be sequence of L;
let t be FinSequence of 3 -tuples_on NAT;

func prodTuples (p,q,r,t) -> Element of the carrier of L * means :Def5: :: POLYNOM3:def 5
( len it = len t & ( for k being Element of NAT st k in dom t holds
it . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) );

existence
ex b₁ being Element of the carrier of L * st
( len b₁ = len t & ( for k being Element of NAT st k in dom t holds
b₁ . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) )

proof end;

uniqueness
for b₁, b₂ being Element of the carrier of L * st len b₁ = len t & ( for k being Element of NAT st k in dom t holds
b₁ . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) & len b₂ = len t & ( for k being Element of NAT st k in dom t holds
b₂ . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines prodTuples POLYNOM3:def 5 :
for L being non empty multMagma
for p, q, r being sequence of L
for t being FinSequence of 3 -tuples_on NAT
for b₆ being Element of the carrier of L * holds
( b₆ = prodTuples (p,q,r,t) iff ( len b₆ = len t & ( for k being Element of NAT st k in dom t holds
b₆ . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) ) );

theorem Th15: :: POLYNOM3:15

for L being non empty multMagma
for p, q, r being sequence of L
for t being FinSequence of 3 -tuples_on NAT
for P being Permutation of (dom t)
for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds
prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P

proof end;

theorem Th16: :: POLYNOM3:16

for D being set
for f being FinSequence of D *
for i being Nat holds Card (f | i) = (Card f) | i

proof end;

theorem :: POLYNOM3:17

canceled;

::$CT

theorem Th17: :: POLYNOM3:18

for p being FinSequence of NAT
for i, j being Nat st i <= j holds
Sum (p | i) <= Sum (p | j)

proof end;

theorem :: POLYNOM3:19

canceled;

::$CT

theorem Th19: :: POLYNOM3:20

for p being FinSequence of REAL
for i being Element of NAT st i < len p holds
Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1))

proof end;

theorem Th20: :: POLYNOM3:21

for p being FinSequence of NAT
for i, j, k1, k2 being Element of NAT st i < len p & j < len p & 1 <= k1 & 1 <= k2 & k1 <= p . (i + 1) & k2 <= p . (j + 1) & (Sum (p | i)) + k1 = (Sum (p | j)) + k2 holds
( i = j & k1 = k2 )

proof end;

theorem Th21: :: POLYNOM3:22

for D1, D2 being set
for f1 being FinSequence of D1 *
for f2 being FinSequence of D2 *
for i1, i2, j1, j2 being Element of NAT st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds
( i1 = i2 & j1 = j2 )

proof end;

definition

let L be non empty ZeroStr ;
mode Polynomial of L is AlgSequence of L;

end;

theorem :: POLYNOM3:23

for L being non empty ZeroStr
for p being Polynomial of L
for n being Element of NAT holds
( n >= len p iff n is_at_least_length_of p ) by ALGSEQ_1:8, XXREAL_0:2, ALGSEQ_1:def 3;

scheme :: POLYNOM3:sch 2
PolynomialLambdaF{ F₁() -> non empty addLoopStr , F₂() -> Element of NAT , F₃( Element of NAT ) -> Element of F₁() } :

ex p being Polynomial of F₁() st
( len p <= F₂() & ( for n being Element of NAT st n < F₂() holds
p . n = F₃(n) ) )

proof end;

registration

let L be non empty right_zeroed addLoopStr ;
let p, q be Polynomial of L;

cluster p + q -> finite-Support ;

coherence
p + q is finite-Support

proof end;

end;

theorem :: POLYNOM3:24

for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of L
for n being Element of NAT st n is_at_least_length_of p & n is_at_least_length_of q holds
n is_at_least_length_of p + q

proof end;

definition

let L be non empty Abelian addLoopStr ;
let p, q be sequence of L;
:: original: +
redefine func p + q -> Element of bool [:NAT, the carrier of L:];
commutativity
for p, q being sequence of L holds p + q = q + p

proof end;

end;

theorem :: POLYNOM3:25

canceled;

::$CT

theorem Th24: :: POLYNOM3:26

for L being non empty add-associative addLoopStr
for p, q, r being sequence of L holds (p + q) + r = p + (q + r)

proof end;

registration

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

cluster - p -> finite-Support ;

coherence
- p is finite-Support

proof end;

end;

Lm1: for L being non empty addLoopStr
for p, q being sequence of L holds p - q = p + (- q)

proof end;

definition

let L be non empty addLoopStr ;
let p, q be sequence of L;

redefine func p - q equals :: POLYNOM3:def 6
p + (- q);

compatibility
for b₁ being Element of bool [:NAT, the carrier of L:] holds
( b₁ = p - q iff b₁ = p + (- q) ) by Lm1;

end;

:: deftheorem defines - POLYNOM3:def 6 :
for L being non empty addLoopStr
for p, q being sequence of L holds p - q = p + (- q);

registration

let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p, q be Polynomial of L;

cluster p - q -> finite-Support ;

coherence
p - q is finite-Support ;

end;

theorem :: POLYNOM3:27

for L being non empty addLoopStr
for p, q being sequence of L
for n being Element of NAT holds (p - q) . n = (p . n) - (q . n) by NORMSP_1:def 3;

definition

let L be non empty ZeroStr ;

func 0_. L -> sequence of L equals :: POLYNOM3:def 7
NAT --> (0. L);

coherence
NAT --> (0. L) is sequence of L ;

end;

:: deftheorem defines 0_. POLYNOM3:def 7 :
for L being non empty ZeroStr holds 0_. L = NAT --> (0. L);

registration

let L be non empty ZeroStr ;

cluster 0_. L -> finite-Support ;

coherence
0_. L is finite-Support

proof end;

end;

theorem Th26: :: POLYNOM3:28

for L being non empty right_zeroed addLoopStr
for p being sequence of L holds p + (0_. L) = p

proof end;

theorem Th27: :: POLYNOM3:29

for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being sequence of L holds p - p = 0_. L

proof end;

definition

let L be non empty multLoopStr_0 ;

func 1_. L -> sequence of L equals :: POLYNOM3:def 8
(0_. L) +* (0,(1. L));

coherence
(0_. L) +* (0,(1. L)) is sequence of L ;

end;

:: deftheorem defines 1_. POLYNOM3:def 8 :
for L being non empty multLoopStr_0 holds 1_. L = (0_. L) +* (0,(1. L));

registration

let L be non empty multLoopStr_0 ;

cluster 1_. L -> finite-Support ;

coherence
1_. L is finite-Support

proof end;

end;

theorem Th28: :: POLYNOM3:30

for L being non empty multLoopStr_0 holds
( (1_. L) . 0 = 1. L & ( for n being Nat st n <> 0 holds
(1_. L) . n = 0. L ) )

proof end;

definition

let L be non empty doubleLoopStr ;
let p, q be sequence of L;

func p *' q -> sequence of L means :Def9: :: POLYNOM3:def 9
for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & it . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) );

existence
ex b₁ being sequence of L st
for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & b₁ . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) )

proof end;

uniqueness
for b₁, b₂ being sequence of L st ( for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & b₁ . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) & ( for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & b₂ . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines *' POLYNOM3:def 9 :
for L being non empty doubleLoopStr
for p, q, b₄ being sequence of L holds
( b₄ = p *' q iff for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & b₄ . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) );

registration

let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ;
let p, q be Polynomial of L;

cluster p *' q -> finite-Support ;

coherence
p *' q is finite-Support

proof end;

end;

theorem Th29: :: POLYNOM3:31

for L being non empty right_complementable Abelian add-associative right_zeroed right-distributive doubleLoopStr
for p, q, r being sequence of L holds p *' (q + r) = (p *' q) + (p *' r)

proof end;

theorem Th30: :: POLYNOM3:32

for L being non empty right_complementable Abelian add-associative right_zeroed left-distributive doubleLoopStr
for p, q, r being sequence of L holds (p + q) *' r = (p *' r) + (q *' r)

proof end;

theorem Th31: :: POLYNOM3:33

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for p, q, r being sequence of L holds (p *' q) *' r = p *' (q *' r)

proof end;

definition

let L be non empty Abelian add-associative right_zeroed commutative doubleLoopStr ;
let p, q be sequence of L;
:: original: *'
redefine func p *' q -> sequence of L;
commutativity
for p, q being sequence of L holds p *' q = q *' p

proof end;

end;

theorem :: POLYNOM3:34

for L being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for p being sequence of L holds p *' (0_. L) = 0_. L

proof end;

theorem Th33: :: POLYNOM3:35

for L being non empty right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr
for p being sequence of L holds p *' (1_. L) = p

proof end;

definition

let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ;

func Polynom-Ring L -> non empty strict doubleLoopStr means :Def10: :: POLYNOM3:def 10
( ( for x being set holds
( x in the carrier of it iff x is Polynomial of L ) ) & ( for x, y being Element of it
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of it
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. it = 0_. L & 1. it = 1_. L );

existence
ex b₁ being non empty strict doubleLoopStr st
( ( for x being set holds
( x in the carrier of b₁ iff x is Polynomial of L ) ) & ( for x, y being Element of b₁
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₁
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b₁ = 0_. L & 1. b₁ = 1_. L )

proof end;

uniqueness
for b₁, b₂ being non empty strict doubleLoopStr st ( for x being set holds
( x in the carrier of b₁ iff x is Polynomial of L ) ) & ( for x, y being Element of b₁
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₁
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b₁ = 0_. L & 1. b₁ = 1_. L & ( for x being set holds
( x in the carrier of b₂ iff x is Polynomial of L ) ) & ( for x, y being Element of b₂
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₂
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b₂ = 0_. L & 1. b₂ = 1_. L holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines Polynom-Ring POLYNOM3:def 10 :
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for b₂ being non empty strict doubleLoopStr holds
( b₂ = Polynom-Ring L iff ( ( for x being set holds
( x in the carrier of b₂ iff x is Polynomial of L ) ) & ( for x, y being Element of b₂
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₂
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. b₂ = 0_. L & 1. b₂ = 1_. L ) );

registration

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

cluster Polynom-Ring L -> non empty strict Abelian ;

coherence
Polynom-Ring L is Abelian

proof end;

end;

registration

let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ;

cluster Polynom-Ring L -> non empty strict add-associative ;

coherence
Polynom-Ring L is add-associative

proof end;

cluster Polynom-Ring L -> non empty strict right_zeroed ;

coherence
Polynom-Ring L is right_zeroed

proof end;

cluster Polynom-Ring L -> non empty right_complementable strict ;

coherence
Polynom-Ring L is right_complementable

proof end;

end;

registration

let L be non empty right_complementable Abelian add-associative right_zeroed distributive commutative doubleLoopStr ;

cluster Polynom-Ring L -> non empty strict commutative ;

coherence
Polynom-Ring L is commutative

proof end;

end;

registration

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

cluster Polynom-Ring L -> non empty strict associative ;

coherence
Polynom-Ring L is associative

proof end;

end;

theorem Th33a: :: POLYNOM3:36

for L being non empty right_complementable add-associative right_zeroed left-distributive well-unital doubleLoopStr
for p being sequence of L holds (1_. L) *' p = p

proof end;

Lm2: now :: thesis: for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for x, e being Element of (Polynom-Ring L) st e = 1. (Polynom-Ring L) holds
( x * e = x & e * x = x )

let L be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for x, e being Element of (Polynom-Ring L) st e = 1. (Polynom-Ring L) holds
( x * e = x & e * x = x )
set Pm = Polynom-Ring L;
let x, e be Element of (Polynom-Ring L); :: thesis: ( e = 1. (Polynom-Ring L) implies ( x * e = x & e * x = x ) )
reconsider p = x as Polynomial of L by Def10;
assume A1: e = 1. (Polynom-Ring L) ; :: thesis: ( x * e = x & e * x = x )
A2: 1. (Polynom-Ring L) = 1_. L by Def10;
hence x * e = p *' (1_. L) by A1, Def10
.= x by Th33 ;
:: thesis: e * x = x
thus e * x = (1_. L) *' p by A1, A2, Def10
.= x by Th33a ; :: thesis: verum

end;

registration

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

cluster Polynom-Ring L -> non empty strict well-unital ;

coherence
Polynom-Ring L is well-unital by Lm2;

end;

registration

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

cluster Polynom-Ring L -> non empty strict distributive ;

coherence
Polynom-Ring L is distributive

proof end;

end;

theorem :: POLYNOM3:37

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr holds 1. (Polynom-Ring L) = 1_. L by Def10;