:: POLYNOM1 semantic presentation

Lm1: for i, j being Nat holds multnat . i,j = i * j
by BINOP_2:def 24;

theorem :: POLYNOM1:1

canceled;

theorem Th2: :: POLYNOM1:2

for X being set
for A being non empty set
for F being BinOp of A
for f being Function of X,A
for x being Element of A holds dom (F [:] f,x) = X

proof end;

theorem Th3: :: POLYNOM1:3

for a, b, c being Nat holds (a -' b) -' c = a -' (b + c)

proof end;

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 LoopStr
for p1, p2 being FinSequence of the carrier of K st dom p1 = dom p2 holds
dom (p1 + p2) = dom p1

proof end;

theorem Th6: :: POLYNOM1:6

for f being Function
for x, y being set holds rng (f +* x,y) c= (rng f) \/ {y}

proof end;

definition

let A, B be set ;
let f be Function of A,B;
let x be set ;
let y be Element of B;
:: original: +*
redefine func f +* x,y -> Function of A,B;
coherence

proof end;

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

proof end;

end;

theorem Th7: :: POLYNOM1:7

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

proof end;

registration

let A be non empty set ;
let F, G be BinOp of A;
let z, u be Element of A;
cluster doubleLoopStr(# A,F,G,z,u #) -> non empty ;
coherence by STRUCT_0:def 1;

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 ;

end;

registration

let X be set ;
cluster being_linear-order well-ordering Relation of X,X;
existence

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

proof end;

end;

registration

cluster {} -> FinSequence-yielding ;
coherence

proof end;

end;

registration

cluster FinSequence-yielding set ;
existence

proof end;

end;

definition

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

proof end;

end;

registration

let i be Nat;
let f be FinSequence;
cluster i |-> f -> FinSequence-yielding ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

cluster Cardinal-yielding set ;
existence

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

proof end;

end;

registration

cluster -> Cardinal-yielding FinSequence of NAT ;
coherence

proof end;

end;

registration

cluster Cardinal-yielding FinSequence of NAT ;
existence

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

proof end;

end;

registration

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

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

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 ;

end;

registration

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

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

proof end;

end;

theorem Th15: :: POLYNOM1:15

for L being non empty LoopStr
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 LoopStr
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 LoopStr
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 LoopStr
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 HGrStr ;
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

proof end;

correctness ;

end;

:: deftheorem POLYNOM1:def 1 :

:: deftheorem Def2 defines * POLYNOM1:def 2 :

definition

let L be non empty HGrStr ;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines * POLYNOM1:def 3 :

theorem Th19: :: POLYNOM1:19

for L being non empty HGrStr
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 HGrStr
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 HGrStr
for a, b being Element of L holds a * <*b*> = <*(a * b)*>

proof end;

theorem Th22: :: POLYNOM1:22

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

proof end;

theorem Th23: :: POLYNOM1:23

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

proof end;

end;

registration

cluster non empty unital strict multLoopStr_0 ;
existence

proof end;

end;

registration

cluster non empty Abelian add-associative right_zeroed right_complementable unital associative commutative strict distributive Field-like non trivial doubleLoopStr ;
existence

proof end;

end;

theorem :: POLYNOM1:25

canceled;

theorem :: POLYNOM1:26

canceled;

theorem Th27: :: POLYNOM1:27

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

proof end;

theorem Th28: :: POLYNOM1:28

for L being non empty add-associative right_zeroed right_complementable unital distributive 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

proof end;

registration

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

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 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 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 add-associative right_zeroed right_complementable LoopStr
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

cluster natural-yielding -> real-yielding set ;
correctness

proof end;

end;

registration

cluster {} -> real-yielding FinSequence-yielding natural-yielding ;
coherence

proof end;

end;

registration

cluster real-yielding natural-yielding set ;
existence

proof end;

end;

definition

let f be natural-yielding Function;
let x be set ;
:: original: .
redefine func f . x -> Nat;
coherence

proof end;

end;

registration

let f be natural-yielding Function;
let x be set ;
let n be Nat;
cluster f +* x,n -> real-yielding natural-yielding ;
coherence

proof end;

end;

registration

let f be real-yielding Function;
let x be set ;
let n be Nat;
cluster f +* x,n -> real-yielding ;
coherence

proof end;

end;

registration

let X be set ;
cluster -> natural-yielding Relation of X, NAT ;
coherence

proof end;

end;

registration

let X be set ;
cluster real-yielding natural-yielding ManySortedSet of X;
existence

proof end;

end;

registration

let X be set ;
cluster real-yielding ManySortedSet of X;
existence

proof end;

end;

registration

let X be set ;
cluster real-yielding ManySortedSet of X;
existence

proof end;

end;

definition

let X be set ;
let b1, b2 be real-yielding ManySortedSet of X;
canceled;
func b1 + b2 -> ManySortedSet of X means :Def5: :: POLYNOM1:def 5
for x being set holds it . x = (b1 . x) + (b2 . x);
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem POLYNOM1:def 4 :

:: deftheorem Def5 defines + POLYNOM1:def 5 :

definition

let X be set ;
let b1, b2 be natural-yielding 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

proof end;

uniqueness

proof end;

end;

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

theorem :: POLYNOM1:37

for X being set
for b, b1, b2 being real-yielding 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-yielding 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 real-yielding ManySortedSet of X;
cluster b1 + b2 -> real-yielding ;
coherence

proof end;

end;

registration

let X be set ;
let b1, b2 be natural-yielding ManySortedSet of X;
cluster b1 + b2 -> real-yielding natural-yielding ;
coherence

proof end;

cluster b1 -' b2 -> real-yielding natural-yielding ;
coherence

proof end;

end;

theorem Th39: :: POLYNOM1:39

for X being set
for b1, b2, b3 being real-yielding 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-yielding 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines support POLYNOM1:def 7 :

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 :

notation

let f be Function;
synonym f has_finite-support for finite-support f;

end;

registration

cluster {} -> real-yielding FinSequence-yielding natural-yielding finite-support ;
coherence

proof end;

end;

registration

cluster finite -> finite-support set ;
coherence

proof end;

end;

registration

cluster non empty real-yielding natural-yielding finite-support set ;
existence

proof end;

end;

registration

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

end;

registration

let X be set ;
cluster real-yielding natural-yielding finite-support Relation of X, NAT ;
existence

proof end;

end;

registration

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

proof end;

end;

registration

let X be set ;
cluster real-yielding natural-yielding finite-support ManySortedSet of X;
existence

proof end;

end;

theorem Th42: :: POLYNOM1:42

for X being set
for b1, b2 being natural-yielding 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-yielding 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Support POLYNOM1:def 9 :

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 :

notation

let X be non empty set ;
let S be ZeroStr ;
let p be Function of X,S;
synonym p has_finite-Support for finite-Support p;

end;

definition

let X be set ;
mode bag of X is natural-yielding finite-support ManySortedSet of X;

end;

registration

let X be finite set ;
cluster -> finite-support ManySortedSet of X;
coherence

proof end;

end;

registration

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

proof end;

cluster b1 -' b2 -> real-yielding natural-yielding finite-support ;
coherence

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

proof end;

end;

:: deftheorem Def11 defines < POLYNOM1:def 11 :

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 ;

end;

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

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 ;

end;

:: deftheorem Def13 defines divides POLYNOM1:def 13 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines Bags POLYNOM1:def 14 :

definition

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

proof end;

end;

theorem :: POLYNOM1:55

Bags {} = {{} }

proof end;

registration

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

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

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

proof end;

end;

definition

let X be set ;
func EmptyBag X -> Element of Bags X equals :: POLYNOM1:def 15
X --> 0;
coherence

proof end;

end;

:: deftheorem defines EmptyBag POLYNOM1:def 15 :

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 Th64: :: POLYNOM1:64

for n being Ordinal
for b being bag of n holds EmptyBag n <=' b

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines BagOrder POLYNOM1:def 16 :

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

proof end;

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

proof end;

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

proof end;

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

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-yielding ManySortedSet of X holds
( g in it iff for x being set st x in X holds
g . x <= f . x );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines NatMinor POLYNOM1:def 17 :

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

proof end;

end;

registration

let X be set ;
let f be Function of X, NAT ;
cluster -> real-yielding natural-yielding Element of NatMinor f;
coherence

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

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 -> non empty finite functional ;
coherence

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines divisors POLYNOM1:def 18 :

registration

let n be Ordinal;
let b be bag of n;
cluster divisors b -> one-to-one non empty finite-support ;
coherence

proof end;

end;

theorem Th68: :: POLYNOM1:68

for n being Ordinal
for i being 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 Nat
for p being bag of n st i in dom it & p = (divisors b) /. i holds
it /. i = <*p,(b -' p)*> ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines decomp POLYNOM1:def 19 :

theorem Th72: :: POLYNOM1:72

for n being Ordinal
for i being 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 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 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 finite-support ;
coherence

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 finite-support ;
coherence ;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem POLYNOM1:def 20 :

:: deftheorem Def21 defines + POLYNOM1:def 21 :

theorem Th79: :: POLYNOM1:79

for n being set
for L being non empty right_zeroed LoopStr
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 LoopStr ;
let p, q be Series of n,L;
:: original: +
redefine func p + q -> Series of n,L;
commutativity

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 add-associative right_zeroed right_complementable LoopStr ;
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

proof end;

uniqueness

proof end;

involutiveness

proof end;

end;

:: deftheorem Def22 defines - POLYNOM1:def 22 :

definition

let n be set ;
let L be non empty add-associative right_zeroed right_complementable LoopStr ;
let p, q be Series of n,L;
func p - q -> Series of n,L equals :: POLYNOM1:def 23
p + (- q);
coherence ;

end;

:: deftheorem defines - POLYNOM1:def 23 :

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 by FUNCOP_1:57;

end;

:: deftheorem defines 0_ POLYNOM1:def 24 :

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 LoopStr
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 unital multLoopStr_0 ;
func 1_ n,L -> Series of n,L equals :: POLYNOM1:def 25
(0_ n,L) +* (EmptyBag n),(1. L);
coherence ;

end;

:: deftheorem defines 1_ POLYNOM1:def 25 :

theorem Th83: :: POLYNOM1:83

for n being set
for L being non empty add-associative right_zeroed right_complementable LoopStr
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 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 add-associative right_zeroed right_complementable 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 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def26 defines *' POLYNOM1:def 26 :

theorem Th85: :: POLYNOM1:85

for n being Ordinal
for L being non empty Abelian add-associative right_zeroed right_complementable associative distributive 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 Abelian add-associative right_zeroed right_complementable unital associative distributive 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 Abelian add-associative right_zeroed right_complementable commutative doubleLoopStr ;
let p, q be Series of n,L;
:: original: *'
redefine func p *' q -> Series of n,L;
commutativity

proof end;

end;

theorem :: POLYNOM1:87

for n being Ordinal
for L being non empty add-associative right_zeroed right_complementable unital distributive 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 add-associative right_zeroed right_complementable unital distributive non trivial 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 add-associative right_zeroed right_complementable unital distributive non trivial 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

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 LoopStr ;
let p, q be Polynomial of n,L;
cluster p + q -> finite-Support ;
coherence

proof end;

end;

registration

let n be Ordinal;
let L be non empty add-associative right_zeroed right_complementable LoopStr ;
let p be Polynomial of n,L;
cluster - p -> finite-Support ;
coherence

proof end;

end;

registration

let n be Nat;
let L be non empty add-associative right_zeroed right_complementable LoopStr ;
let p, q be Polynomial of n,L;
cluster p - q -> finite-Support ;
coherence ;

end;

registration

let n be Ordinal;
let S be non empty ZeroStr ;
cluster 0_ n,S -> finite-Support ;
coherence

proof end;

end;

registration

let n be Ordinal;
let L be non empty add-associative right_zeroed right_complementable unital right-distributive non trivial doubleLoopStr ;
cluster 1_ n,L -> finite-Support ;
coherence

proof end;

end;

registration

let n be Ordinal;
let L be non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr ;
let p, q be Polynomial of n,L;
cluster p *' q -> finite-Support ;
coherence

proof end;

end;

definition

let n be Ordinal;
let L be non empty add-associative right_zeroed right_complementable unital distributive non trivial 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

proof end;