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

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 b₁ being non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr st b₁ is degenerated holds
b₁ is trivial

proof end;

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 b₁ being non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr st not b₁ is trivial holds
not b₁ 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

proof end;

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

proof end;

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

proof end;

theorem Th4: :: POLYNOM1:4

for L being non empty addLoopStr
for p being Element of the carrier of L * holds <*(Sum p)*> = Sum <*p*>

proof end;

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)

proof end;

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 & ( for i being object st i in dom p holds
it /. i = a * (p /. i) ) );

compatibility
for b₁ being FinSequence of the carrier of L holds
( b₁ = a * p iff ( dom b₁ = dom p & ( for i being object st i in dom p holds
b₁ /. i = a * (p /. i) ) ) )

proof end;

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 b₄ being FinSequence of the carrier of L holds
( b₄ = a * p iff ( dom b₄ = dom p & ( for i being object st i in dom p holds
b₄ /. 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;

func p * a -> FinSequence of the carrier of L means :Def2: :: POLYNOM1:def 2
( dom it = dom p & ( for i being object st i in dom p holds
it /. i = (p /. i) * a ) );

existence
ex b₁ being FinSequence of the carrier of L st
( dom b₁ = dom p & ( for i being object st i in dom p holds
b₁ /. i = (p /. i) * a ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of the carrier of L st dom b₁ = dom p & ( for i being object st i in dom p holds
b₁ /. i = (p /. i) * a ) & dom b₂ = dom p & ( for i being object st i in dom p holds
b₂ /. i = (p /. i) * a ) holds
b₁ = b₂

proof end;

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 b₄ being FinSequence of the carrier of L holds
( b₄ = p * a iff ( dom b₄ = dom p & ( for i being object st i in dom p holds
b₄ /. 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

proof end;

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

proof end;

theorem Th8: :: POLYNOM1:8

for L being non empty multMagma
for a, b being Element of L holds a * <*b*> = <*(a * b)*>

proof end;

theorem Th9: :: POLYNOM1:9

for L being non empty multMagma
for a, b being Element of L holds <*b*> * a = <*(b * a)*>

proof end;

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)

proof end;

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)

proof end;

registration

cluster non empty strict right_unital for multLoopStr_0 ;

existence
ex b₁ being non empty strict multLoopStr_0 st b₁ is right_unital

proof end;

end;

registration

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

existence
ex b₁ being non empty doubleLoopStr st
( b₁ is strict & b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is associative & b₁ is commutative & b₁ is distributive & b₁ is almost_left_invertible & b₁ is well-unital & not b₁ is trivial )

proof end;

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)

proof end;

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

proof end;

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)

proof end;

definition

let S be ZeroStr ;
let f be the carrier of S -valued Function;

func Support f -> set means :Def3: :: POLYNOM1:def 3
for x being object holds
( x in it iff ( x in dom f & f . x <> 0. S ) );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff ( x in dom f & f . x <> 0. S ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ( x in dom f & f . x <> 0. S ) ) ) & ( for x being object holds
( x in b₂ iff ( x in dom f & f . x <> 0. S ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Support POLYNOM1:def 3 :
for S being ZeroStr
for f being the carrier of b₁ -valued Function
for b₃ being set holds
( b₃ = Support f iff for x being object holds
( x in b₃ iff ( x in dom f & f . x <> 0. S ) ) );

definition

let X be non empty set ;
let S be non empty ZeroStr ;
let f be Function of X,S;

:: original: Support
redefine func Support f -> Subset of X means :Def4: :: POLYNOM1:def 4
for x being Element of X holds
( x in it iff f . x <> 0. S );

coherence
Support f is Subset of X

proof end;

compatibility
for b₁ being Subset of X holds
( b₁ = Support f iff for x being Element of X holds
( x in b₁ iff f . x <> 0. S ) )

proof end;

end;

:: deftheorem Def4 defines Support POLYNOM1:def 4 :
for X being non empty set
for S being non empty ZeroStr
for f being Function of X,S
for b₄ being Subset of X holds
( b₄ = Support f iff for x being Element of X holds
( x in b₄ iff f . x <> 0. S ) );

definition

let S be ZeroStr ;
let p be the carrier of S -valued Function;

attr p is finite-Support means :Def5: :: POLYNOM1:def 5
Support p is finite ;

end;

:: deftheorem Def5 defines finite-Support POLYNOM1:def 5 :
for S being ZeroStr
for p being the carrier of b₁ -valued Function 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 func p . x -> Element of L;
coherence
p . x is Element of L

proof end;

end;

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;

func p + 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 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)

proof end;

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

proof end;

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)

proof end;

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

proof end;

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)

proof end;

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)

proof end;

definition

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

proof end;

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)

proof end;

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;

func p - q -> Series of n,L equals :: POLYNOM1:def 7
p + (- q);

coherence
p + (- q) is Series of n,L ;

end;

:: deftheorem defines - POLYNOM1:def 7 :
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 8
(Bags n) --> (0. S);

coherence
(Bags n) --> (0. S) is Series of n,S ;

end;

:: deftheorem defines 0_ POLYNOM1:def 8 :
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

proof end;

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

proof end;

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 9
(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 9 :
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)

proof end;

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 & ( for b being bag of n st b <> EmptyBag n holds
(1_ (n,L)) . b = 0. L ) )

proof end;

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;

func p *' q -> Series of n,L means :Def10: :: POLYNOM1:def 10
for b being bag of n ex s being FinSequence of the carrier of L st
( it . b = Sum s & len s = len (decomp b) & ( 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*> & s /. k = (p . b1) * (q . b2) ) ) );

existence
ex b₁ being Series of n,L st
for b being bag of n ex s being FinSequence of the carrier of L st
( b₁ . b = Sum s & len s = len (decomp b) & ( 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*> & s /. k = (p . b1) * (q . b2) ) ) )

proof end;

uniqueness
for b₁, b₂ being Series of n,L st ( for b being bag of n ex s being FinSequence of the carrier of L st
( b₁ . b = Sum s & len s = len (decomp b) & ( 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*> & s /. k = (p . b1) * (q . b2) ) ) ) ) & ( for b being bag of n ex s being FinSequence of the carrier of L st
( b₂ . b = Sum s & len s = len (decomp b) & ( 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*> & s /. k = (p . b1) * (q . b2) ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines *' POLYNOM1:def 10 :
for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed doubleLoopStr
for p, q, b₅ being Series of n,L holds
( b₅ = p *' q iff for b being bag of n ex s being FinSequence of the carrier of L st
( b₅ . b = Sum s & len s = len (decomp b) & ( 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*> & s /. k = (p . b1) * (q . b2) ) ) ) );

theorem Th26: :: POLYNOM1:26

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

proof end;

theorem Th27: :: POLYNOM1:27

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

proof end;

definition

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

proof end;

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)

proof end;

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

proof end;

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

proof end;

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 b₁ being Series of n,S st b₁ is finite-Support

proof end;

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;

cluster p + q -> finite-Support ;

coherence
p + q is finite-Support

proof end;

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

proof end;

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;

cluster p - 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

proof end;

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

proof end;

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;

cluster p *' q -> finite-Support ;

coherence
p *' q is finite-Support

proof end;

end;

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 :Def11: :: POLYNOM1:def 11
( ( for x being set holds
( x in the carrier of it iff x is Polynomial of n,L ) ) & ( for x, y being Element of it
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of it
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. it = 0_ (n,L) & 1. it = 1_ (n,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 n,L ) ) & ( for x, y being Element of b₁
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₁
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. b₁ = 0_ (n,L) & 1. b₁ = 1_ (n,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 n,L ) ) & ( for x, y being Element of b₁
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₁
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. b₁ = 0_ (n,L) & 1. b₁ = 1_ (n,L) & ( for x being set holds
( x in the carrier of b₂ iff x is Polynomial of n,L ) ) & ( for x, y being Element of b₂
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₂
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. b₂ = 0_ (n,L) & 1. b₂ = 1_ (n,L) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines Polynom-Ring POLYNOM1:def 11 :
for n being Ordinal
for L being non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for b₃ being non empty strict doubleLoopStr holds
( b₃ = Polynom-Ring (n,L) iff ( ( for x being set holds
( x in the carrier of b₃ iff x is Polynomial of n,L ) ) & ( for x, y being Element of b₃
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₃
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. b₃ = 0_ (n,L) & 1. b₃ = 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

proof end;

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

proof end;

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

proof end;

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

proof end;

end;

registration

let n be Ordinal;
let L be non empty non trivial right_complementable right_unital distributive Abelian add-associative right_zeroed commutative doubleLoopStr ;

cluster Polynom-Ring (n,L) -> non empty strict commutative ;

coherence
Polynom-Ring (n,L) is commutative

proof end;

end;

registration

let n be Ordinal;
let L be non empty non trivial right_complementable right_unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

cluster Polynom-Ring (n,L) -> non empty strict associative ;

coherence
Polynom-Ring (n,L) is associative

proof end;

end;

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

let n be Ordinal; :: thesis: for L being non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for x, e being Element of (Polynom-Ring (n,L)) st e = 1. (Polynom-Ring (n,L)) holds
( x * e = x & e * x = x )
let L be non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for x, e being Element of (Polynom-Ring (n,L)) st e = 1. (Polynom-Ring (n,L)) holds
( x * e = x & 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 & e * x = x ) )
reconsider p = x as Polynomial of n,L by Def11;
assume A1: e = 1. (Polynom-Ring (n,L)) ; :: thesis: ( x * e = x & e * x = x )
A2: 1. (Polynom-Ring (n,L)) = 1_ (n,L) by Def11;
hence x * e = p *' (1_ (n,L)) by A1, Def11
.= x by Th29 ;
:: thesis: e * x = x
thus e * x = (1_ (n,L)) *' p by A1, A2, Def11
.= x by Th30 ; :: thesis: verum

end;

registration

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

cluster Polynom-Ring (n,L) -> non empty strict right-distributive well-unital ;

coherence
( Polynom-Ring (n,L) is well-unital & Polynom-Ring (n,L) is right-distributive )

proof end;

end;

theorem :: POLYNOM1:31

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