:: Multivariate polynomials with arbitrary number of variables
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received September 22, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

registration
cluster non empty degenerated right_complementable right-distributive right_unital add-associative right_zeroed  ->  non empty trivial right_complementable right-distributive right_unital add-associative right_zeroed for doubleLoopStr ;
coherence
 for b1 being non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr st b1 is degenerated holds
b1 is trivial
proofend;
end;

registration
cluster non empty non trivial right_complementable right-distributive right_unital add-associative right_zeroed  ->  non empty non degenerated right_complementable right-distributive right_unital add-associative right_zeroed for doubleLoopStr ;
coherence
 for b1 being non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr st not b1 is trivial holds
not b1 is degenerated ;
end;

theorem Th1: :: POLYNOM1:1
for K being non empty addLoopStr
for p1, p2 being FinSequence of the carrier of K st dom p1 = dom p2 holds
dom (p1 + p2) = dom p1
proofend;

theorem Th2: :: POLYNOM1:2
for L being non empty addLoopStr
for F being FinSequence of the carrier of L * holds dom (Sum F) = dom F
proofend;

theorem Th3: :: POLYNOM1:3
for L being non empty addLoopStr
for F being FinSequence of the carrier of L * holds Sum (<*> ( the carrier of L *)) = <*> the carrier of L
proofend;

theorem Th4: :: POLYNOM1:4
for L being non empty addLoopStr
for p being Element of the carrier of L * holds <*(Sum p)*> = Sum <*p*>
proofend;

theorem Th5: :: POLYNOM1:5
for L being non empty addLoopStr
for F, G being FinSequence of the carrier of L * holds Sum (F ^ G) = (Sum F) ^ (Sum G)
proofend;

definition
let L be non empty multMagma ;
let p be FinSequence of the carrier of L;
let a be Element of L;
redefine func a * p means :Def1: :: POLYNOM1:def 1
( dom it = dom p &amp; ( for i being set st i in dom p holds
it /. i = a * (p /. i) ) );
compatibility
 for b1 being FinSequence of the carrier of L holds
( b1 = a * p iff ( dom b1 = dom p &amp; ( for i being set st i in dom p holds
b1 /. i = a * (p /. i) ) ) )
proofend;
end;

:: deftheorem Def1 defines * POLYNOM1:def_1_:_
 for L being non empty multMagma
for p being FinSequence of the carrier of L
for a being Element of L
for b4 being FinSequence of the carrier of L holds
( b4 = a * p iff ( dom b4 = dom p &amp; ( for i being set st i in dom p holds
b4 /. i = a * (p /. i) ) ) );

definition
let L be non empty multMagma ;
let p be FinSequence of the carrier of L;
let a be Element of L;
funcp * a ->  FinSequence of the carrier of L means :Def2: :: POLYNOM1:def 2
( dom it = dom p &amp; ( for i being set st i in dom p holds
it /. i = (p /. i) * a ) );
existence
 ex b1 being FinSequence of the carrier of L st
( dom b1 = dom p &amp; ( for i being set st i in dom p holds
b1 /. i = (p /. i) * a ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of the carrier of L st dom b1 = dom p &amp; ( for i being set st i in dom p holds
b1 /. i = (p /. i) * a ) &amp; dom b2 = dom p &amp; ( for i being set st i in dom p holds
b2 /. i = (p /. i) * a ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines * POLYNOM1:def_2_:_
 for L being non empty multMagma
for p being FinSequence of the carrier of L
for a being Element of L
for b4 being FinSequence of the carrier of L holds
( b4 = p * a iff ( dom b4 = dom p &amp; ( for i being set st i in dom p holds
b4 /. i = (p /. i) * a ) ) );

theorem Th6: :: POLYNOM1:6
for L being non empty multMagma
for a being Element of L holds a * (<*> the carrier of L) = <*> the carrier of L
proofend;

theorem Th7: :: POLYNOM1:7
for L being non empty multMagma
for a being Element of L holds (<*> the carrier of L) * a = <*> the carrier of L
proofend;

theorem Th8: :: POLYNOM1:8
for L being non empty multMagma
for a, b being Element of L holds a * <*b*> = <*(a * b)*>
proofend;

theorem Th9: :: POLYNOM1:9
for L being non empty multMagma
for a, b being Element of L holds <*b*> * a = <*(b * a)*>
proofend;

theorem Th10: :: POLYNOM1:10
for L being non empty multMagma
for a being Element of L
for p, q being FinSequence of the carrier of L holds a * (p ^ q) = (a * p) ^ (a * q)
proofend;

theorem Th11: :: POLYNOM1:11
for L being non empty multMagma
for a being Element of L
for p, q being FinSequence of the carrier of L holds (p ^ q) * a = (p * a) ^ (q * a)
proofend;

registration
cluster non empty strict right_unital for multLoopStr_0 ;
existence
 ex b1 being non empty strict multLoopStr_0 st b1 is right_unital
proofend;
end;

registration
cluster non empty non trivial right_complementable almost_left_invertible strict associative commutative well-unital distributive Abelian add-associative right_zeroed for doubleLoopStr ;
existence
 ex b1 being non empty doubleLoopStr st
( b1 is strict &amp; b1 is Abelian &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable &amp; b1 is associative &amp; b1 is commutative &amp; b1 is distributive &amp; b1 is almost_left_invertible &amp; b1 is well-unital &amp; not b1 is trivial )
proofend;
end;

theorem Th12: :: POLYNOM1:12
for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for a being Element of L
for p being FinSequence of the carrier of L holds Sum (a * p) = a * (Sum p)
proofend;

theorem Th13: :: POLYNOM1:13
for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for a being Element of L
for p being FinSequence of the carrier of L holds Sum (p * a) = (Sum p) * a
proofend;

begin

theorem Th14: :: POLYNOM1:14
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for F being FinSequence of the carrier of L * holds Sum (FlattenSeq F) = Sum (Sum F)
proofend;

definition
let X be non empty set ;
let S be ZeroStr ;
let f be Function of X,S;
func Support f ->  Subset of X means :Def3: :: POLYNOM1:def 3
 for x being Element of X holds
( x in it iff f . x <> 0. S );
existence
 ex b1 being Subset of X st
for x being Element of X holds
( x in b1 iff f . x <> 0. S )
proofend;
uniqueness
 for b1, b2 being Subset of X st ( for x being Element of X holds
( x in b1 iff f . x <> 0. S ) ) &amp; ( for x being Element of X holds
( x in b2 iff f . x <> 0. S ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines Support POLYNOM1:def_3_:_
 for X being non empty set
for S being ZeroStr
for f being Function of X,S
for b4 being Subset of X holds
( b4 = Support f iff for x being Element of X holds
( x in b4 iff f . x <> 0. S ) );

definition
let X be non empty set ;
let S be ZeroStr ;
let p be Function of X,S;
attrp is finite-Support  means :Def4: :: POLYNOM1:def 4
 Support p is finite ;
end;

:: deftheorem Def4 defines finite-Support POLYNOM1:def_4_:_
 for X being non empty set
for S being ZeroStr
for p being Function of X,S holds
( p is finite-Support iff Support p is finite );

definition
let n be set ;
let L be non empty 1-sorted ;
let p be Function of (Bags n),L;
let x be bag of n;
:: original:.
redefine funcp . x ->  Element of L;
coherence
 p . x is Element of L
proofend;
end;

begin

definition
let X be set ;
let S be 1-sorted ;
mode Series of X,S is Function of (Bags X),S;
end;

definition
let n be set ;
let L be non empty addLoopStr ;
let p, q be Series of n,L;
funcp + q ->  Series of n,L equals :: POLYNOM1:def 5
p + q;
coherence
 p + q is Series of n,L ;
end;

:: deftheorem  defines + POLYNOM1:def_5_:_
 for n being set
for L being non empty addLoopStr
for p, q being Series of n,L holds p + q = p + q;

theorem Th15: :: POLYNOM1:15
for n being set
for L being non empty addLoopStr
for p, q being Series of n,L
for x being bag of n holds (p + q) . x = (p . x) + (q . x)
proofend;

theorem :: POLYNOM1:16
for n being set
for L being non empty addLoopStr
for p, q, r being Series of n,L st ( for x being bag of n holds r . x = (p . x) + (q . x) ) holds
r = p + q
proofend;

theorem Th17: :: POLYNOM1:17
for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L
for x being bag of n holds (- p) . x = - (p . x)
proofend;

theorem :: POLYNOM1:18
for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, r being Series of n,L st ( for x being bag of n holds r . x = - (p . x) ) holds
r = - p
proofend;

theorem :: POLYNOM1:19
for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L holds p = - (- p)
proofend;

theorem Th20: :: POLYNOM1:20
for n being set
for L being non empty right_zeroed addLoopStr
for p, q being Series of n,L holds Support (p + q) c= (Support p) \/ (Support q)
proofend;

definition
let n be set ;
let L be non empty Abelian right_zeroed addLoopStr ;
let p, q be Series of n,L;
:: original:+
redefine funcp + q ->  Series of n,L;
commutativity
 for p, q being Series of n,L holds p + q = q + p
proofend;
end;

theorem Th21: :: POLYNOM1:21
for n being set
for L being non empty add-associative right_zeroed doubleLoopStr
for p, q, r being Series of n,L holds (p + q) + r = p + (q + r)
proofend;

definition
let n be set ;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p, q be Series of n,L;
funcp - q ->  Series of n,L equals :: POLYNOM1:def 6
p + (- q);
coherence
 p + (- q) is Series of n,L ;
end;

:: deftheorem  defines - POLYNOM1:def_6_:_
 for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, q being Series of n,L holds p - q = p + (- q);

definition
let n be set ;
let S be non empty ZeroStr ;
func 0_ (n,S) ->  Series of n,S equals :: POLYNOM1:def 7
(Bags n) --> (0. S);
coherence
 (Bags n) --> (0. S) is Series of n,S ;
end;

:: deftheorem  defines 0_ POLYNOM1:def_7_:_
 for n being set
for S being non empty ZeroStr holds 0_ (n,S) = (Bags n) --> (0. S);

theorem Th22: :: POLYNOM1:22
for n being set
for S being non empty ZeroStr
for b being bag of n holds (0_ (n,S)) . b = 0. S
proofend;

theorem Th23: :: POLYNOM1:23
for n being set
for L being non empty right_zeroed addLoopStr
for p being Series of n,L holds p + (0_ (n,L)) = p
proofend;

definition
let n be set ;
let L be non empty right_unital multLoopStr_0 ;
func 1_ (n,L) ->  Series of n,L equals :: POLYNOM1:def 8
(0_ (n,L)) +* ((EmptyBag n),(1. L));
coherence
 (0_ (n,L)) +* ((EmptyBag n),(1. L)) is Series of n,L ;
end;

:: deftheorem  defines 1_ POLYNOM1:def_8_:_
 for n being set
for L being non empty right_unital multLoopStr_0 holds 1_ (n,L) = (0_ (n,L)) +* ((EmptyBag n),(1. L));

theorem Th24: :: POLYNOM1:24
for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L holds p - p = 0_ (n,L)
proofend;

theorem Th25: :: POLYNOM1:25
for n being set
for L being non empty right_unital multLoopStr_0 holds
( (1_ (n,L)) . (EmptyBag n) = 1. L &amp; ( for b being bag of n st b <> EmptyBag n holds
(1_ (n,L)) . b = 0. L ) )
proofend;

definition
let n be Ordinal;
let L be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let p, q be Series of n,L;
funcp *' q ->  Series of n,L means :Def9: :: POLYNOM1:def 9
 for b being bag of n ex s being FinSequence of the carrier of L st
( it . b = Sum s &amp; len s = len (decomp b) &amp; ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> &amp; s /. k = (p . b1) * (q . b2) ) ) );
existence
 ex b1 being Series of n,L st
for b being bag of n ex s being FinSequence of the carrier of L st
( b1 . b = Sum s &amp; len s = len (decomp b) &amp; ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> &amp; s /. k = (p . b1) * (q . b2) ) ) )
proofend;
uniqueness
 for b1, b2 being Series of n,L st ( for b being bag of n ex s being FinSequence of the carrier of L st
( b1 . b = Sum s &amp; len s = len (decomp b) &amp; ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> &amp; s /. k = (p . b1) * (q . b2) ) ) ) ) &amp; ( for b being bag of n ex s being FinSequence of the carrier of L st
( b2 . b = Sum s &amp; len s = len (decomp b) &amp; ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> &amp; s /. k = (p . b1) * (q . b2) ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines *' POLYNOM1:def_9_:_
 for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed doubleLoopStr
for p, q, b5 being Series of n,L holds
( b5 = p *' q iff for b being bag of n ex s being FinSequence of the carrier of L st
( b5 . b = Sum s &amp; len s = len (decomp b) &amp; ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> &amp; s /. k = (p . b1) * (q . b2) ) ) ) );

theorem Th26: :: POLYNOM1:26
for n being Ordinal
for L being non empty right_complementable associative distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being Series of n,L holds p *' (q + r) = (p *' q) + (p *' r)
proofend;

theorem Th27: :: POLYNOM1:27
for n being Ordinal
for L being non empty right_complementable associative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being Series of n,L holds (p *' q) *' r = p *' (q *' r)
proofend;

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

theorem :: POLYNOM1:28
for n being Ordinal
for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds p *' (0_ (n,L)) = 0_ (n,L)
proofend;

theorem Th29: :: POLYNOM1:29
for n being Ordinal
for L being non empty non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds p *' (1_ (n,L)) = p
proofend;

theorem Th30: :: POLYNOM1:30
for n being Ordinal
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds (1_ (n,L)) *' p = p
proofend;

begin

registration
let n be set ;
let S be non empty ZeroStr ;
cluster Relation-like Bags n -defined the carrier of S -valued Function-like non empty total quasi_total finite-Support for Element of bool [:(Bags n), the carrier of S:];
existence
 ex b1 being Series of n,S st b1 is finite-Support
proofend;
end;

definition
let n be Ordinal;
let S be non empty ZeroStr ;
mode Polynomial of n,S is finite-Support Series of n,S;
end;

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

registration
let n be Ordinal;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p be Polynomial of n,L;
cluster - p ->  finite-Support ;
coherence
 - p is finite-Support
proofend;
end;

registration
let n be Element of NAT ;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p, q be Polynomial of n,L;
clusterp - q ->  finite-Support ;
coherence
 p - q is finite-Support ;
end;

registration
let n be Ordinal;
let S be non empty ZeroStr ;
cluster 0_ (n,S) ->  finite-Support ;
coherence
 0_ (n,S) is finite-Support
proofend;
end;

registration
let n be Ordinal;
let L be non trivial right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr ;
cluster 1_ (n,L) ->  finite-Support ;
coherence
 1_ (n,L) is finite-Support
proofend;
end;

registration
let n be Ordinal;
let L be non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;
let p, q be Polynomial of n,L;
clusterp *' q ->  finite-Support ;
coherence
 p *' q is finite-Support
proofend;
end;

begin

definition
let n be Ordinal;
let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;
func Polynom-Ring (n,L) ->  non empty strict doubleLoopStr  means :Def10: :: POLYNOM1:def 10
( ( for x being set holds
( x in the carrier of it iff x is Polynomial of n,L ) ) &amp; ( for x, y being Element of it
for p, q being Polynomial of n,L st x = p &amp; y = q holds
x + y = p + q ) &amp; ( for x, y being Element of it
for p, q being Polynomial of n,L st x = p &amp; y = q holds
x * y = p *' q ) &amp; 0. it = 0_ (n,L) &amp; 1. it = 1_ (n,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 n,L ) ) &amp; ( for x, y being Element of b1
for p, q being Polynomial of n,L st x = p &amp; y = q holds
x + y = p + q ) &amp; ( for x, y being Element of b1
for p, q being Polynomial of n,L st x = p &amp; y = q holds
x * y = p *' q ) &amp; 0. b1 = 0_ (n,L) &amp; 1. b1 = 1_ (n,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 n,L ) ) &amp; ( for x, y being Element of b1
for p, q being Polynomial of n,L st x = p &amp; y = q holds
x + y = p + q ) &amp; ( for x, y being Element of b1
for p, q being Polynomial of n,L st x = p &amp; y = q holds
x * y = p *' q ) &amp; 0. b1 = 0_ (n,L) &amp; 1. b1 = 1_ (n,L) &amp; ( for x being set holds
( x in the carrier of b2 iff x is Polynomial of n,L ) ) &amp; ( for x, y being Element of b2
for p, q being Polynomial of n,L st x = p &amp; y = q holds
x + y = p + q ) &amp; ( for x, y being Element of b2
for p, q being Polynomial of n,L st x = p &amp; y = q holds
x * y = p *' q ) &amp; 0. b2 = 0_ (n,L) &amp; 1. b2 = 1_ (n,L) holds
b1 = b2
proofend;
end;

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

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

registration
let n be Ordinal;
let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) ->  non empty strict add-associative ;
coherence
 Polynom-Ring (n,L) is add-associative
proofend;
end;

registration
let n be Ordinal;
let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) ->  non empty strict right_zeroed ;
coherence
 Polynom-Ring (n,L) is right_zeroed
proofend;
end;

registration
let n be Ordinal;
let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) ->  non empty right_complementable strict ;
coherence
 Polynom-Ring (n,L) is right_complementable
proofend;
end;

registration
let n be Ordinal;
let L be non empty non trivial right_complementable commutative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) ->  non empty strict commutative ;
coherence
 Polynom-Ring (n,L) is commutative
proofend;
end;

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

Lm1: now__::_thesis:_for_n_being_Ordinal
for_L_being_non_empty_non_trivial_right_complementable_associative_well-unital_distributive_Abelian_add-associative_right_zeroed_doubleLoopStr_
for_x,_e_being_Element_of_(Polynom-Ring_(n,L))_st_e_=_1._(Polynom-Ring_(n,L))_holds_
(_x_*_e_=_x_&amp;_e_*_x_=_x_)
let n be Ordinal; ::_thesis: for L being non empty non trivial right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for x, e being Element of (Polynom-Ring (n,L)) st e = 1. (Polynom-Ring (n,L)) holds
( x * e = x &amp; e * x = x )
let L be non empty non trivial right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for x, e being Element of (Polynom-Ring (n,L)) st e = 1. (Polynom-Ring (n,L)) holds
( x * e = x &amp; e * x = x )
set Pm = Polynom-Ring (n,L);
let x, e be Element of (Polynom-Ring (n,L)); ::_thesis: ( e = 1. (Polynom-Ring (n,L)) implies ( x * e = x &amp; e * x = x ) )
reconsider p = x as Polynomial of n,L by Def10;
assume A1: e = 1. (Polynom-Ring (n,L)) ; ::_thesis: ( x * e = x &amp; e * x = x )
A2: 1. (Polynom-Ring (n,L)) = 1_ (n,L) by Def10;
hence x * e = p *' (1_ (n,L)) by A1, Def10
.= x by Th29 ;
::_thesis: e * x = x
thus e * x = (1_ (n,L)) *' p by A1, A2, Def10
.= x by Th30 ; ::_thesis: verum
end;

registration
let n be Ordinal;
let L be non empty non trivial right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) ->  non empty strict right-distributive well-unital ;
coherence
 ( Polynom-Ring (n,L) is well-unital &amp; Polynom-Ring (n,L) is right-distributive )
proofend;
end;

theorem :: POLYNOM1:31
for n being Ordinal
for L being non empty non trivial right_complementable associative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr holds 1. (Polynom-Ring (n,L)) = 1_ (n,L) by Def10;