:: Preliminaries to Polynomials
:: by Andrzej Trybulec
::
:: Received August 7, 2009
:: Copyright (c) 2009 Association of Mizar Users

begin

definition

let D be set ;
let p, q be Element of D * ;
:: original: ^
redefine func p ^ q -> Element of D * ;
coherence
p ^ q is Element of D *

proof end;

end;

registration

let D be set ;
cluster Relation-like NAT -defined D -valued Function-like empty finite countable FinSequence-like FinSubsequence-like Element of D * ;
existence
ex b₁ being Element of D * st b₁ is empty

proof end;

end;

definition

let D be set ;
:: original: <*>
redefine func <*> D -> empty Element of D * ;
coherence
<*> D is empty Element of D * by FINSEQ_1:def 11;

end;

definition

let D be non empty set ;
let d be Element of D;
:: original: <*
redefine func <*d*> -> Element of D * ;
coherence
<*d*> is Element of D *

proof end;

let e be Element of D;
:: original: <*
redefine func <*d,e*> -> Element of D * ;
coherence
<*d,e*> is Element of D *

proof end;

end;

begin

registration

let X be set ;
cluster -> FinSequence-like Element of X * ;
coherence
for b₁ being Element of X * holds b₁ is FinSequence-like ;

end;

definition

let D be set ;
let F be FinSequence of D * ;
func FlattenSeq F -> Element of D * means :Def14: :: PRE_POLY:def 1
ex g being BinOp of (D *) st
( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & it = g "**" F );
existence
ex b₁ being Element of D * ex g being BinOp of (D *) st
( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b₁ = g "**" F )

proof end;

uniqueness
for b₁, b₂ being Element of D * st ex g being BinOp of (D *) st
( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b₁ = g "**" F ) & ex g being BinOp of (D *) st
( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b₂ = g "**" F ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines FlattenSeq PRE_POLY:def 1 :
for D being set
for F being FinSequence of D *
for b₃ being Element of D * holds
( b₃ = FlattenSeq F iff ex g being BinOp of (D *) st
( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b₃ = g "**" F ) );

theorem Th13D: :: PRE_POLY:1

for D being set
for d being Element of D * holds FlattenSeq <*d*> = d

proof end;

theorem Th20D: :: PRE_POLY:2

for D being set holds FlattenSeq (<*> (D *)) = <*> D

proof end;

theorem Th21D: :: PRE_POLY:3

for D being set
for F, G being FinSequence of D * holds FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G)

proof end;

theorem :: PRE_POLY:4

for D being set
for p, q being Element of D * holds FlattenSeq <*p,q*> = p ^ q

proof end;

theorem :: PRE_POLY:5

for D being set
for p, q, r being Element of D * holds FlattenSeq <*p,q,r*> = (p ^ q) ^ r

proof end;

theorem :: PRE_POLY:6

for D being set
for F, G being FinSequence of D * st F c= G holds
FlattenSeq F c= FlattenSeq G

proof end;

begin

scheme :: PRE_POLY:sch 1
Regr1{ F₁() -> Nat, P₁[ set ] } :

for k being Element of NAT st k <= F₁() holds
P₁[k]

provided

A1: P₁[F₁()] and
A2: for k being Element of NAT st k < F₁() & P₁[k + 1] holds
P₁[k]

proof end;

registration

let n be Nat;
cluster Seg (n + 1) -> non empty ;
coherence
not Seg (n + 1) is empty ;

end;

theorem :: PRE_POLY:7

for A being set holds {} |_2 A = {} ;

registration

let X be set ;
cluster non empty Element of bool (Fin X);
existence
not for b₁ being Subset of (Fin X) holds b₁ is empty

proof end;

end;

registration

let X be non empty set ;
cluster non empty with_non-empty_elements Element of bool (Fin X);
existence
ex b₁ being Subset of (Fin X) st
( not b₁ is empty & b₁ is with_non-empty_elements )

proof end;

end;

registration

let X be non empty set ;
let F be non empty with_non-empty_elements Subset of (Fin X);
cluster non empty Element of F;
existence
not for b₁ being Element of F holds b₁ is empty

proof end;

end;

registration

let X be non empty set ;
cluster with_non-empty_element Element of bool (Fin X);
existence
not for b₁ being Subset of (Fin X) holds b₁ is empty-membered

proof end;

end;

definition

let X be non empty set ;
let R be Order of X;
let A be Subset of X;
:: original: |_2
redefine func R |_2 A -> Order of A;
coherence
R |_2 A is Order of A

proof end;

end;

scheme :: PRE_POLY:sch 2
SubFinite{ F₁() -> set , F₂() -> Subset of F₁(), P₁[ set ] } :

P₁[F₂()]

provided

A1: F₂() is finite and
A2: P₁[ {} F₁()] and
A3: for x being Element of F₁()
for B being Subset of F₁() st x in F₂() & B c= F₂() & P₁[B] holds
P₁[B \/ {x}]

proof end;

registration

let X be non empty set ;
let F be with_non-empty_element Subset of (Fin X);
cluster non empty finite Element of F;
existence
ex b₁ being Element of F st
( b₁ is finite & not b₁ is empty )

proof end;

end;

theorem Th3: :: PRE_POLY:8

for A, B being finite set st A c= B & card A = card B holds
A = B

proof end;

definition

let X be set ;
let A be finite Subset of X;
let R be Order of X;
assume A1: R linearly_orders A ;
func SgmX (R,A) -> FinSequence of X means :Def2T: :: PRE_POLY:def 2
( rng it = A & ( for n, m being Nat st n in dom it & m in dom it & n < m holds
( it /. n <> it /. m & [(it /. n),(it /. m)] in R ) ) );
existence
ex b₁ being FinSequence of X st
( rng b₁ = A & ( for n, m being Nat st n in dom b₁ & m in dom b₁ & n < m holds
( b₁ /. n <> b₁ /. m & [(b₁ /. n),(b₁ /. m)] in R ) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of X st rng b₁ = A & ( for n, m being Nat st n in dom b₁ & m in dom b₁ & n < m holds
( b₁ /. n <> b₁ /. m & [(b₁ /. n),(b₁ /. m)] in R ) ) & rng b₂ = A & ( for n, m being Nat st n in dom b₂ & m in dom b₂ & n < m holds
( b₂ /. n <> b₂ /. m & [(b₂ /. n),(b₂ /. m)] in R ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2T defines SgmX PRE_POLY:def 2 :
for X being set
for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
for b₄ being FinSequence of X holds
( b₄ = SgmX (R,A) iff ( rng b₄ = A & ( for n, m being Nat st n in dom b₄ & m in dom b₄ & n < m holds
( b₄ /. n <> b₄ /. m & [(b₄ /. n),(b₄ /. m)] in R ) ) ) );

theorem :: PRE_POLY:9

for X being set
for A being finite Subset of X
for R being Order of X
for f being FinSequence of X st rng f = A & ( for n, m being Nat st n in dom f & m in dom f & n < m holds
( f /. n <> f /. m & [(f /. n),(f /. m)] in R ) ) holds
f = SgmX (R,A)

proof end;

registration

let X be set ;
let F be non empty Subset of (Fin X);
cluster -> finite Element of F;
coherence
for b₁ being Element of F holds b₁ is finite ;

end;

definition

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

proof end;

end;

theorem Th8T: :: PRE_POLY:10

for X being set
for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
SgmX (R,A) is one-to-one

proof end;

theorem :: PRE_POLY:11

for X being set
for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
len (SgmX (R,A)) = card A

proof end;

begin

theorem Th3: :: PRE_POLY:12

for n being Nat
for M being FinSequence st len M = n + 1 holds
len (Del (M,(n + 1))) = n

proof end;

theorem :: PRE_POLY:13

for n being Nat
for M being FinSequence st len M = n + 1 holds
M = (Del (M,(len M))) ^ <*(M . (len M))*>

proof end;

definition

let IT be Function;
attr IT is FinSequence-yielding means :Def1M: :: PRE_POLY:def 3
for x being set st x in dom IT holds
IT . x is FinSequence;

end;

:: deftheorem Def1M defines FinSequence-yielding PRE_POLY:def 3 :
for IT being Function holds
( IT is FinSequence-yielding iff for x being set st x in dom IT holds
IT . x is FinSequence );

registration

cluster Relation-like Function-like FinSequence-yielding set ;
existence
ex b₁ being Function st b₁ is FinSequence-yielding

proof end;

end;

definition

let F, G be FinSequence-yielding Function;
func F ^^ G -> FinSequence-yielding Function means :Def2M: :: PRE_POLY:def 4
( dom it = (dom F) /\ (dom G) & ( for i being set st i in dom it holds
for f, g being FinSequence st f = F . i & g = G . i holds
it . i = f ^ g ) );
existence
ex b₁ being FinSequence-yielding Function st
( dom b₁ = (dom F) /\ (dom G) & ( for i being set st i in dom b₁ holds
for f, g being FinSequence st f = F . i & g = G . i holds
b₁ . i = f ^ g ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence-yielding Function st dom b₁ = (dom F) /\ (dom G) & ( for i being set st i in dom b₁ holds
for f, g being FinSequence st f = F . i & g = G . i holds
b₁ . i = f ^ g ) & dom b₂ = (dom F) /\ (dom G) & ( for i being set st i in dom b₂ holds
for f, g being FinSequence st f = F . i & g = G . i holds
b₂ . i = f ^ g ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2M defines ^^ PRE_POLY:def 4 :
for F, G, b₃ being FinSequence-yielding Function holds
( b₃ = F ^^ G iff ( dom b₃ = (dom F) /\ (dom G) & ( for i being set st i in dom b₃ holds
for f, g being FinSequence st f = F . i & g = G . i holds
b₃ . i = f ^ g ) ) );

begin

theorem :: PRE_POLY:14

for V, C being non empty set ex f being Element of PFuncs (V,C) st f <> {}

proof end;

theorem :: PRE_POLY:15

for V, C being set
for f being Element of PFuncs (V,C)
for g being set st g c= f holds
g in PFuncs (V,C)

proof end;

theorem Th4: :: PRE_POLY:16

for V, C being set holds PFuncs (V,C) c= bool [:V,C:]

proof end;

theorem Th5: :: PRE_POLY:17

for V, C being set st V is finite & C is finite holds
PFuncs (V,C) is finite

proof end;

registration

cluster functional non empty finite set ;
existence
ex b₁ being set st
( b₁ is functional & b₁ is finite & not b₁ is empty )

proof end;

end;

begin

registration

let D be set ;
cluster -> FinSequence-yielding FinSequence of D * ;
coherence
for b₁ being FinSequence of D * holds b₁ is FinSequence-yielding

proof end;

end;

registration

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

proof end;

end;

begin

theorem Th4: :: PRE_POLY:18

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

proof end;

registration

let X be set ;
let f be ManySortedSet of X;
let x, y be set ;
cluster f +* (x,y) -> X -defined ;
coherence
f +* (x,y) is X -defined

proof end;

end;

registration

let X be set ;
let f be ManySortedSet of X;
let x, y be set ;
cluster f +* (x,y) -> X -defined total X -defined Function;
coherence
for b₁ being X -defined Function st b₁ = f +* (x,y) holds
b₁ is total

proof end;

end;

theorem Th7: :: PRE_POLY:19

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 Relation-like X -defined X -valued total reflexive antisymmetric transitive well-ordering being_linear-order Element of bool [:X,X:];
existence
ex b₁ being Order of X st
( b₁ is being_linear-order & b₁ is well-ordering )

proof end;

end;

theorem Th8: :: PRE_POLY:20

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: :: PRE_POLY:21

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 Relation-like Function-like empty -> FinSequence-yielding set ;
coherence
for b₁ being Function st b₁ is empty holds
b₁ is FinSequence-yielding

proof end;

end;

registration

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

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 Relation-like Function-like finite Cardinal-yielding countable FinSequence-like FinSubsequence-like set ;
existence
ex b₁ being FinSequence st b₁ is Cardinal-yielding

proof end;

end;

theorem Th10: :: PRE_POLY:22

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 Relation-like NAT -defined NAT -valued Function-like finite Cardinal-yielding countable FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued rational-valued integer-valued natural-valued 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: :: PRE_POLY:23

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: :: PRE_POLY:24

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

proof end;

theorem Th13: :: PRE_POLY:25

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: :: PRE_POLY:26

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;

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: :: PRE_POLY:27

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

proof end;

theorem Th31: :: PRE_POLY:28

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: :: PRE_POLY:29

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: :: PRE_POLY:30

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 Th35: :: PRE_POLY:31

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 :: PRE_POLY:32

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;

begin

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 Relation-like X -defined Function-like total natural-valued set ;
existence
ex b₁ being ManySortedSet of X st b₁ is natural-valued

proof end;

end;

registration

let X be set ;
cluster Relation-like X -defined Function-like total real-valued set ;
existence
ex b₁ being ManySortedSet of X st b₁ is real-valued

proof end;

end;

registration

let X be set ;
cluster Relation-like X -defined Function-like total real-valued set ;
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;
:: original: +
redefine func b1 + b2 -> ManySortedSet of X means :Def5: :: PRE_POLY: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 Def5 defines + PRE_POLY: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: :: PRE_POLY: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 -' PRE_POLY: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 :: PRE_POLY:33

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: :: PRE_POLY:34

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: :: PRE_POLY:35

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

proof end;

theorem :: PRE_POLY:36

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

proof end;

begin

definition

let f be Function;
func support f -> set means :Def7: :: PRE_POLY: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 PRE_POLY: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: :: PRE_POLY:37

for f being Function holds support f c= dom f

proof end;

definition

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

end;

:: deftheorem Def8 defines finite-support PRE_POLY:def 8 :
for f being Function holds
( f is finite-support iff support f is finite );

registration

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

proof end;

end;

registration

cluster Relation-like Function-like 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 Relation-like X -defined NAT -valued Function-like total quasi_total complex-valued ext-real-valued real-valued rational-valued integer-valued natural-valued finite-support Element of bool [: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 Relation-like X -defined Function-like total natural-valued finite-support set ;
existence
ex b₁ being ManySortedSet of X st
( b₁ is natural-valued & b₁ is finite-support )

proof end;

end;

theorem Th42: :: PRE_POLY:38

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: :: PRE_POLY:39

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

proof end;

begin

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 Relation-like X -defined Function-like total -> finite-support set ;
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: :: PRE_POLY:40

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: :: PRE_POLY:def 9
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 < PRE_POLY:def 9 :
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: :: PRE_POLY:41

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: :: PRE_POLY:def 10
( p < q or p = q );
reflexivity
for p being bag of n holds
( p < p or p = p ) ;

end;

:: deftheorem Def12 defines <=' PRE_POLY:def 10 :
for n being Ordinal
for p, q being bag of n holds
( p <=' q iff ( p < q or p = q ) );

theorem Th46: :: PRE_POLY:42

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

proof end;

theorem :: PRE_POLY:43

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

proof end;

theorem :: PRE_POLY:44

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

proof end;

theorem Th49: :: PRE_POLY:45

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: :: PRE_POLY:def 11
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 PRE_POLY:def 11 :
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: :: PRE_POLY:46

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: :: PRE_POLY:47

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

proof end;

theorem Th52: :: PRE_POLY:48

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

proof end;

theorem Th53: :: PRE_POLY:49

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

proof end;

theorem Th54: :: PRE_POLY:50

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: :: PRE_POLY:def 12
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 PRE_POLY:def 12 :
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 :: PRE_POLY:51

Bags {} = {{}}

proof end;

registration

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

proof end;

end;

registration

let X be set ;
let B be non empty Subset of (Bags X);
cluster -> Relation-like Function-like Element of B;
coherence
for b₁ being Element of B holds
( b₁ is Function-like & b₁ is Relation-like ) by Def14;

end;

registration

let X be set ;
let B be non empty Subset of (Bags X);
cluster -> X -defined Element of B;
coherence
for b₁ being Element of B holds b₁ is X -defined by Def14;

end;

registration

let X be set ;
let B be non empty Subset of (Bags X);
cluster -> total natural-valued finite-support Element of B;
coherence
for b₁ being Element of B holds
( b₁ is total & b₁ is natural-valued & b₁ is finite-support ) by Def14;

end;

definition

let X be set ;
func EmptyBag X -> Element of Bags X equals :: PRE_POLY:def 13
X --> 0;
coherence
X --> 0 is Element of Bags X

proof end;

end;

:: deftheorem defines EmptyBag PRE_POLY:def 13 :
for X being set holds EmptyBag X = X --> 0;

theorem Th56: :: PRE_POLY:52

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

proof end;

theorem :: PRE_POLY:53

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

proof end;

theorem Th58: :: PRE_POLY:54

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

proof end;

theorem :: PRE_POLY:55

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

proof end;

theorem Th60: :: PRE_POLY:56

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

proof end;

theorem Th61: :: PRE_POLY:57

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: :: PRE_POLY:58

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

proof end;

theorem Th63: :: PRE_POLY:59

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

proof end;

theorem :: PRE_POLY:60

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: :: PRE_POLY:def 14
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 PRE_POLY:def 14 :
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: :: PRE_POLY:def 15
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 PRE_POLY:def 15 :
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: :: PRE_POLY:61

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 -> functional non empty ;
coherence
( not NatMinor f is empty & NatMinor f is functional ) by Th65;

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: :: PRE_POLY:62

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: :: PRE_POLY:63

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: :: PRE_POLY:def 16
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 PRE_POLY:def 16 :
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: :: PRE_POLY:64

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: :: PRE_POLY:65

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: :: PRE_POLY:66

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: :: PRE_POLY:67

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: :: PRE_POLY:def 17
( 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 PRE_POLY:def 17 :
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: :: PRE_POLY:68

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: :: PRE_POLY:69

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: :: PRE_POLY:70

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 :: PRE_POLY:71

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 :: PRE_POLY:72

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 :: PRE_POLY:73

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

proof end;

theorem :: PRE_POLY:74

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;

theorem :: PRE_POLY:75

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

proof end;