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

theorem :: POLYNOM1:1

canceled;

theorem :: POLYNOM1:2

canceled;

theorem :: POLYNOM1:3

canceled;

theorem Th4: :: POLYNOM1:4

for X being set
for R being Relation st field R c= X holds
R is Relation of X

proof end;

theorem Th5: :: POLYNOM1:5

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;

definition

let X be set ;
let f be ManySortedSet of X;
let x, y be set ;
:: original: +*
redefine func f +* x,y -> ManySortedSet of X;
coherence
f +* x,y is ManySortedSet of X

proof end;

end;

theorem :: POLYNOM1:6

canceled;

theorem Th7: :: POLYNOM1:7

for f being one-to-one Function holds card f = card (rng f)

proof end;

definition

let A, X be set ;
let D be FinSequence-DOMAIN of A;
let p be PartFunc of X,D;
let i be set ;
:: original: /.
redefine func p /. i -> Element of D;
coherence
p /. i is Element of D ;

end;

registration

let X be set ;
cluster well-ordering being_linear-order Relation of X,X;
existence
ex b₁ being Order of X st
( b₁ is being_linear-order & b₁ is well-ordering )

proof end;

end;

theorem Th8: :: POLYNOM1:8

for X being non empty set
for A being non empty finite Subset of X
for R being Order of X
for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds
[x,y] in R ) holds
(SgmX R,A) /. 1 = x

proof end;

theorem Th9: :: POLYNOM1:9

for X being non empty set
for A being non empty finite Subset of X
for R being Order of X
for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds
[y,x] in R ) holds
(SgmX R,A) /. (len (SgmX R,A)) = x

proof end;

registration

let X be non empty set ;
let A be non empty finite Subset of X;
let R be being_linear-order Order of X;
cluster SgmX R,A -> one-to-one non empty ;
coherence
( not SgmX R,A is empty & SgmX R,A is one-to-one )

proof end;

end;

registration

cluster empty -> FinSequence-yielding set ;
coherence
for b₁ being Function st b₁ is empty holds
b₁ is FinSequence-yielding

proof end;

end;

definition

let F, G be FinSequence-yielding FinSequence;
:: original: ^^
redefine func F ^^ G -> FinSequence-yielding FinSequence;
coherence
F ^^ G is FinSequence-yielding FinSequence

proof end;

end;

registration

let i be Element of NAT ;
let f be FinSequence;
cluster i |-> f -> FinSequence-yielding ;
coherence
i |-> f is FinSequence-yielding

proof end;

end;

registration

let F be FinSequence-yielding FinSequence;
let x be set ;
cluster F . x -> FinSequence-like ;
coherence
F . x is FinSequence-like

proof end;

end;

registration

let F be FinSequence;
cluster Card F -> FinSequence-like ;
coherence
Card F is FinSequence-like

proof end;

end;

registration

cluster Cardinal-yielding set ;
existence
ex b₁ being FinSequence st b₁ is Cardinal-yielding

proof end;

end;

theorem Th10: :: POLYNOM1:10

for f being Function holds
( f is Cardinal-yielding iff for y being set st y in rng f holds
y is Cardinal )

proof end;

registration

let F, G be Cardinal-yielding FinSequence;
cluster F ^ G -> Cardinal-yielding ;
coherence
F ^ G is Cardinal-yielding

proof end;

end;

registration

cluster -> Cardinal-yielding FinSequence of NAT ;
coherence
for b₁ being FinSequence of NAT holds b₁ is Cardinal-yielding

proof end;

end;

registration

cluster Cardinal-yielding FinSequence of NAT ;
existence
ex b₁ being FinSequence of NAT st b₁ is Cardinal-yielding

proof end;

end;

definition

let D be set ;
let F be FinSequence of D * ;
:: original: Card
redefine func Card F -> Cardinal-yielding FinSequence of NAT ;
coherence
Card F is Cardinal-yielding FinSequence of NAT

proof end;

end;

registration

let F be FinSequence of NAT ;
let i be Element of NAT ;
cluster F | i -> Cardinal-yielding ;
coherence
F | i is Cardinal-yielding ;

end;

theorem Th11: :: POLYNOM1:11

for F being Function
for X being set holds Card (F | X) = (Card F) | X

proof end;

registration

let F be empty Function;
cluster Card F -> empty ;
coherence
Card F is empty

proof end;

end;

theorem Th12: :: POLYNOM1:12

for p being set holds Card <*p*> = <*(card p)*>

proof end;

theorem Th13: :: POLYNOM1:13

for F, G being FinSequence holds Card (F ^ G) = (Card F) ^ (Card G)

proof end;

registration

let X be set ;
cluster <*> X -> FinSequence-yielding ;
coherence
<*> X is FinSequence-yielding ;

end;

registration

let f be FinSequence;
cluster <*f*> -> FinSequence-yielding ;
coherence
<*f*> is FinSequence-yielding

proof end;

end;

theorem Th14: :: POLYNOM1:14

for f being Function holds
( f is FinSequence-yielding iff for y being set st y in rng f holds
y is FinSequence )

proof end;

registration

let F, G be FinSequence-yielding FinSequence;
cluster F ^ G -> FinSequence-yielding ;
coherence
F ^ G is FinSequence-yielding

proof end;

end;

theorem Th15: :: POLYNOM1:15

for L being non empty addLoopStr
for F being FinSequence of the carrier of L * holds dom (Sum F) = dom F

proof end;

theorem Th16: :: POLYNOM1:16

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 Th17: :: POLYNOM1:17

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

proof end;

theorem Th18: :: POLYNOM1:18

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;
canceled;
:: original: *
redefine func a * p -> FinSequence of the carrier of L means :Def2: :: POLYNOM1:def 2
( dom it = dom p & ( for i being set 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 set st i in dom p holds
b₁ /. i = a * (p /. i) ) ) )

proof end;

correctness
coherence
a * p is FinSequence of the carrier of L;
;

end;

:: deftheorem POLYNOM1:def 1 :

canceled;

:: 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₄ = a * p iff ( dom b₄ = dom p & ( for i being set 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 :Def3: :: POLYNOM1:def 3
( dom it = dom p & ( for i being set 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 set 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 set st i in dom p holds
b₁ /. i = (p /. i) * a ) & dom b₂ = dom p & ( for i being set st i in dom p holds
b₂ /. i = (p /. i) * a ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines * POLYNOM1:def 3 :

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 set st i in dom p holds
b₄ /. i = (p /. i) * a ) ) );

theorem Th19: :: POLYNOM1:19

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 Th20: :: POLYNOM1:20

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 Th21: :: POLYNOM1:21

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

proof end;

theorem Th22: :: POLYNOM1:22

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

proof end;

theorem Th23: :: POLYNOM1:23

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 Th24: :: POLYNOM1:24

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 non degenerated -> non empty non trivial multLoopStr_0 ;
coherence
for b₁ being non empty multLoopStr_0 st not b₁ is degenerated holds
not b₁ is trivial ;

end;

registration

cluster non empty strict right_unital 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 :: POLYNOM1:25

canceled;

theorem :: POLYNOM1:26

canceled;

theorem Th27: :: POLYNOM1:27

for L being non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr st 0. L = 1. L holds
L is trivial

proof end;

theorem Th28: :: POLYNOM1:28

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 Th29: :: POLYNOM1:29

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;

registration

let D be set ;
let F be empty FinSequence of D * ;
cluster FlattenSeq F -> empty ;
coherence
FlattenSeq F is empty

proof end;

end;

theorem Th30: :: POLYNOM1:30

for D being set
for F being FinSequence of D * holds len (FlattenSeq F) = Sum (Card F)

proof end;

theorem Th31: :: POLYNOM1:31

for D, E being set
for F being FinSequence of D *
for G being FinSequence of E * st Card F = Card G holds
len (FlattenSeq F) = len (FlattenSeq G)

proof end;

theorem Th32: :: POLYNOM1:32

for D being set
for F being FinSequence of D *
for k being set st k in dom (FlattenSeq F) holds
ex i, j being Element of NAT st
( i in dom F & j in dom (F . i) & k = (Sum (Card (F | (i -' 1)))) + j & (F . i) . j = (FlattenSeq F) . k )

proof end;

theorem Th33: :: POLYNOM1:33

for D being set
for F being FinSequence of D *
for i, j being Element of NAT st i in dom F & j in dom (F . i) holds
( (Sum (Card (F | (i -' 1)))) + j in dom (FlattenSeq F) & (F . i) . j = (FlattenSeq F) . ((Sum (Card (F | (i -' 1)))) + j) )

proof end;

theorem Th34: :: POLYNOM1:34

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;

theorem Th35: :: POLYNOM1:35

for X, Y being non empty set
for f being FinSequence of X *
for v being Function of X,Y holds ((dom f) --> v) ** f is FinSequence of Y *

proof end;

theorem Th36: :: POLYNOM1:36

for X, Y being non empty set
for f being FinSequence of X *
for v being Function of X,Y ex F being FinSequence of Y * st
( F = ((dom f) --> v) ** f & v * (FlattenSeq f) = FlattenSeq F )

proof end;

registration

let f be natural-valued Function;
let x be set ;
let n be natural number ;
cluster f +* x,n -> natural-valued ;
coherence
f +* x,n is natural-valued

proof end;

end;

registration

let f be real-valued Function;
let x be set ;
let n be real number ;
cluster f +* x,n -> real-valued ;
coherence
f +* x,n is real-valued

proof end;

end;

registration

let X be set ;
cluster natural-valued ManySortedSet of X;
existence
ex b₁ being ManySortedSet of X st b₁ is natural-valued

proof end;

end;

registration

let X be set ;
cluster real-valued ManySortedSet of X;
existence
ex b₁ being ManySortedSet of X st b₁ is real-valued

proof end;

end;

registration

let X be set ;
cluster real-valued ManySortedSet of X;
existence
ex b₁ being ManySortedSet of X st b₁ is real-valued

proof end;

end;

definition

let X be set ;
let b1, b2 be complex-valued ManySortedSet of X;
canceled;
:: original: +
redefine func b1 + b2 -> ManySortedSet of X means :Def5: :: POLYNOM1:def 5
for x being set holds it . x = (b1 . x) + (b2 . x);
coherence
b1 + b2 is ManySortedSet of X

proof end;

compatibility
for b₁ being ManySortedSet of X holds
( b₁ = b1 + b2 iff for x being set holds b₁ . x = (b1 . x) + (b2 . x) )

proof end;

end;

:: deftheorem POLYNOM1:def 4 :

canceled;

:: deftheorem Def5 defines + POLYNOM1:def 5 :

for X being set
for b1, b2 being complex-valued ManySortedSet of X
for b₄ being ManySortedSet of X holds
( b₄ = b1 + b2 iff for x being set holds b₄ . x = (b1 . x) + (b2 . x) );

definition

let X be set ;
let b1, b2 be natural-valued ManySortedSet of X;
func b1 -' b2 -> ManySortedSet of X means :Def6: :: POLYNOM1:def 6
for x being set holds it . x = (b1 . x) -' (b2 . x);
existence
ex b₁ being ManySortedSet of X st
for x being set holds b₁ . x = (b1 . x) -' (b2 . x)

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of X st ( for x being set holds b₁ . x = (b1 . x) -' (b2 . x) ) & ( for x being set holds b₂ . x = (b1 . x) -' (b2 . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines -' POLYNOM1:def 6 :

for X being set
for b1, b2 being natural-valued ManySortedSet of X
for b₄ being ManySortedSet of X holds
( b₄ = b1 -' b2 iff for x being set holds b₄ . x = (b1 . x) -' (b2 . x) );

theorem :: POLYNOM1:37

for X being set
for b, b1, b2 being real-valued ManySortedSet of X st ( for x being set st x in X holds
b . x = (b1 . x) + (b2 . x) ) holds
b = b1 + b2

proof end;

theorem Th38: :: POLYNOM1:38

for X being set
for b, b1, b2 being natural-valued ManySortedSet of X st ( for x being set st x in X holds
b . x = (b1 . x) -' (b2 . x) ) holds
b = b1 -' b2

proof end;

registration

let X be set ;
let b1, b2 be natural-valued ManySortedSet of X;
cluster b1 + b2 -> natural-valued ;
coherence
b1 + b2 is natural-valued ;
cluster b1 -' b2 -> natural-valued ;
coherence
b1 -' b2 is natural-valued

proof end;

end;

theorem Th39: :: POLYNOM1:39

for X being set
for b1, b2, b3 being real-valued ManySortedSet of X holds (b1 + b2) + b3 = b1 + (b2 + b3)

proof end;

theorem :: POLYNOM1:40

for X being set
for b, c, d being natural-valued ManySortedSet of X holds (b -' c) -' d = b -' (c + d)

proof end;

definition

let f be Function;
func support f -> set means :Def7: :: POLYNOM1:def 7
for x being set holds
( x in it iff f . x <> 0 );
existence
ex b₁ being set st
for x being set holds
( x in b₁ iff f . x <> 0 )

proof end;

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

proof end;

end;

:: deftheorem Def7 defines support POLYNOM1:def 7 :

for f being Function
for b₂ being set holds
( b₂ = support f iff for x being set holds
( x in b₂ iff f . x <> 0 ) );

theorem Th41: :: POLYNOM1:41

for f being Function holds support f c= dom f

proof end;

definition

let f be Function;
attr f is finite-support means :Def8: :: POLYNOM1:def 8
support f is finite;

end;

:: deftheorem Def8 defines finite-support POLYNOM1:def 8 :

for f being Function holds
( f is finite-support iff support f is finite );

registration

cluster finite -> finite-support set ;
coherence
for b₁ being Function st b₁ is finite holds
b₁ is finite-support

proof end;

end;

registration

cluster non empty natural-valued finite-support set ;
existence
ex b₁ being Function st
( b₁ is natural-valued & b₁ is finite-support & not b₁ is empty )

proof end;

end;

registration

let f be finite-support Function;
cluster support f -> finite ;
coherence
support f is finite by Def8;

end;

registration

let X be set ;
cluster finite-support Relation of X, NAT ;
existence
ex b₁ being Function of X, NAT st b₁ is finite-support

proof end;

end;

registration

let f be finite-support Function;
let x, y be set ;
cluster f +* x,y -> finite-support ;
coherence
f +* x,y is finite-support

proof end;

end;

registration

let X be set ;
cluster natural-valued finite-support ManySortedSet of X;
existence
ex b₁ being ManySortedSet of X st
( b₁ is natural-valued & b₁ is finite-support )

proof end;

end;

theorem Th42: :: POLYNOM1:42

for X being set
for b1, b2 being natural-valued ManySortedSet of X holds support (b1 + b2) = (support b1) \/ (support b2)

proof end;

theorem Th43: :: POLYNOM1:43

for X being set
for b1, b2 being natural-valued ManySortedSet of X holds support (b1 -' b2) c= support b1

proof end;

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 :Def9: :: POLYNOM1:def 9
for x being Element of X holds
( x in it iff f . x <> 0. S );
existence
ex b₁ being Subset of X st
for x being Element of X holds
( x in b₁ iff f . x <> 0. S )

proof end;

uniqueness
for b₁, b₂ being Subset of X st ( for x being Element of X holds
( x in b₁ iff f . x <> 0. S ) ) & ( for x being Element of X holds
( x in b₂ iff f . x <> 0. S ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines Support POLYNOM1:def 9 :

for X being non empty set
for S being 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 X be non empty set ;
let S be ZeroStr ;
let p be Function of X,S;
attr p is finite-Support means :Def10: :: POLYNOM1:def 10
Support p is finite;

end;

:: deftheorem Def10 defines finite-Support POLYNOM1:def 10 :

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 X be set ;
mode bag of X is natural-valued finite-support ManySortedSet of X;

end;

registration

let X be finite set ;
cluster -> finite-support ManySortedSet of X;
coherence
for b₁ being ManySortedSet of X holds b₁ is finite-support

proof end;

end;

registration

let X be set ;
let b1, b2 be bag of X;
cluster b1 + b2 -> finite-support ;
coherence
b1 + b2 is finite-support

proof end;

cluster b1 -' b2 -> finite-support ;
coherence
b1 -' b2 is finite-support

proof end;

end;

theorem Th44: :: POLYNOM1:44

for X being set holds X --> 0 is bag of X

proof end;

definition

let n be Ordinal;
let p, q be bag of n;
pred p < q means :Def11: :: POLYNOM1:def 11
ex k being Ordinal st
( p . k < q . k & ( for l being Ordinal st l in k holds
p . l = q . l ) );
asymmetry
for p, q being bag of n st ex k being Ordinal st
( p . k < q . k & ( for l being Ordinal st l in k holds
p . l = q . l ) ) holds
for k being Ordinal holds
( not q . k < p . k or ex l being Ordinal st
( l in k & not q . l = p . l ) )

proof end;

end;

:: deftheorem Def11 defines < POLYNOM1:def 11 :

for n being Ordinal
for p, q being bag of n holds
( p < q iff ex k being Ordinal st
( p . k < q . k & ( for l being Ordinal st l in k holds
p . l = q . l ) ) );

theorem Th45: :: POLYNOM1:45

for n being Ordinal
for p, q, r being bag of n st p < q & q < r holds
p < r

proof end;

definition

let n be Ordinal;
let p, q be bag of n;
pred p <=' q means :Def12: :: POLYNOM1:def 12
( p < q or p = q );
reflexivity
for p being bag of n holds
( p < p or p = p ) ;

end;

:: deftheorem Def12 defines <=' POLYNOM1:def 12 :

for n being Ordinal
for p, q being bag of n holds
( p <=' q iff ( p < q or p = q ) );

theorem Th46: :: POLYNOM1:46

for n being Ordinal
for p, q, r being bag of n st p <=' q & q <=' r holds
p <=' r

proof end;

theorem :: POLYNOM1:47

for n being Ordinal
for p, q, r being bag of n st p < q & q <=' r holds
p < r

proof end;

theorem :: POLYNOM1:48

for n being Ordinal
for p, q, r being bag of n st p <=' q & q < r holds
p < r

proof end;

theorem Th49: :: POLYNOM1:49

for n being Ordinal
for p, q being bag of n holds
( p <=' q or q <=' p )

proof end;

definition

let X be set ;
let d, b be bag of X;
pred d divides b means :Def13: :: POLYNOM1:def 13
for k being set holds d . k <= b . k;
reflexivity
for d being bag of X
for k being set holds d . k <= d . k ;

end;

:: deftheorem Def13 defines divides POLYNOM1:def 13 :

for X being set
for d, b being bag of X holds
( d divides b iff for k being set holds d . k <= b . k );

theorem Th50: :: POLYNOM1:50

for n being set
for d, b being bag of n st ( for k being set st k in n holds
d . k <= b . k ) holds
d divides b

proof end;

theorem Th51: :: POLYNOM1:51

for n being Ordinal
for b1, b2 being bag of n st b1 divides b2 holds
(b2 -' b1) + b1 = b2

proof end;

theorem Th52: :: POLYNOM1:52

for X being set
for b1, b2 being bag of X holds (b2 + b1) -' b1 = b2

proof end;

theorem Th53: :: POLYNOM1:53

for n being Ordinal
for d, b being bag of n st d divides b holds
d <=' b

proof end;

theorem Th54: :: POLYNOM1:54

for n being set
for b, b1, b2 being bag of n st b = b1 + b2 holds
b1 divides b

proof end;

definition

let X be set ;
func Bags X -> set means :Def14: :: POLYNOM1:def 14
for x being set holds
( x in it iff x is bag of X );
existence
ex b₁ being set st
for x being set holds
( x in b₁ iff x is bag of X )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff x is bag of X ) ) & ( for x being set holds
( x in b₂ iff x is bag of X ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines Bags POLYNOM1:def 14 :

for X being set
for b₂ being set holds
( b₂ = Bags X iff for x being set holds
( x in b₂ iff x is bag of X ) );

definition

let X be set ;
:: original: Bags
redefine func Bags X -> Subset of (Bags X);
coherence
Bags X is Subset of (Bags X)

proof end;

end;

theorem :: POLYNOM1:55

Bags {} = {{} }

proof end;

registration

let X be set ;
cluster Bags X -> non empty ;
coherence
not Bags X is empty

proof end;

end;

definition

let X be set ;
let B be non empty Subset of (Bags X);
:: original: Element
redefine mode Element of B -> bag of X;
coherence
for b₁ being Element of B holds b₁ is bag of X

proof end;

end;

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 ;
func EmptyBag X -> Element of Bags X equals :: POLYNOM1:def 15
X --> 0 ;
coherence
X --> 0 is Element of Bags X

proof end;

end;

:: deftheorem defines EmptyBag POLYNOM1:def 15 :

for X being set holds EmptyBag X = X --> 0 ;

theorem Th56: :: POLYNOM1:56

for X, x being set holds (EmptyBag X) . x = 0

proof end;

theorem :: POLYNOM1:57

for X being set
for b being bag of X holds b + (EmptyBag X) = b

proof end;

theorem Th58: :: POLYNOM1:58

for X being set
for b being bag of X holds b -' (EmptyBag X) = b

proof end;

theorem :: POLYNOM1:59

for X being set
for b being bag of X holds (EmptyBag X) -' b = EmptyBag X

proof end;

theorem Th60: :: POLYNOM1:60

for X being set
for b being bag of X holds b -' b = EmptyBag X

proof end;

theorem Th61: :: POLYNOM1:61

for n being set
for b1, b2 being bag of n st b1 divides b2 & b2 -' b1 = EmptyBag n holds
b2 = b1

proof end;

theorem Th62: :: POLYNOM1:62

for n being set
for b being bag of n st b divides EmptyBag n holds
EmptyBag n = b

proof end;

theorem Th63: :: POLYNOM1:63

for n being set
for b being bag of n holds EmptyBag n divides b

proof end;

theorem :: POLYNOM1:64

for n being Ordinal
for b being bag of n holds EmptyBag n <=' b by Th53, Th63;

definition

let n be Ordinal;
func BagOrder n -> Order of Bags n means :Def16: :: POLYNOM1:def 16
for p, q being bag of n holds
( [p,q] in it iff p <=' q );
existence
ex b₁ being Order of Bags n st
for p, q being bag of n holds
( [p,q] in b₁ iff p <=' q )

proof end;

uniqueness
for b₁, b₂ being Order of Bags n st ( for p, q being bag of n holds
( [p,q] in b₁ iff p <=' q ) ) & ( for p, q being bag of n holds
( [p,q] in b₂ iff p <=' q ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def16 defines BagOrder POLYNOM1:def 16 :

for n being Ordinal
for b₂ being Order of Bags n holds
( b₂ = BagOrder n iff for p, q being bag of n holds
( [p,q] in b₂ iff p <=' q ) );

Lm1: for n being Ordinal holds BagOrder n is_reflexive_in Bags n

proof end;

Lm2: for n being Ordinal holds BagOrder n is_antisymmetric_in Bags n

proof end;

Lm3: for n being Ordinal holds BagOrder n is_transitive_in Bags n

proof end;

Lm4: for n being Ordinal holds BagOrder n linearly_orders Bags n

proof end;

registration

let n be Ordinal;
cluster BagOrder n -> being_linear-order ;
coherence
BagOrder n is being_linear-order

proof end;

end;

definition

let X be set ;
let f be Function of X, NAT ;
func NatMinor f -> Subset of (Funcs X,NAT ) means :Def17: :: POLYNOM1:def 17
for g being natural-valued ManySortedSet of X holds
( g in it iff for x being set st x in X holds
g . x <= f . x );
existence
ex b₁ being Subset of (Funcs X,NAT ) st
for g being natural-valued ManySortedSet of X holds
( g in b₁ iff for x being set st x in X holds
g . x <= f . x )

proof end;

uniqueness
for b₁, b₂ being Subset of (Funcs X,NAT ) st ( for g being natural-valued ManySortedSet of X holds
( g in b₁ iff for x being set st x in X holds
g . x <= f . x ) ) & ( for g being natural-valued ManySortedSet of X holds
( g in b₂ iff for x being set st x in X holds
g . x <= f . x ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def17 defines NatMinor POLYNOM1:def 17 :

for X being set
for f being Function of X, NAT
for b₃ being Subset of (Funcs X,NAT ) holds
( b₃ = NatMinor f iff for g being natural-valued ManySortedSet of X holds
( g in b₃ iff for x being set st x in X holds
g . x <= f . x ) );

theorem Th65: :: POLYNOM1:65

for X being set
for f being Function of X, NAT holds f in NatMinor f

proof end;

registration

let X be set ;
let f be Function of X, NAT ;
cluster NatMinor f -> non empty functional ;
coherence
( not NatMinor f is empty & NatMinor f is functional )

proof end;

end;

registration

let X be set ;
let f be Function of X, NAT ;
cluster -> natural-valued Element of NatMinor f;
coherence
for b₁ being Element of NatMinor f holds b₁ is natural-valued

proof end;

end;

theorem Th66: :: POLYNOM1:66

for X being set
for f being finite-support Function of X, NAT holds NatMinor f c= Bags X

proof end;

definition

let X be set ;
let f be finite-support Function of X, NAT ;
:: original: support
redefine func support f -> Element of Fin X;
coherence
support f is Element of Fin X

proof end;

end;

theorem Th67: :: POLYNOM1:67

for X being non empty set
for f being finite-support Function of X, NAT holds card (NatMinor f) = multnat $$ (support f),(addnat [:] f,1)

proof end;

registration

let X be set ;
let f be finite-support Function of X, NAT ;
cluster NatMinor f -> finite ;
coherence
NatMinor f is finite

proof end;

end;

definition

let n be Ordinal;
let b be bag of n;
func divisors b -> FinSequence of Bags n means :Def18: :: POLYNOM1:def 18
ex S being non empty finite Subset of (Bags n) st
( it = SgmX (BagOrder n),S & ( for p being bag of n holds
( p in S iff p divides b ) ) );
existence
ex b₁ being FinSequence of Bags n ex S being non empty finite Subset of (Bags n) st
( b₁ = SgmX (BagOrder n),S & ( for p being bag of n holds
( p in S iff p divides b ) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of Bags n st ex S being non empty finite Subset of (Bags n) st
( b₁ = SgmX (BagOrder n),S & ( for p being bag of n holds
( p in S iff p divides b ) ) ) & ex S being non empty finite Subset of (Bags n) st
( b₂ = SgmX (BagOrder n),S & ( for p being bag of n holds
( p in S iff p divides b ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def18 defines divisors POLYNOM1:def 18 :

for n being Ordinal
for b being bag of n
for b₃ being FinSequence of Bags n holds
( b₃ = divisors b iff ex S being non empty finite Subset of (Bags n) st
( b₃ = SgmX (BagOrder n),S & ( for p being bag of n holds
( p in S iff p divides b ) ) ) );

registration

let n be Ordinal;
let b be bag of n;
cluster divisors b -> one-to-one non empty ;
coherence
( not divisors b is empty & divisors b is one-to-one )

proof end;

end;

theorem Th68: :: POLYNOM1:68

for n being Ordinal
for i being Element of NAT
for b being bag of n st i in dom (divisors b) holds
(divisors b) /. i divides b

proof end;

theorem Th69: :: POLYNOM1:69

for n being Ordinal
for b being bag of n holds
( (divisors b) /. 1 = EmptyBag n & (divisors b) /. (len (divisors b)) = b )

proof end;

theorem Th70: :: POLYNOM1:70

for n being Ordinal
for i being Nat
for b, b1, b2 being bag of n st i > 1 & i < len (divisors b) holds
( (divisors b) /. i <> EmptyBag n & (divisors b) /. i <> b )

proof end;

theorem Th71: :: POLYNOM1:71

for n being Ordinal holds divisors (EmptyBag n) = <*(EmptyBag n)*>

proof end;

definition

let n be Ordinal;
let b be bag of n;
func decomp b -> FinSequence of 2 -tuples_on (Bags n) means :Def19: :: POLYNOM1:def 19
( dom it = dom (divisors b) & ( for i being Element of NAT
for p being bag of n st i in dom it & p = (divisors b) /. i holds
it /. i = <*p,(b -' p)*> ) );
existence
ex b₁ being FinSequence of 2 -tuples_on (Bags n) st
( dom b₁ = dom (divisors b) & ( for i being Element of NAT
for p being bag of n st i in dom b₁ & p = (divisors b) /. i holds
b₁ /. i = <*p,(b -' p)*> ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of 2 -tuples_on (Bags n) st dom b₁ = dom (divisors b) & ( for i being Element of NAT
for p being bag of n st i in dom b₁ & p = (divisors b) /. i holds
b₁ /. i = <*p,(b -' p)*> ) & dom b₂ = dom (divisors b) & ( for i being Element of NAT
for p being bag of n st i in dom b₂ & p = (divisors b) /. i holds
b₂ /. i = <*p,(b -' p)*> ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def19 defines decomp POLYNOM1:def 19 :

for n being Ordinal
for b being bag of n
for b₃ being FinSequence of 2 -tuples_on (Bags n) holds
( b₃ = decomp b iff ( dom b₃ = dom (divisors b) & ( for i being Element of NAT
for p being bag of n st i in dom b₃ & p = (divisors b) /. i holds
b₃ /. i = <*p,(b -' p)*> ) ) );

theorem Th72: :: POLYNOM1:72

for n being Ordinal
for i being Element of NAT
for b being bag of n st i in dom (decomp b) holds
ex b1, b2 being bag of n st
( (decomp b) /. i = <*b1,b2*> & b = b1 + b2 )

proof end;

theorem Th73: :: POLYNOM1:73

for n being Ordinal
for b, b1, b2 being bag of n st b = b1 + b2 holds
ex i being Element of NAT st
( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> )

proof end;

theorem Th74: :: POLYNOM1:74

for n being Ordinal
for i being Element of NAT
for b, b1, b2 being bag of n st i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> holds
b1 = (divisors b) /. i

proof end;

registration

let n be Ordinal;
let b be bag of n;
cluster decomp b -> one-to-one non empty FinSequence-yielding ;
coherence
( not decomp b is empty & decomp b is one-to-one & decomp b is FinSequence-yielding )

proof end;

end;

registration

let n be Ordinal;
let b be Element of Bags n;
cluster decomp b -> one-to-one non empty FinSequence-yielding ;
coherence
( not decomp b is empty & decomp b is one-to-one & decomp b is FinSequence-yielding ) ;

end;

theorem Th75: :: POLYNOM1:75

for n being Ordinal
for b being bag of n holds
( (decomp b) /. 1 = <*(EmptyBag n),b*> & (decomp b) /. (len (decomp b)) = <*b,(EmptyBag n)*> )

proof end;

theorem Th76: :: POLYNOM1:76

for n being Ordinal
for i being Nat
for b, b1, b2 being bag of n st i > 1 & i < len (decomp b) & (decomp b) /. i = <*b1,b2*> holds
( b1 <> EmptyBag n & b2 <> EmptyBag n )

proof end;

theorem Th77: :: POLYNOM1:77

for n being Ordinal holds decomp (EmptyBag n) = <*<*(EmptyBag n),(EmptyBag n)*>*>

proof end;

theorem Th78: :: POLYNOM1:78

for n being Ordinal
for b being bag of n
for f, g being FinSequence of (3 -tuples_on (Bags n)) * st dom f = dom (decomp b) & dom g = dom (decomp b) & ( for k being Nat st k in dom f holds
f . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) ) & ( for k being Nat st k in dom g holds
g . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)) ) holds
ex p being Permutation of dom (FlattenSeq f) st FlattenSeq g = (FlattenSeq f) * p

proof 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;
canceled;
func p + q -> Series of n,L means :Def21: :: POLYNOM1:def 21
for x being bag of n holds it . x = (p . x) + (q . x);
existence
ex b₁ being Series of n,L st
for x being bag of n holds b₁ . x = (p . x) + (q . x)

proof end;

uniqueness
for b₁, b₂ being Series of n,L st ( for x being bag of n holds b₁ . x = (p . x) + (q . x) ) & ( for x being bag of n holds b₂ . x = (p . x) + (q . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem POLYNOM1:def 20 :

canceled;

:: deftheorem Def21 defines + POLYNOM1:def 21 :

for n being set
for L being non empty addLoopStr
for p, q, b₅ being Series of n,L holds
( b₅ = p + q iff for x being bag of n holds b₅ . x = (p . x) + (q . x) );

theorem Th79: :: POLYNOM1:79

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 Th80: :: POLYNOM1:80

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 be Series of n,L;
func - p -> Series of n,L means :Def22: :: POLYNOM1:def 22
for x being bag of n holds it . x = - (p . x);
existence
ex b₁ being Series of n,L st
for x being bag of n holds b₁ . x = - (p . x)

proof end;

uniqueness
for b₁, b₂ being Series of n,L st ( for x being bag of n holds b₁ . x = - (p . x) ) & ( for x being bag of n holds b₂ . x = - (p . x) ) holds
b₁ = b₂

proof end;

involutiveness
for b₁, b₂ being Series of n,L st ( for x being bag of n holds b₁ . x = - (b₂ . x) ) holds
for x being bag of n holds b₂ . x = - (b₁ . x)

proof end;

end;

:: deftheorem Def22 defines - POLYNOM1:def 22 :

for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, b₄ being Series of n,L holds
( b₄ = - p iff for x being bag of n holds b₄ . x = - (p . x) );

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 23
p + (- q);
coherence
p + (- q) is Series of n,L ;

end;

:: deftheorem defines - POLYNOM1:def 23 :

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 24
(Bags n) --> (0. S);
coherence
(Bags n) --> (0. S) is Series of n,S ;

end;

:: deftheorem defines 0_ POLYNOM1:def 24 :

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

theorem Th81: :: POLYNOM1:81

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 Th82: :: POLYNOM1:82

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 25
(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 25 :

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 Th83: :: POLYNOM1:83

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 Th84: :: POLYNOM1:84

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 :Def26: :: POLYNOM1:def 26
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 Def26 defines *' POLYNOM1:def 26 :

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 Th85: :: POLYNOM1:85

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)

proof end;

theorem Th86: :: POLYNOM1:86

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)

proof end;

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 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:87

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 Th88: :: POLYNOM1:88

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 Th89: :: POLYNOM1:89

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 finite-Support Relation of 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 empty 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 empty non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;
func Polynom-Ring n,L -> non empty strict doubleLoopStr means :Def27: :: POLYNOM1:def 27
( ( 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 Def27 defines Polynom-Ring POLYNOM1:def 27 :

for n being Ordinal
for L being non empty 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 empty 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 empty 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 empty 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 empty 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 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

proof end;

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

proof end;

end;

Lm5: now

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 & 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 & 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 ) )
assume A1: e = 1. (Polynom-Ring n,L) ; :: thesis: ( x * e = x & e * x = x )
reconsider p = x as Polynomial of n,L by Def27;
A2: 1. (Polynom-Ring n,L) = 1_ n,L by Def27;
hence x * e = p *' (1_ n,L) by A1, Def27
.= x by Th88 ;
:: thesis: e * x = x
thus e * x = (1_ n,L) *' p by A1, A2, Def27
.= x by Th89 ; :: 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 & Polynom-Ring n,L is right-distributive )

proof end;

end;

theorem :: POLYNOM1:90

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

theorem :: POLYNOM1:91

for X being set
for b1, b2 being real-valued ManySortedSet of X holds support (b1 + b2) c= (support b1) \/ (support b2)

proof end;