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


begin

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
proofend;

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)
proofend;

theorem Th3: :: POLYNOM3:3
for p being FinSequence of REAL holds Sum p = Sum (Rev p)
proofend;

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
proofend;

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 funcp ^ q ->  Element of (k + n) -tuples_on D;
coherence
 p ^ q is Element of (k + n) -tuples_on D
proofend;
end;

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

scheme :: POLYNOM3:sch 1
SeqOfSeqLambdaD{ F1() ->  non empty set , F2() ->  Element of NAT , F3( Element of NAT ) ->  Element of NAT , F4( set , set ) ->  Element of F1() } :
 ex p being FinSequence of F1() * st
( len p = F2() &amp; ( for k being Element of NAT st k in Seg F2() holds
( len (p /. k) = F3(k) &amp; ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F4(k,n) ) ) ) )
proofend;

begin

definition
let n be Element of NAT ;
let p, q be Element of n -tuples_on NAT;
predp < q means :Def1: :: POLYNOM3:def 1
 ex i being Element of NAT st
( i in Seg n &amp; p . i < q . i &amp; ( for k being Element of NAT st 1 <= k &amp; 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 &amp; p . i < q . i &amp; ( for k being Element of NAT st 1 <= k &amp; 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 Element of NAT st
( 1 <= k &amp; k < i &amp; not q . k = p . k ) )
proofend;
end;

:: deftheorem Def1 defines < POLYNOM3:def_1_:_
 for n being Element of 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 &amp; p . i < q . i &amp; ( for k being Element of NAT st 1 <= k &amp; 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;
predp <= q means :Def2: :: 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 Def2 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 &amp; q < r implies p < r ) &amp; ( ( ( p < q &amp; q <= r ) or ( p <= q &amp; q < r ) or ( p <= q &amp; q <= r ) ) implies p <= r ) )
proofend;

theorem Th6: :: POLYNOM3:6
for n being Element of 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 &amp; p . i <> q . i &amp; ( for k being Element of NAT st 1 <= k &amp; k < i holds
p . k = q . k ) )
proofend;

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 )
proofend;

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 b1 being Order of (n -tuples_on NAT) st
for p, q being Element of n -tuples_on NAT holds
( [p,q] in b1 iff p <= q )
proofend;
uniqueness
 for b1, b2 being Order of (n -tuples_on NAT) st ( for p, q being Element of n -tuples_on NAT holds
( [p,q] in b1 iff p <= q ) ) &amp; ( for p, q being Element of n -tuples_on NAT holds
( [p,q] in b2 iff p <= q ) ) holds
b1 = b2
proofend;
end;

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

registration
let n be Element of NAT ;
cluster TuplesOrder n ->  being_linear-order ;
coherence
 TuplesOrder n is being_linear-order
proofend;
end;

begin

definition
let i be non empty 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) &amp; ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) );
existence
 ex b1 being FinSequence of i -tuples_on NAT ex A being finite Subset of (i -tuples_on NAT) st
( b1 = SgmX ((TuplesOrder i),A) &amp; ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of i -tuples_on NAT st ex A being finite Subset of (i -tuples_on NAT) st
( b1 = SgmX ((TuplesOrder i),A) &amp; ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) &amp; ex A being finite Subset of (i -tuples_on NAT) st
( b2 = SgmX ((TuplesOrder i),A) &amp; ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines Decomp POLYNOM3:def_4_:_
 for i being non empty Element of NAT
for n being Element of NAT
for b3 being FinSequence of i -tuples_on NAT holds
( b3 = Decomp (n,i) iff ex A being finite Subset of (i -tuples_on NAT) st
( b3 = SgmX ((TuplesOrder i),A) &amp; ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) );

registration
let i be non empty 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 &amp; Decomp (n,i) is one-to-one &amp; Decomp (n,i) is FinSequence-yielding )
proofend;
end;

theorem Th8: :: POLYNOM3:8
for n being Element of NAT holds len (Decomp (n,1)) = 1
proofend;

theorem Th9: :: POLYNOM3:9
for n being Element of NAT holds len (Decomp (n,2)) = n + 1
proofend;

theorem :: POLYNOM3:10
for n being Element of NAT holds Decomp (n,1) = <*<*n*>*>
proofend;

theorem Th11: :: POLYNOM3:11
for i, j, n, k1, k2 being Element of NAT st (Decomp (n,2)) . i = <*k1,(n -' k1)*> &amp; (Decomp (n,2)) . j = <*k2,(n -' k2)*> holds
( i < j iff k1 < k2 )
proofend;

theorem Th12: :: POLYNOM3:12
for i, n, k1, k2 being Element of NAT st (Decomp (n,2)) . i = <*k1,(n -' k1)*> &amp; (Decomp (n,2)) . (i + 1) = <*k2,(n -' k2)*> holds
k2 = k1 + 1
proofend;

theorem Th13: :: POLYNOM3:13
for n being Element of NAT holds (Decomp (n,2)) . 1 = <*0,n*>
proofend;

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)*>
proofend;

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 &amp; ( 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 b1 being Element of the carrier of L * st
( len b1 = len t &amp; ( for k being Element of NAT st k in dom t holds
b1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) )
proofend;
uniqueness
 for b1, b2 being Element of the carrier of L * st len b1 = len t &amp; ( for k being Element of NAT st k in dom t holds
b1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) &amp; len b2 = len t &amp; ( for k being Element of NAT st k in dom t holds
b2 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) holds
b1 = b2
proofend;
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 b6 being Element of the carrier of L * holds
( b6 = prodTuples (p,q,r,t) iff ( len b6 = len t &amp; ( for k being Element of NAT st k in dom t holds
b6 . 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
proofend;

theorem Th16: :: POLYNOM3:16
for D being set
for f being FinSequence of D *
for i being Element of NAT holds Card (f | i) = (Card f) | i
proofend;

theorem :: POLYNOM3:17
for p being FinSequence of REAL
for q being FinSequence of NAT st p = q holds
for i being Element of NAT holds p | i = q | i ;

theorem Th18: :: POLYNOM3:18
for p being FinSequence of NAT
for i, j being Element of NAT st i <= j holds
Sum (p | i) <= Sum (p | j)
proofend;

theorem :: POLYNOM3:19
for D being set
for p being FinSequence of D
for i being Element of NAT st i < len p holds
p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> by FINSEQ_5:83;

theorem Th20: :: 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))
proofend;

theorem Th21: :: POLYNOM3:21
for p being FinSequence of NAT
for i, j, k1, k2 being Element of NAT st i < len p &amp; j < len p &amp; 1 <= k1 &amp; 1 <= k2 &amp; k1 <= p . (i + 1) &amp; k2 <= p . (j + 1) &amp; (Sum (p | i)) + k1 = (Sum (p | j)) + k2 holds
( i = j &amp; k1 = k2 )
proofend;

theorem Th22: :: 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 &amp; i2 in dom f2 &amp; j1 in dom (f1 . i1) &amp; j2 in dom (f2 . i2) &amp; Card f1 = Card f2 &amp; (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds
( i1 = i2 &amp; j1 = j2 )
proofend;

begin

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

theorem Th23: :: 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 )
proofend;

scheme :: POLYNOM3:sch 2
PolynomialLambdaF{ F1() ->  non empty addLoopStr , F2() ->  Element of NAT , F3( Element of NAT ) ->  Element of F1() } :
 ex p being Polynomial of F1() st
( len p <= F2() &amp; ( for n being Element of NAT st n < F2() holds
p . n = F3(n) ) )
proofend;

registration
let L be non empty right_zeroed addLoopStr ;
let p, q be Polynomial of L;
clusterp + q ->  finite-Support ;
coherence
 p + q is finite-Support
proofend;
end;

theorem Th24: :: 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 &amp; n is_at_least_length_of q holds
n is_at_least_length_of p + q
proofend;

theorem :: POLYNOM3:25
for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of L holds support (p + q) c= (support p) \/ (support q)
proofend;

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

theorem Th26: :: 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)
proofend;

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
proofend;
end;

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

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 b1 being Element of bool [:NAT, the carrier of L:] holds
( b1 = p - q iff b1 = 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;
clusterp - 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
proofend;
end;

theorem Th28: :: POLYNOM3:28
for L being non empty right_zeroed addLoopStr
for p being sequence of L holds p + (0_. L) = p
proofend;

theorem Th29: :: 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
proofend;

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
proofend;
end;

theorem Th30: :: POLYNOM3:30
for L being non empty multLoopStr_0 holds
( (1_. L) . 0 = 1. L &amp; ( for n being Nat st n <> 0 holds
(1_. L) . n = 0. L ) )
proofend;

definition
let L be non empty doubleLoopStr ;
let p, q be sequence of L;
funcp *' 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 &amp; it . i = Sum r &amp; ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) );
existence
 ex b1 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 &amp; b1 . i = Sum r &amp; ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) )
proofend;
uniqueness
 for b1, b2 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 &amp; b1 . i = Sum r &amp; ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) &amp; ( for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 &amp; b2 . i = Sum r &amp; ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines *' POLYNOM3:def_9_:_
 for L being non empty doubleLoopStr
for p, q, b4 being sequence of L holds
( b4 = p *' q iff for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 &amp; b4 . i = Sum r &amp; ( 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 distributive add-associative right_zeroed doubleLoopStr ;
let p, q be Polynomial of L;
clusterp *' q ->  finite-Support ;
coherence
 p *' q is finite-Support
proofend;
end;

theorem Th31: :: POLYNOM3:31
for L being non empty right_complementable right-distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being sequence of L holds p *' (q + r) = (p *' q) + (p *' r)
proofend;

theorem Th32: :: POLYNOM3:32
for L being non empty right_complementable left-distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being sequence of L holds (p + q) *' r = (p *' r) + (q *' r)
proofend;

definition
let n be Element of NAT ;
:: original:<*
redefine func<*n*> ->  Element of 1 -tuples_on NAT;
coherence
 <*n*> is Element of 1 -tuples_on NAT
proofend;
end;

theorem Th33: :: POLYNOM3:33
for L being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being sequence of L holds (p *' q) *' r = p *' (q *' r)
proofend;

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

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

theorem Th35: :: POLYNOM3:35
for L being non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr
for p being sequence of L holds p *' (1_. L) = p
proofend;

begin

definition
let L be non empty right_complementable distributive add-associative right_zeroed 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 ) ) &amp; ( for x, y being Element of it
for p, q being sequence of L st x = p &amp; y = q holds
x + y = p + q ) &amp; ( for x, y being Element of it
for p, q being sequence of L st x = p &amp; y = q holds
x * y = p *' q ) &amp; 0. it = 0_. L &amp; 1. it = 1_. L );
existence
 ex b1 being non empty strict doubleLoopStr st
( ( for x being set holds
( x in the carrier of b1 iff x is Polynomial of L ) ) &amp; ( for x, y being Element of b1
for p, q being sequence of L st x = p &amp; y = q holds
x + y = p + q ) &amp; ( for x, y being Element of b1
for p, q being sequence of L st x = p &amp; y = q holds
x * y = p *' q ) &amp; 0. b1 = 0_. L &amp; 1. b1 = 1_. L )
proofend;
uniqueness
 for b1, b2 being non empty strict doubleLoopStr st ( for x being set holds
( x in the carrier of b1 iff x is Polynomial of L ) ) &amp; ( for x, y being Element of b1
for p, q being sequence of L st x = p &amp; y = q holds
x + y = p + q ) &amp; ( for x, y being Element of b1
for p, q being sequence of L st x = p &amp; y = q holds
x * y = p *' q ) &amp; 0. b1 = 0_. L &amp; 1. b1 = 1_. L &amp; ( for x being set holds
( x in the carrier of b2 iff x is Polynomial of L ) ) &amp; ( for x, y being Element of b2
for p, q being sequence of L st x = p &amp; y = q holds
x + y = p + q ) &amp; ( for x, y being Element of b2
for p, q being sequence of L st x = p &amp; y = q holds
x * y = p *' q ) &amp; 0. b2 = 0_. L &amp; 1. b2 = 1_. L holds
b1 = b2
proofend;
end;

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

registration
let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring L ->  non empty strict Abelian ;
coherence
 Polynom-Ring L is Abelian
proofend;
end;

registration
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring L ->  non empty strict add-associative ;
coherence
 Polynom-Ring L is add-associative
proofend;
cluster Polynom-Ring L ->  non empty strict right_zeroed ;
coherence
 Polynom-Ring L is right_zeroed
proofend;
cluster Polynom-Ring L ->  non empty right_complementable strict ;
coherence
 Polynom-Ring L is right_complementable
proofend;
end;

registration
let L be non empty right_complementable commutative distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring L ->  non empty strict commutative ;
coherence
 Polynom-Ring L is commutative
proofend;
end;

registration
let L be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring L ->  non empty strict associative ;
coherence
 Polynom-Ring L is associative
proofend;
end;

Lm2: now__::_thesis:_for_L_being_non_empty_right_complementable_commutative_well-unital_distributive_Abelian_add-associative_right_zeroed_doubleLoopStr_
for_x,_e_being_Element_of_(Polynom-Ring_L)_st_e_=_1._(Polynom-Ring_L)_holds_
(_x_*_e_=_x_&amp;_e_*_x_=_x_)
let L be non empty right_complementable commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for x, e being Element of (Polynom-Ring L) st e = 1. (Polynom-Ring L) holds
( x * e = x &amp; 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 &amp; e * x = x ) )
reconsider p = x as Polynomial of L by Def10;
assume A1: e = 1. (Polynom-Ring L) ; ::_thesis: ( x * e = x &amp; e * x = x )
A2: 1. (Polynom-Ring L) = 1_. L by Def10;
hence x * e = p *' (1_. L) by A1, Def10
.= x by Th35 ;
::_thesis: e * x = x
thus e * x = p *' (1_. L) by A1, A2, Def10
.= x by Th35 ; ::_thesis: verum
end;

registration
let L be non empty right_complementable commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring L ->  non empty strict well-unital ;
coherence
 Polynom-Ring L is well-unital
proofend;
end;

registration
let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring L ->  non empty strict distributive ;
coherence
 Polynom-Ring L is distributive
proofend;
end;

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