:: POLYNOM1 semantic presentation

Lemma1: for b₁, b₂ being Nat holds multnat . b₁,b₂ = b₁ * b₂
by BINOP_2:def 24;

theorem Th1: :: POLYNOM1:1

canceled;

theorem Th2: :: POLYNOM1:2

for b₁ being set
for b₂ being non empty set
for b₃ being BinOp of b₂
for b₄ being Function of b₁,b₂
for b₅ being Element of b₂ holds dom (b₃ [:] b₄,b₅) = b₁

proof end;

theorem Th3: :: POLYNOM1:3

for b₁, b₂, b₃ being Nat holds (b₁ -' b₂) -' b₃ = b₁ -' (b₂ + b₃)

proof end;

theorem Th4: :: POLYNOM1:4

for b₁ being set
for b₂ being Relation st field b₂ c= b₁ holds
b₂ is Relation of b₁

proof end;

theorem Th5: :: POLYNOM1:5

for b₁ being non empty LoopStr
for b₂, b₃ being FinSequence of the carrier of b₁ st dom b₂ = dom b₃ holds
dom (b₂ + b₃) = dom b₂

proof end;

theorem Th6: :: POLYNOM1:6

for b₁ being Function
for b₂, b₃ being set holds rng (b₁ +* b₂,b₃) c= (rng b₁) \/ {b₃}

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Function of c₁,c₂;
let c₄ be set ;
let c₅ be Element of c₂;
redefine func +* as c₃ +* c₄,c₅ -> Function of a₁,a₂;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃, c₄ be set ;
redefine func +* as c₂ +* c₃,c₄ -> ManySortedSet of a₁;
coherence

proof end;

end;

theorem Th7: :: POLYNOM1:7

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

proof end;

registration

let c₁ be non empty set ;
let c₂, c₃ be BinOp of c₁;
let c₄, c₅ be Element of c₁;
cluster doubleLoopStr(# a₁,a₂,a₃,a₄,a₅ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

definition

let c₁, c₂ be set ;
let c₃ be FinSequence-DOMAIN of c₁;
let c₄ be PartFunc of c₂,c₃;
let c₅ be set ;
redefine func /. as c₄ /. c₅ -> Element of a₃;
coherence ;

end;

registration

let c₁ be set ;
cluster being_linear-order well-ordering Relation of a₁,a₁;
existence

proof end;

end;

theorem Th8: :: POLYNOM1:8

for b₁ being non empty set
for b₂ being non empty finite Subset of b₁
for b₃ being Order of b₁
for b₄ being Element of b₁ st b₄ in b₂ & b₃ linearly_orders b₂ & ( for b₅ being Element of b₁ st b₅ in b₂ holds
[b₄,b₅] in b₃ ) holds
(SgmX b₃,b₂) /. 1 = b₄

proof end;

theorem Th9: :: POLYNOM1:9

for b₁ being non empty set
for b₂ being non empty finite Subset of b₁
for b₃ being Order of b₁
for b₄ being Element of b₁ st b₄ in b₂ & b₃ linearly_orders b₂ & ( for b₅ being Element of b₁ st b₅ in b₂ holds
[b₅,b₄] in b₃ ) holds
(SgmX b₃,b₂) /. (len (SgmX b₃,b₂)) = b₄

proof end;

registration

let c₁ be non empty set ;
let c₂ be non empty finite Subset of c₁;
let c₃ be being_linear-order Order of c₁;
cluster SgmX a₃,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 c₁, c₂ be FinSequence-yielding FinSequence;
redefine func ^^ as c₁ ^^ c₂ -> FinSequence-yielding FinSequence;
coherence

proof end;

end;

registration

let c₁ be Nat;
let c₂ be FinSequence;
cluster a₁ |-> a₂ -> FinSequence-yielding ;
coherence

proof end;

end;

registration

let c₁ be FinSequence-yielding FinSequence;
let c₂ be set ;
cluster a₁ . a₂ -> FinSequence-like ;
coherence

proof end;

end;

registration

let c₁ be FinSequence;
cluster Card a₁ -> FinSequence-like ;
coherence

proof end;

end;

registration

cluster Cardinal-yielding set ;
existence

proof end;

end;

theorem Th10: :: POLYNOM1:10

for b₁ being Function holds
( b₁ is Cardinal-yielding iff for b₂ being set st b₂ in rng b₁ holds
b₂ is Cardinal )

proof end;

registration

let c₁, c₂ be Cardinal-yielding FinSequence;
cluster a₁ ^ a₂ -> 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 c₁ be set ;
let c₂ be FinSequence of c₁ * ;
redefine func Card as Card c₂ -> Cardinal-yielding FinSequence of NAT ;
coherence

proof end;

end;

registration

let c₁ be FinSequence of NAT ;
let c₂ be Nat;
cluster a₁ | a₂ -> Cardinal-yielding ;
coherence ;

end;

theorem Th11: :: POLYNOM1:11

for b₁ being Function
for b₂ being set holds Card (b₁ | b₂) = (Card b₁) | b₂

proof end;

registration

let c₁ be empty Function;
cluster Card a₁ -> empty ;
coherence

proof end;

end;

theorem Th12: :: POLYNOM1:12

for b₁ being set holds Card <*b₁*> = <*(Card b₁)*>

proof end;

theorem Th13: :: POLYNOM1:13

for b₁, b₂ being FinSequence holds Card (b₁ ^ b₂) = (Card b₁) ^ (Card b₂)

proof end;

registration

let c₁ be set ;
cluster <*> a₁ -> FinSequence-yielding ;
coherence ;

end;

registration

let c₁ be FinSequence;
cluster <*a₁*> -> FinSequence-yielding ;
coherence

proof end;

end;

theorem Th14: :: POLYNOM1:14

for b₁ being Function holds
( b₁ is FinSequence-yielding iff for b₂ being set st b₂ in rng b₁ holds
b₂ is FinSequence )

proof end;

registration

let c₁, c₂ be FinSequence-yielding FinSequence;
cluster a₁ ^ a₂ -> FinSequence-yielding ;
coherence

proof end;

end;

theorem Th15: :: POLYNOM1:15

for b₁ being non empty LoopStr
for b₂ being FinSequence of the carrier of b₁ * holds dom (Sum b₂) = dom b₂

proof end;

theorem Th16: :: POLYNOM1:16

for b₁ being non empty LoopStr
for b₂ being FinSequence of the carrier of b₁ * holds Sum (<*> (the carrier of b₁ * )) = <*> the carrier of b₁

proof end;

theorem Th17: :: POLYNOM1:17

for b₁ being non empty LoopStr
for b₂ being Element of the carrier of b₁ * holds <*(Sum b₂)*> = Sum <*b₂*>

proof end;

theorem Th18: :: POLYNOM1:18

for b₁ being non empty LoopStr
for b₂, b₃ being FinSequence of the carrier of b₁ * holds Sum (b₂ ^ b₃) = (Sum b₂) ^ (Sum b₃)

proof end;

definition

let c₁ be non empty HGrStr ;
let c₂ be FinSequence of the carrier of c₁;
let c₃ be Element of c₁;
canceled;
redefine func * as c₃ * c₂ -> FinSequence of the carrier of a₁ means :Def2: :: POLYNOM1:def 2
( dom a₄ = dom a₂ & ( for b₁ being set st b₁ in dom a₂ holds
a₄ /. b₁ = a₃ * (a₂ /. b₁) ) );
compatibility

proof end;

correctness ;

end;

:: deftheorem Def1 POLYNOM1:def 1 :

:: deftheorem Def2 defines * POLYNOM1:def 2 :

definition

let c₁ be non empty HGrStr ;
let c₂ be FinSequence of the carrier of c₁;
let c₃ be Element of c₁;
func c₂ * c₃ -> FinSequence of the carrier of a₁ means :Def3: :: POLYNOM1:def 3
( dom a₄ = dom a₂ & ( for b₁ being set st b₁ in dom a₂ holds
a₄ /. b₁ = (a₂ /. b₁) * a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines * POLYNOM1:def 3 :

theorem Th19: :: POLYNOM1:19

for b₁ being non empty HGrStr
for b₂ being Element of b₁ holds b₂ * (<*> the carrier of b₁) = <*> the carrier of b₁

proof end;

theorem Th20: :: POLYNOM1:20

for b₁ being non empty HGrStr
for b₂ being Element of b₁ holds (<*> the carrier of b₁) * b₂ = <*> the carrier of b₁

proof end;

theorem Th21: :: POLYNOM1:21

for b₁ being non empty HGrStr
for b₂, b₃ being Element of b₁ holds b₂ * <*b₃*> = <*(b₂ * b₃)*>

proof end;

theorem Th22: :: POLYNOM1:22

for b₁ being non empty HGrStr
for b₂, b₃ being Element of b₁ holds <*b₃*> * b₂ = <*(b₃ * b₂)*>

proof end;

theorem Th23: :: POLYNOM1:23

for b₁ being non empty HGrStr
for b₂ being Element of b₁
for b₃, b₄ being FinSequence of the carrier of b₁ holds b₂ * (b₃ ^ b₄) = (b₂ * b₃) ^ (b₂ * b₄)

proof end;

theorem Th24: :: POLYNOM1:24

for b₁ being non empty HGrStr
for b₂ being Element of b₁
for b₃, b₄ being FinSequence of the carrier of b₁ holds (b₃ ^ b₄) * b₂ = (b₃ * b₂) ^ (b₄ * b₂)

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 Th25: :: POLYNOM1:25

canceled;

theorem Th26: :: POLYNOM1:26

canceled;

theorem Th27: :: POLYNOM1:27

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

proof end;

theorem Th28: :: POLYNOM1:28

for b₁ being non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr
for b₂ being Element of b₁
for b₃ being FinSequence of the carrier of b₁ holds Sum (b₂ * b₃) = b₂ * (Sum b₃)

proof end;

theorem Th29: :: POLYNOM1:29

proof end;

registration

let c₁ be set ;
let c₂ be empty FinSequence of c₁ * ;
cluster FlattenSeq a₂ -> empty ;
coherence

proof end;

end;

theorem Th30: :: POLYNOM1:30

for b₁ being set
for b₂ being FinSequence of b₁ * holds len (FlattenSeq b₂) = Sum (Card b₂)

proof end;

theorem Th31: :: POLYNOM1:31

for b₁, b₂ being set
for b₃ being FinSequence of b₁ *
for b₄ being FinSequence of b₂ * st Card b₃ = Card b₄ holds
len (FlattenSeq b₃) = len (FlattenSeq b₄)

proof end;

theorem Th32: :: POLYNOM1:32

for b₁ being set
for b₂ being FinSequence of b₁ *
for b₃ being set st b₃ in dom (FlattenSeq b₂) holds
ex b₄, b₅ being Nat st
( b₄ in dom b₂ & b₅ in dom (b₂ . b₄) & b₃ = (Sum (Card (b₂ | (b₄ -' 1)))) + b₅ & (b₂ . b₄) . b₅ = (FlattenSeq b₂) . b₃ )

proof end;

theorem Th33: :: POLYNOM1:33

for b₁ being set
for b₂ being FinSequence of b₁ *
for b₃, b₄ being Nat st b₃ in dom b₂ & b₄ in dom (b₂ . b₃) holds
( (Sum (Card (b₂ | (b₃ -' 1)))) + b₄ in dom (FlattenSeq b₂) & (b₂ . b₃) . b₄ = (FlattenSeq b₂) . ((Sum (Card (b₂ | (b₃ -' 1)))) + b₄) )

proof end;

theorem Th34: :: POLYNOM1:34

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being FinSequence of the carrier of b₁ * holds Sum (FlattenSeq b₂) = Sum (Sum b₂)

proof end;

theorem Th35: :: POLYNOM1:35

for b₁, b₂ being non empty set
for b₃ being FinSequence of b₁ *
for b₄ being Function of b₁,b₂ holds ((dom b₃) --> b₄) ** b₃ is FinSequence of b₂ *

proof end;

theorem Th36: :: POLYNOM1:36

for b₁, b₂ being non empty set
for b₃ being FinSequence of b₁ *
for b₄ being Function of b₁,b₂ ex b₅ being FinSequence of b₂ * st
( b₅ = ((dom b₃) --> b₄) ** b₃ & b₄ * (FlattenSeq b₃) = FlattenSeq b₅ )

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 c₁ be natural-yielding Function;
let c₂ be set ;
redefine func . as c₁ . c₂ -> Nat;
coherence

proof end;

end;

registration

let c₁ be natural-yielding Function;
let c₂ be set ;
let c₃ be Nat;
cluster a₁ +* a₂,a₃ -> real-yielding natural-yielding ;
coherence

proof end;

end;

registration

let c₁ be real-yielding Function;
let c₂ be set ;
let c₃ be Nat;
cluster a₁ +* a₂,a₃ -> real-yielding ;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster -> natural-yielding Relation of a₁, NAT ;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster real-yielding natural-yielding ManySortedSet of a₁;
existence

proof end;

end;

registration

let c₁ be set ;
cluster real-yielding ManySortedSet of a₁;
existence

proof end;

end;

registration

let c₁ be set ;
cluster real-yielding ManySortedSet of a₁;
existence

proof end;

end;

definition

let c₁ be set ;
let c₂, c₃ be real-yielding ManySortedSet of c₁;
canceled;
func c₂ + c₃ -> ManySortedSet of a₁ means :Def5: :: POLYNOM1:def 5
for b₁ being set holds a₄ . b₁ = (a₂ . b₁) + (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def4 POLYNOM1:def 4 :

:: deftheorem Def5 defines + POLYNOM1:def 5 :

definition

let c₁ be set ;
let c₂, c₃ be natural-yielding ManySortedSet of c₁;
func c₂ -' c₃ -> ManySortedSet of a₁ means :Def6: :: POLYNOM1:def 6
for b₁ being set holds a₄ . b₁ = (a₂ . b₁) -' (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th37: :: POLYNOM1:37

for b₁ being set
for b₂, b₃, b₄ being real-yielding ManySortedSet of b₁ st ( for b₅ being set st b₅ in b₁ holds
b₂ . b₅ = (b₃ . b₅) + (b₄ . b₅) ) holds
b₂ = b₃ + b₄

proof end;

theorem Th38: :: POLYNOM1:38

for b₁ being set
for b₂, b₃, b₄ being natural-yielding ManySortedSet of b₁ st ( for b₅ being set st b₅ in b₁ holds
b₂ . b₅ = (b₃ . b₅) -' (b₄ . b₅) ) holds
b₂ = b₃ -' b₄

proof end;

registration

let c₁ be set ;
let c₂, c₃ be real-yielding ManySortedSet of c₁;
cluster a₂ + a₃ -> real-yielding ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂, c₃ be natural-yielding ManySortedSet of c₁;
cluster a₂ + a₃ -> real-yielding natural-yielding ;
coherence

proof end;

cluster a₂ -' a₃ -> real-yielding natural-yielding ;
coherence

proof end;

end;

theorem Th39: :: POLYNOM1:39

for b₁ being set
for b₂, b₃, b₄ being real-yielding ManySortedSet of b₁ holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄)

proof end;

theorem Th40: :: POLYNOM1:40

for b₁ being set
for b₂, b₃, b₄ being natural-yielding ManySortedSet of b₁ holds (b₂ -' b₃) -' b₄ = b₂ -' (b₃ + b₄)

proof end;

definition

let c₁ be Function;
func support c₁ -> set means :Def7: :: POLYNOM1:def 7
for b₁ being set holds
( b₁ in a₂ iff a₁ . b₁ <> 0 );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines support POLYNOM1:def 7 :

theorem Th41: :: POLYNOM1:41

for b₁ being Function holds support b₁ c= dom b₁

proof end;

definition

let c₁ be Function;
attr a₁ is finite-support means :Def8: :: POLYNOM1:def 8
support a₁ is finite;

end;

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

notation

let c₁ be Function;
synonym c₁ has_finite-support for finite-support c₁;

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 c₁ be finite-support Function;
cluster support a₁ -> finite ;
coherence by Def8;

end;

registration

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

proof end;

end;

registration

let c₁ be finite-support Function;
let c₂, c₃ be set ;
cluster a₁ +* a₂,a₃ -> finite-support ;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster real-yielding natural-yielding finite-support ManySortedSet of a₁;
existence

proof end;

end;

theorem Th42: :: POLYNOM1:42

for b₁ being set
for b₂, b₃ being natural-yielding ManySortedSet of b₁ holds support (b₂ + b₃) = (support b₂) \/ (support b₃)

proof end;

theorem Th43: :: POLYNOM1:43

for b₁ being set
for b₂, b₃ being natural-yielding ManySortedSet of b₁ holds support (b₂ -' b₃) c= support b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be ZeroStr ;
let c₃ be Function of c₁,c₂;
func Support c₃ -> Subset of a₁ means :Def9: :: POLYNOM1:def 9
for b₁ being Element of a₁ holds
( b₁ in a₄ iff a₃ . b₁ <> 0. a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Support POLYNOM1:def 9 :

definition

let c₁ be non empty set ;
let c₂ be ZeroStr ;
let c₃ be Function of c₁,c₂;
attr a₃ is finite-Support means :Def10: :: POLYNOM1:def 10
Support a₃ is finite;

end;

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

notation

let c₁ be non empty set ;
let c₂ be ZeroStr ;
let c₃ be Function of c₁,c₂;
synonym c₃ has_finite-Support for finite-Support c₃;

end;

definition

let c₁ be set ;
mode bag of a₁ is natural-yielding finite-support ManySortedSet of a₁;

end;

registration

let c₁ be finite set ;
cluster -> finite-support ManySortedSet of a₁;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂, c₃ be bag of c₁;
cluster a₂ + a₃ -> real-yielding natural-yielding finite-support ;
coherence

proof end;

cluster a₂ -' a₃ -> real-yielding natural-yielding finite-support ;
coherence

proof end;

end;

theorem Th44: :: POLYNOM1:44

for b₁ being set holds b₁ --> 0 is bag of b₁

proof end;

definition

let c₁ be Ordinal;
let c₂, c₃ be bag of c₁;
pred c₂ < c₃ means :Def11: :: POLYNOM1:def 11
ex b₁ being Ordinal st
( a₂ . b₁ < a₃ . b₁ & ( for b₂ being Ordinal st b₂ in b₁ holds
a₂ . b₂ = a₃ . b₂ ) );
asymmetry

proof end;

end;

:: deftheorem Def11 defines < POLYNOM1:def 11 :

theorem Th45: :: POLYNOM1:45

for b₁ being Ordinal
for b₂, b₃, b₄ being bag of b₁ st b₂ < b₃ & b₃ < b₄ holds
b₂ < b₄

proof end;

definition

let c₁ be Ordinal;
let c₂, c₃ be bag of c₁;
pred c₂ <=' c₃ means :Def12: :: POLYNOM1:def 12
( a₂ < a₃ or a₂ = a₃ );
reflexivity ;

end;

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

theorem Th46: :: POLYNOM1:46

for b₁ being Ordinal
for b₂, b₃, b₄ being bag of b₁ st b₂ <=' b₃ & b₃ <=' b₄ holds
b₂ <=' b₄

proof end;

theorem Th47: :: POLYNOM1:47

for b₁ being Ordinal
for b₂, b₃, b₄ being bag of b₁ st b₂ < b₃ & b₃ <=' b₄ holds
b₂ < b₄

proof end;

theorem Th48: :: POLYNOM1:48

for b₁ being Ordinal
for b₂, b₃, b₄ being bag of b₁ st b₂ <=' b₃ & b₃ < b₄ holds
b₂ < b₄

proof end;

theorem Th49: :: POLYNOM1:49

for b₁ being Ordinal
for b₂, b₃ being bag of b₁ holds
( b₂ <=' b₃ or b₃ <=' b₂ )

proof end;

definition

let c₁ be set ;
let c₂, c₃ be bag of c₁;
pred c₂ divides c₃ means :Def13: :: POLYNOM1:def 13
for b₁ being set holds a₂ . b₁ <= a₃ . b₁;
reflexivity ;

end;

:: deftheorem Def13 defines divides POLYNOM1:def 13 :

theorem Th50: :: POLYNOM1:50

for b₁ being set
for b₂, b₃ being bag of b₁ st ( for b₄ being set st b₄ in b₁ holds
b₂ . b₄ <= b₃ . b₄ ) holds
b₂ divides b₃

proof end;

theorem Th51: :: POLYNOM1:51

for b₁ being Ordinal
for b₂, b₃ being bag of b₁ st b₂ divides b₃ holds
(b₃ -' b₂) + b₂ = b₃

proof end;

theorem Th52: :: POLYNOM1:52

for b₁ being set
for b₂, b₃ being bag of b₁ holds (b₃ + b₂) -' b₂ = b₃

proof end;

theorem Th53: :: POLYNOM1:53

for b₁ being Ordinal
for b₂, b₃ being bag of b₁ st b₂ divides b₃ holds
b₂ <=' b₃

proof end;

theorem Th54: :: POLYNOM1:54

for b₁ being set
for b₂, b₃, b₄ being bag of b₁ st b₂ = b₃ + b₄ holds
b₃ divides b₂

proof end;

definition

let c₁ be set ;
func Bags c₁ -> set means :Def14: :: POLYNOM1:def 14
for b₁ being set holds
( b₁ in a₂ iff b₁ is bag of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines Bags POLYNOM1:def 14 :

definition

let c₁ be set ;
redefine func Bags as Bags c₁ -> Subset of (Bags a₁);
coherence

proof end;

end;

theorem Th55: :: POLYNOM1:55

Bags {} = {{} }

proof end;

registration

let c₁ be set ;
cluster Bags a₁ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be non empty Subset of (Bags c₁);
redefine mode Element as Element of c₂ -> bag of a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be non empty 1-sorted ;
let c₃ be Function of Bags c₁,c₂;
let c₄ be bag of c₁;
redefine func . as c₃ . c₄ -> Element of a₂;
coherence

proof end;

end;

definition

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

proof end;

end;

:: deftheorem Def15 defines EmptyBag POLYNOM1:def 15 :

theorem Th56: :: POLYNOM1:56

for b₁, b₂ being set holds (EmptyBag b₁) . b₂ = 0

proof end;

theorem Th57: :: POLYNOM1:57

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

proof end;

theorem Th58: :: POLYNOM1:58

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

proof end;

theorem Th59: :: POLYNOM1:59

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

proof end;

theorem Th60: :: POLYNOM1:60

for b₁ being set
for b₂ being bag of b₁ holds b₂ -' b₂ = EmptyBag b₁

proof end;

theorem Th61: :: POLYNOM1:61

for b₁ being set
for b₂, b₃ being bag of b₁ st b₂ divides b₃ & b₃ -' b₂ = EmptyBag b₁ holds
b₃ = b₂

proof end;

theorem Th62: :: POLYNOM1:62

for b₁ being set
for b₂ being bag of b₁ st b₂ divides EmptyBag b₁ holds
EmptyBag b₁ = b₂

proof end;

theorem Th63: :: POLYNOM1:63

for b₁ being set
for b₂ being bag of b₁ holds EmptyBag b₁ divides b₂

proof end;

theorem Th64: :: POLYNOM1:64

for b₁ being Ordinal
for b₂ being bag of b₁ holds EmptyBag b₁ <=' b₂

proof end;

definition

let c₁ be Ordinal;
func BagOrder c₁ -> Order of Bags a₁ means :Def16: :: POLYNOM1:def 16
for b₁, b₂ being bag of a₁ holds
( [b₁,b₂] in a₂ iff b₁ <=' b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines BagOrder POLYNOM1:def 16 :

Lemma69: for b₁ being Ordinal holds BagOrder b₁ is_reflexive_in Bags b₁

proof end;

Lemma70: for b₁ being Ordinal holds BagOrder b₁ is_antisymmetric_in Bags b₁

proof end;

Lemma71: for b₁ being Ordinal holds BagOrder b₁ is_transitive_in Bags b₁

proof end;

Lemma72: for b₁ being Ordinal holds BagOrder b₁ linearly_orders Bags b₁

proof end;

registration

let c₁ be Ordinal;
cluster BagOrder a₁ -> being_linear-order ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be Function of c₁, NAT ;
func NatMinor c₂ -> Subset of (Funcs a₁,NAT ) means :Def17: :: POLYNOM1:def 17
for b₁ being natural-yielding ManySortedSet of a₁ holds
( b₁ in a₃ iff for b₂ being set st b₂ in a₁ holds
b₁ . b₂ <= a₂ . b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines NatMinor POLYNOM1:def 17 :

theorem Th65: :: POLYNOM1:65

for b₁ being set
for b₂ being Function of b₁, NAT holds b₂ in NatMinor b₂

proof end;

registration

let c₁ be set ;
let c₂ be Function of c₁, NAT ;
cluster NatMinor a₂ -> non empty functional ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be Function of c₁, NAT ;
cluster -> real-yielding natural-yielding Element of NatMinor a₂;
coherence

proof end;

end;

theorem Th66: :: POLYNOM1:66

for b₁ being set
for b₂ being finite-support Function of b₁, NAT holds NatMinor b₂ c= Bags b₁

proof end;

definition

let c₁ be set ;
let c₂ be finite-support Function of c₁, NAT ;
redefine func support as support c₂ -> Element of Fin a₁;
coherence

proof end;

end;

theorem Th67: :: POLYNOM1:67

for b₁ being non empty set
for b₂ being finite-support Function of b₁, NAT holds Card (NatMinor b₂) = multnat $$ (support b₂),(addnat [:] b₂,1)

proof end;

registration

let c₁ be set ;
let c₂ be finite-support Function of c₁, NAT ;
cluster NatMinor a₂ -> non empty finite functional ;
coherence

proof end;

end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines divisors POLYNOM1:def 18 :

registration

let c₁ be Ordinal;
let c₂ be bag of c₁;
cluster divisors a₂ -> one-to-one non empty finite-support ;
coherence

proof end;

end;

theorem Th68: :: POLYNOM1:68

for b₁ being Ordinal
for b₂ being Nat
for b₃ being bag of b₁ st b₂ in dom (divisors b₃) holds
(divisors b₃) /. b₂ divides b₃

proof end;

theorem Th69: :: POLYNOM1:69

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

proof end;

theorem Th70: :: POLYNOM1:70

for b₁ being Ordinal
for b₂ being Nat
for b₃, b₄, b₅ being bag of b₁ st b₂ > 1 & b₂ < len (divisors b₃) holds
( (divisors b₃) /. b₂ <> EmptyBag b₁ & (divisors b₃) /. b₂ <> b₃ )

proof end;

theorem Th71: :: POLYNOM1:71

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

proof end;

definition

let c₁ be Ordinal;
let c₂ be bag of c₁;
func decomp c₂ -> FinSequence of 2 -tuples_on (Bags a₁) means :Def19: :: POLYNOM1:def 19
( dom a₃ = dom (divisors a₂) & ( for b₁ being Nat
for b₂ being bag of a₁ st b₁ in dom a₃ & b₂ = (divisors a₂) /. b₁ holds
a₃ /. b₁ = <*b₂,(a₂ -' b₂)*> ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines decomp POLYNOM1:def 19 :

theorem Th72: :: POLYNOM1:72

for b₁ being Ordinal
for b₂ being Nat
for b₃ being bag of b₁ st b₂ in dom (decomp b₃) holds
ex b₄, b₅ being bag of b₁ st
( (decomp b₃) /. b₂ = <*b₄,b₅*> & b₃ = b₄ + b₅ )

proof end;

theorem Th73: :: POLYNOM1:73

for b₁ being Ordinal
for b₂, b₃, b₄ being bag of b₁ st b₂ = b₃ + b₄ holds
ex b₅ being Nat st
( b₅ in dom (decomp b₂) & (decomp b₂) /. b₅ = <*b₃,b₄*> )

proof end;

theorem Th74: :: POLYNOM1:74

for b₁ being Ordinal
for b₂ being Nat
for b₃, b₄, b₅ being bag of b₁ st b₂ in dom (decomp b₃) & (decomp b₃) /. b₂ = <*b₄,b₅*> holds
b₄ = (divisors b₃) /. b₂

proof end;

registration

let c₁ be Ordinal;
let c₂ be bag of c₁;
cluster decomp a₂ -> one-to-one non empty FinSequence-yielding finite-support ;
coherence

proof end;

end;

registration

let c₁ be Ordinal;
let c₂ be Element of Bags c₁;
cluster decomp a₂ -> one-to-one non empty FinSequence-yielding finite-support ;
coherence ;

end;

theorem Th75: :: POLYNOM1:75

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

proof end;

theorem Th76: :: POLYNOM1:76

for b₁ being Ordinal
for b₂ being Nat
for b₃, b₄, b₅ being bag of b₁ st b₂ > 1 & b₂ < len (decomp b₃) & (decomp b₃) /. b₂ = <*b₄,b₅*> holds
( b₄ <> EmptyBag b₁ & b₅ <> EmptyBag b₁ )

proof end;

theorem Th77: :: POLYNOM1:77

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

proof end;

theorem Th78: :: POLYNOM1:78

for b₁ being Ordinal
for b₂ being bag of b₁
for b₃, b₄ being FinSequence of (3 -tuples_on (Bags b₁)) * st dom b₃ = dom (decomp b₂) & dom b₄ = dom (decomp b₂) & ( for b₅ being Nat st b₅ in dom b₃ holds
b₃ . b₅ = (decomp (((decomp b₂) /. b₅) /. 1)) ^^ ((len (decomp (((decomp b₂) /. b₅) /. 1))) |-> <*(((decomp b₂) /. b₅) /. 2)*>) ) & ( for b₅ being Nat st b₅ in dom b₄ holds
b₄ . b₅ = ((len (decomp (((decomp b₂) /. b₅) /. 2))) |-> <*(((decomp b₂) /. b₅) /. 1)*>) ^^ (decomp (((decomp b₂) /. b₅) /. 2)) ) holds
ex b₅ being Permutation of dom (FlattenSeq b₃) st FlattenSeq b₄ = (FlattenSeq b₃) * b₅

proof end;

definition

let c₁ be set ;
let c₂ be 1-sorted ;
mode Series of a₁,a₂ is Function of Bags a₁,a₂;

end;

definition

let c₁ be set ;
let c₂ be non empty LoopStr ;
let c₃, c₄ be Series of c₁,c₂;
canceled;
func c₃ + c₄ -> Series of a₁,a₂ means :Def21: :: POLYNOM1:def 21
for b₁ being bag of a₁ holds a₅ . b₁ = (a₃ . b₁) + (a₄ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 POLYNOM1:def 20 :

:: deftheorem Def21 defines + POLYNOM1:def 21 :

theorem Th79: :: POLYNOM1:79

for b₁ being set
for b₂ being non empty right_zeroed LoopStr
for b₃, b₄ being Series of b₁,b₂ holds Support (b₃ + b₄) c= (Support b₃) \/ (Support b₄)

proof end;

definition

let c₁ be set ;
let c₂ be non empty Abelian right_zeroed LoopStr ;
let c₃, c₄ be Series of c₁,c₂;
redefine func + as c₃ + c₄ -> Series of a₁,a₂;
commutativity

proof end;

end;

theorem Th80: :: POLYNOM1:80

for b₁ being set
for b₂ being non empty add-associative right_zeroed doubleLoopStr
for b₃, b₄, b₅ being Series of b₁,b₂ holds (b₃ + b₄) + b₅ = b₃ + (b₄ + b₅)

proof end;

definition

let c₁ be set ;
let c₂ be non empty add-associative right_zeroed right_complementable LoopStr ;
let c₃ be Series of c₁,c₂;
func - c₃ -> Series of a₁,a₂ means :Def22: :: POLYNOM1:def 22
for b₁ being bag of a₁ holds a₄ . b₁ = - (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

involutiveness

proof end;

end;

:: deftheorem Def22 defines - POLYNOM1:def 22 :

definition

let c₁ be set ;
let c₂ be non empty add-associative right_zeroed right_complementable LoopStr ;
let c₃, c₄ be Series of c₁,c₂;
func c₃ - c₄ -> Series of a₁,a₂ equals :: POLYNOM1:def 23
a₃ + (- a₄);
coherence ;

end;

:: deftheorem Def23 defines - POLYNOM1:def 23 :

definition

let c₁ be set ;
let c₂ be non empty ZeroStr ;
func 0_ c₁,c₂ -> Series of a₁,a₂ equals :: POLYNOM1:def 24
(Bags a₁) --> (0. a₂);
coherence by FUNCOP_1:57;

end;

:: deftheorem Def24 defines 0_ POLYNOM1:def 24 :

theorem Th81: :: POLYNOM1:81

for b₁ being set
for b₂ being non empty ZeroStr
for b₃ being bag of b₁ holds (0_ b₁,b₂) . b₃ = 0. b₂

proof end;

theorem Th82: :: POLYNOM1:82

for b₁ being set
for b₂ being non empty right_zeroed LoopStr
for b₃ being Series of b₁,b₂ holds b₃ + (0_ b₁,b₂) = b₃

proof end;

definition

let c₁ be set ;
let c₂ be non empty unital multLoopStr_0 ;
func 1_ c₁,c₂ -> Series of a₁,a₂ equals :: POLYNOM1:def 25
(0_ a₁,a₂) +* (EmptyBag a₁),(1. a₂);
coherence ;

end;

:: deftheorem Def25 defines 1_ POLYNOM1:def 25 :

theorem Th83: :: POLYNOM1:83

for b₁ being set
for b₂ being non empty add-associative right_zeroed right_complementable LoopStr
for b₃ being Series of b₁,b₂ holds b₃ - b₃ = 0_ b₁,b₂

proof end;

theorem Th84: :: POLYNOM1:84

for b₁ being set
for b₂ being non empty unital multLoopStr_0 holds
( (1_ b₁,b₂) . (EmptyBag b₁) = 1. b₂ & ( for b₃ being bag of b₁ st b₃ <> EmptyBag b₁ holds
(1_ b₁,b₂) . b₃ = 0. b₂ ) )

proof end;

definition

let c₁ be Ordinal;
let c₂ be non empty add-associative right_zeroed right_complementable doubleLoopStr ;
let c₃, c₄ be Series of c₁,c₂;
func c₃ *' c₄ -> Series of a₁,a₂ means :Def26: :: POLYNOM1:def 26
for b₁ being bag of a₁ ex b₂ being FinSequence of the carrier of a₂ st
( a₅ . b₁ = Sum b₂ & len b₂ = len (decomp b₁) & ( for b₃ being Nat st b₃ in dom b₂ holds
ex b₄, b₅ being bag of a₁ st
( (decomp b₁) /. b₃ = <*b₄,b₅*> & b₂ /. b₃ = (a₃ . b₄) * (a₄ . b₅) ) ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th85: :: POLYNOM1:85

for b₁ being Ordinal
for b₂ being non empty Abelian add-associative right_zeroed right_complementable associative distributive doubleLoopStr
for b₃, b₄, b₅ being Series of b₁,b₂ holds b₃ *' (b₄ + b₅) = (b₃ *' b₄) + (b₃ *' b₅)

proof end;

theorem Th86: :: POLYNOM1:86

for b₁ being Ordinal
for b₂ being non empty Abelian add-associative right_zeroed right_complementable unital associative distributive doubleLoopStr
for b₃, b₄, b₅ being Series of b₁,b₂ holds (b₃ *' b₄) *' b₅ = b₃ *' (b₄ *' b₅)

proof end;

definition

let c₁ be Ordinal;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable commutative doubleLoopStr ;
let c₃, c₄ be Series of c₁,c₂;
redefine func *' as c₃ *' c₄ -> Series of a₁,a₂;
commutativity

proof end;

end;

theorem Th87: :: POLYNOM1:87

for b₁ being Ordinal
for b₂ being non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr
for b₃ being Series of b₁,b₂ holds b₃ *' (0_ b₁,b₂) = 0_ b₁,b₂

proof end;

theorem Th88: :: POLYNOM1:88

for b₁ being Ordinal
for b₂ being non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for b₃ being Series of b₁,b₂ holds b₃ *' (1_ b₁,b₂) = b₃

proof end;

theorem Th89: :: POLYNOM1:89

proof end;

registration

let c₁ be set ;
let c₂ be non empty ZeroStr ;
cluster finite-Support Relation of Bags a₁,the carrier of a₂;
existence

proof end;

end;

definition

let c₁ be Ordinal;
let c₂ be non empty ZeroStr ;
mode Polynomial of a₁,a₂ is finite-Support Series of a₁,a₂;

end;

registration

let c₁ be Ordinal;
let c₂ be non empty right_zeroed LoopStr ;
let c₃, c₄ be Polynomial of c₁,c₂;
cluster a₃ + a₄ -> finite-Support ;
coherence

proof end;

end;

registration

let c₁ be Ordinal;
let c₂ be non empty add-associative right_zeroed right_complementable LoopStr ;
let c₃ be Polynomial of c₁,c₂;
cluster - a₃ -> finite-Support ;
coherence

proof end;

end;

registration

let c₁ be Nat;
let c₂ be non empty add-associative right_zeroed right_complementable LoopStr ;
let c₃, c₄ be Polynomial of c₁,c₂;
cluster a₃ - a₄ -> finite-Support ;
coherence ;

end;

registration

let c₁ be Ordinal;
let c₂ be non empty ZeroStr ;
cluster 0_ a₁,a₂ -> finite-Support ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

let c₁ be Ordinal;
let c₂ be non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr ;
let c₃, c₄ be Polynomial of c₁,c₂;
cluster a₃ *' a₄ -> finite-Support ;
coherence

proof end;

end;

definition

let c₁ be Ordinal;
let c₂ be non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr ;
func Polynom-Ring c₁,c₂ -> non empty strict doubleLoopStr means :Def27: :: POLYNOM1:def 27
( ( for b₁ being set holds
( b₁ in the carrier of a₃ iff b₁ is Polynomial of a₁,a₂ ) ) & ( for b₁, b₂ being Element of a₃
for b₃, b₄ being Polynomial of a₁,a₂ st b₁ = b₃ & b₂ = b₄ holds
b₁ + b₂ = b₃ + b₄ ) & ( for b₁, b₂ being Element of a₃
for b₃, b₄ being Polynomial of a₁,a₂ st b₁ = b₃ & b₂ = b₄ holds
b₁ * b₂ = b₃ *' b₄ ) & 0. a₃ = 0_ a₁,a₂ & 1_ a₃ = 1_ a₁,a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def27 defines Polynom-Ring POLYNOM1:def 27 :

registration

let c₁ be Ordinal;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr ;
cluster Polynom-Ring a₁,a₂ -> non empty Abelian strict ;
coherence

proof end;

end;

registration

let c₁ be Ordinal;
let c₂ be non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr ;
cluster Polynom-Ring a₁,a₂ -> non empty add-associative strict ;
coherence

proof end;

end;

registration

proof end;

end;

registration

proof end;

end;

registration

let c₁ be Ordinal;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable unital commutative distributive non trivial doubleLoopStr ;
cluster Polynom-Ring a₁,a₂ -> non empty Abelian add-associative right_zeroed right_complementable commutative strict ;
coherence

proof end;

end;

registration

let c₁ be Ordinal;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable unital associative distributive non trivial doubleLoopStr ;
cluster Polynom-Ring a₁,a₂ -> non empty Abelian add-associative right_zeroed right_complementable associative strict ;
coherence

proof end;

end;

E104: now

let c₁ be Ordinal;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable unital associative distributive non trivial doubleLoopStr ;
set c₃ = Polynom-Ring c₁,c₂;
let c₄, c₅ be Element of (Polynom-Ring c₁,c₂);
assume E105: c₅ = 1_ (Polynom-Ring c₁,c₂) ;
reconsider c₆ = c₄ as Polynomial of c₁,c₂ by Def27;
E106: 1_ (Polynom-Ring c₁,c₂) = 1_ c₁,c₂ by Def27;
hence c₄ * c₅ = c₆ *' (1_ c₁,c₂) by E105, Def27
.= c₄ by Th88 ;

thus c₅ * c₄ = (1_ c₁,c₂) *' c₆ by E106, E105, Def27
.= c₄ by Th89 ;

end;

registration

proof end;

end;

theorem Th90: :: POLYNOM1:90

for b₁ being Ordinal
for b₂ being non empty Abelian add-associative right_zeroed right_complementable unital associative distributive non trivial doubleLoopStr holds 1. (Polynom-Ring b₁,b₂) = 1_ b₁,b₂

proof end;

theorem Th91: :: POLYNOM1:91

for b₁ being set
for b₂, b₃ being real-yielding ManySortedSet of b₁ holds support (b₂ + b₃) c= (support b₂) \/ (support b₃)

proof end;