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


begin

definition
let D be set ;
let p, q be Element of D * ;
:: original:^
redefine funcp ^ q ->  Element of D * ;
coherence
 p ^ q is Element of D *
proofend;
end;

registration
let D be set ;
cluster Relation-like NAT -defined D -valued Function-like empty finite countable FinSequence-like FinSubsequence-like for Element of D * ;
existence
 ex b1 being Element of D * st b1 is empty
proofend;
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 *
proofend;
let e be Element of D;
:: original:<*
redefine func<*d,e*> ->  Element of D * ;
coherence
 <*d,e*> is Element of D *
proofend;
end;

begin

registration
let X be set ;
cluster  ->  FinSequence-like for Element of X * ;
coherence
 for b1 being Element of X * holds b1 is FinSequence-like ;
end;

definition
let D be set ;
let F be FinSequence of D * ;
func FlattenSeq F ->  Element of D *  means :Def1: :: PRE_POLY:def 1
 ex g being BinOp of (D *) st
( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) &amp; it = g "**" F );
existence
 ex b1 being Element of D * ex g being BinOp of (D *) st
( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) &amp; b1 = g "**" F )
proofend;
uniqueness
 for b1, b2 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 ) &amp; b1 = g "**" F ) &amp; ex g being BinOp of (D *) st
( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) &amp; b2 = g "**" F ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines FlattenSeq PRE_POLY:def_1_:_
 for D being set
for F being FinSequence of D *
for b3 being Element of D * holds
( b3 = FlattenSeq F iff ex g being BinOp of (D *) st
( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) &amp; b3 = g "**" F ) );

theorem Th1: :: PRE_POLY:1
for D being set
for d being Element of D * holds FlattenSeq <*d*> = d
proofend;

:: from SCMFSA_7, 2006.03.14, A.T.
theorem Th2: :: PRE_POLY:2
for D being set holds FlattenSeq (<*> (D *)) = <*> D
proofend;

theorem Th3: :: PRE_POLY:3
for D being set
for F, G being FinSequence of D * holds FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G)
proofend;

theorem :: PRE_POLY:4
for D being set
for p, q being Element of D * holds FlattenSeq <*p,q*> = p ^ q
proofend;

theorem :: PRE_POLY:5
for D being set
for p, q, r being Element of D * holds FlattenSeq <*p,q,r*> = (p ^ q) ^ r
proofend;

:: from SCMFSA_7, 2007.07.22, A.T.
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
proofend;

begin

scheme :: PRE_POLY:sch 1
Regr1{ F1() ->  Nat, P1[ set ] } :
 for k being Element of NAT st k <= F1() holds
P1[k]
provided
A1: P1[F1()] and
A2: for k being Element of NAT st k < F1() &amp; P1[k + 1] holds
P1[k]
proofend;

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 for Element of bool (Fin X);
existence
 not for b1 being Subset of (Fin X) holds b1 is empty
proofend;
end;

registration
let X be non empty set ;
cluster non empty with_non-empty_elements for Element of bool (Fin X);
existence
 ex b1 being Subset of (Fin X) st
( not b1 is empty &amp; b1 is with_non-empty_elements )
proofend;
end;

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

registration
let X be non empty set ;
cluster with_non-empty_element for Element of bool (Fin X);
existence
 ex b1 being Subset of (Fin X) st b1 is with_non-empty_element
proofend;
end;

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

scheme :: PRE_POLY:sch 2
SubFinite{ F1() ->  set , F2() ->  Subset of F1(), P1[ set ] } :
 P1[F2()]
provided
A1: F2() is finite and
A2: P1[ {} F1()] and
A3: for x being Element of F1()
for B being Subset of F1() st x in F2() &amp; B c= F2() &amp; P1[B] holds
P1[B \/ {x}]
proofend;

registration
let X be non empty set ;
let F be with_non-empty_element Subset of (Fin X);
cluster non empty finite for Element of F;
existence
 ex b1 being Element of F st
( b1 is finite &amp; not b1 is empty )
proofend;
end;

theorem Th8: :: PRE_POLY:8
for A, B being finite set st A c= B &amp; card A = card B holds
A = B
proofend;

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 :Def2: :: PRE_POLY:def 2
( rng it = A &amp; ( for n, m being Nat st n in dom it &amp; m in dom it &amp; n < m holds
( it /. n <> it /. m &amp; [(it /. n),(it /. m)] in R ) ) );
existence
 ex b1 being FinSequence of X st
( rng b1 = A &amp; ( for n, m being Nat st n in dom b1 &amp; m in dom b1 &amp; n < m holds
( b1 /. n <> b1 /. m &amp; [(b1 /. n),(b1 /. m)] in R ) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of X st rng b1 = A &amp; ( for n, m being Nat st n in dom b1 &amp; m in dom b1 &amp; n < m holds
( b1 /. n <> b1 /. m &amp; [(b1 /. n),(b1 /. m)] in R ) ) &amp; rng b2 = A &amp; ( for n, m being Nat st n in dom b2 &amp; m in dom b2 &amp; n < m holds
( b2 /. n <> b2 /. m &amp; [(b2 /. n),(b2 /. m)] in R ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 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 b4 being FinSequence of X holds
( b4 = SgmX (R,A) iff ( rng b4 = A &amp; ( for n, m being Nat st n in dom b4 &amp; m in dom b4 &amp; n < m holds
( b4 /. n <> b4 /. m &amp; [(b4 /. n),(b4 /. 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 &amp; ( for n, m being Nat st n in dom f &amp; m in dom f &amp; n < m holds
( f /. n <> f /. m &amp; [(f /. n),(f /. m)] in R ) ) holds
f = SgmX (R,A)
proofend;

registration
let X be set ;
let F be non empty Subset of (Fin X);
cluster  ->  finite for Element of F;
coherence
 for b1 being Element of F holds b1 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 b1 being Element of F holds b1 is Subset of X
proofend;
end;

theorem Th10: :: 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
proofend;

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

begin

theorem Th12: :: PRE_POLY:12
for n being Nat
for M being FinSequence st len M = n + 1 holds
len (Del (M,(n + 1))) = n
proofend;

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))*>
proofend;

definition
let IT be Function;
attrIT is FinSequence-yielding  means :Def3: :: PRE_POLY:def 3
 for x being set st x in dom IT holds
IT . x is FinSequence;
end;

:: deftheorem Def3 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 for set ;
existence
 ex b1 being Function st b1 is FinSequence-yielding
proofend;
end;

definition
let F, G be FinSequence-yielding Function;
funcF ^^ G ->  FinSequence-yielding Function means :Def4: :: PRE_POLY:def 4
( dom it = (dom F) /\ (dom G) &amp; ( for i being set st i in dom it holds
for f, g being FinSequence st f = F . i &amp; g = G . i holds
it . i = f ^ g ) );
existence
 ex b1 being FinSequence-yielding Function st
( dom b1 = (dom F) /\ (dom G) &amp; ( for i being set st i in dom b1 holds
for f, g being FinSequence st f = F . i &amp; g = G . i holds
b1 . i = f ^ g ) )
proofend;
uniqueness
 for b1, b2 being FinSequence-yielding Function st dom b1 = (dom F) /\ (dom G) &amp; ( for i being set st i in dom b1 holds
for f, g being FinSequence st f = F . i &amp; g = G . i holds
b1 . i = f ^ g ) &amp; dom b2 = (dom F) /\ (dom G) &amp; ( for i being set st i in dom b2 holds
for f, g being FinSequence st f = F . i &amp; g = G . i holds
b2 . i = f ^ g ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines ^^ PRE_POLY:def_4_:_
 for F, G, b3 being FinSequence-yielding Function holds
( b3 = F ^^ G iff ( dom b3 = (dom F) /\ (dom G) &amp; ( for i being set st i in dom b3 holds
for f, g being FinSequence st f = F . i &amp; g = G . i holds
b3 . 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 <> {}
proofend;

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)
proofend;

theorem Th16: :: PRE_POLY:16
for V, C being set holds PFuncs (V,C) c= bool [:V,C:]
proofend;

theorem Th17: :: PRE_POLY:17
for V, C being set st V is finite &amp; C is finite holds
PFuncs (V,C) is finite
proofend;

registration
cluster functional non empty finite for set ;
existence
 ex b1 being set st
( b1 is functional &amp; b1 is finite &amp; not b1 is empty )
proofend;
end;

begin

registration
let D be set ;
cluster  ->  FinSequence-yielding for FinSequence of D * ;
coherence
 for b1 being FinSequence of D * holds b1 is FinSequence-yielding
proofend;
end;

registration
cluster Relation-like Function-like FinSequence-yielding  ->  Function-yielding for set ;
coherence
 for b1 being Function st b1 is FinSequence-yielding holds
b1 is Function-yielding
proofend;
end;

begin

theorem Th18: :: PRE_POLY:18
for X being set
for R being Relation st field R c= X holds
R is Relation of X
proofend;

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

registration
let X be set ;
let f be ManySortedSet of X;
let x, y be set ;
clusterf +* (x,y) -> X -defined total for X -defined Function;
coherence
 for b1 being X -defined Function st b1 = f +* (x,y) holds
b1 is total
proofend;
end;

theorem Th19: :: PRE_POLY:19
for f being one-to-one Function holds card f = card (rng f)
proofend;

definition
let A, X be set ;
let D be non empty FinSequenceSet of A;
let p be PartFunc of X,D;
let i be set ;
:: original:/.
redefine funcp /. 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 quasi_total reflexive antisymmetric transitive well-ordering being_linear-order for Element of bool [:X,X:];
existence
 ex b1 being Order of X st
( b1 is being_linear-order &amp; b1 is well-ordering )
proofend;
end;

theorem Th20: :: 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 &amp; R linearly_orders A &amp; ( for y being Element of X st y in A holds
[x,y] in R ) holds
(SgmX (R,A)) /. 1 = x
proofend;

theorem Th21: :: 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 &amp; R linearly_orders A &amp; ( for y being Element of X st y in A holds
[y,x] in R ) holds
(SgmX (R,A)) /. (len (SgmX (R,A))) = x
proofend;

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 &amp; SgmX (R,A) is one-to-one )
proofend;
end;

registration
cluster Relation-like Function-like empty  ->  FinSequence-yielding for set ;
coherence
 for b1 being Function st b1 is empty holds
b1 is FinSequence-yielding
proofend;
end;

registration
let F, G be FinSequence-yielding FinSequence;
clusterF ^^ G ->  FinSequence-like FinSequence-yielding ;
coherence
 F ^^ G is FinSequence-like
proofend;
end;

registration
let i be Element of NAT ;
let f be FinSequence;
clusteri |-> f ->  FinSequence-yielding ;
coherence
 i |-> f is FinSequence-yielding
proofend;
end;

registration
let F be FinSequence-yielding FinSequence;
let x be set ;
clusterF . x ->  FinSequence-like ;
coherence
 F . x is FinSequence-like
proofend;
end;

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

registration
cluster Relation-like NAT -defined Function-like finite Cardinal-yielding countable FinSequence-like FinSubsequence-like for set ;
existence
 ex b1 being FinSequence st b1 is Cardinal-yielding
proofend;
end;

theorem Th22: :: 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 )
proofend;

registration
let F, G be Cardinal-yielding FinSequence;
clusterF ^ G ->  Cardinal-yielding ;
coherence
 F ^ G is Cardinal-yielding
proofend;
end;

registration
cluster  ->  Cardinal-yielding for FinSequence of NAT ;
coherence
 for b1 being FinSequence of NAT holds b1 is Cardinal-yielding
proofend;
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 natural-valued for FinSequence of NAT ;
existence
 ex b1 being FinSequence of NAT st b1 is Cardinal-yielding
proofend;
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
proofend;
end;

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

theorem Th23: :: PRE_POLY:23
for F being Function
for X being set holds Card (F | X) = (Card F) | X
proofend;

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

theorem Th24: :: PRE_POLY:24
for p being set holds Card <*p*> = <*(card p)*>
proofend;

theorem Th25: :: PRE_POLY:25
for F, G being FinSequence holds Card (F ^ G) = (Card F) ^ (Card G)
proofend;

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
proofend;
end;

theorem Th26: :: 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 )
proofend;

registration
let F, G be FinSequence-yielding FinSequence;
clusterF ^ G ->  FinSequence-yielding ;
coherence
 F ^ G is FinSequence-yielding
proofend;
end;

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

theorem Th27: :: PRE_POLY:27
for D being set
for F being FinSequence of D * holds len (FlattenSeq F) = Sum (Card F)
proofend;

theorem Th28: :: 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)
proofend;

theorem Th29: :: 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 &amp; j in dom (F . i) &amp; k = (Sum (Card (F | (i -' 1)))) + j &amp; (F . i) . j = (FlattenSeq F) . k )
proofend;

theorem Th30: :: 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 &amp; j in dom (F . i) holds
( (Sum (Card (F | (i -' 1)))) + j in dom (FlattenSeq F) &amp; (F . i) . j = (FlattenSeq F) . ((Sum (Card (F | (i -' 1)))) + j) )
proofend;

theorem Th31: :: 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 *
proofend;

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 &amp; v * (FlattenSeq f) = FlattenSeq F )
proofend;

begin

registration
let f be natural-valued Function;
let x be set ;
let n be Nat;
clusterf +* (x,n) ->  natural-valued ;
coherence
 f +* (x,n) is natural-valued
proofend;
end;

registration
let f be real-valued Function;
let x be set ;
let n be real number ;
clusterf +* (x,n) ->  real-valued ;
coherence
 f +* (x,n) is real-valued
proofend;
end;

definition
let X be set ;
let b1, b2 be complex-valued ManySortedSet of X;
:: original:+
redefine funcb1 + 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 ;
compatibility
 for b1 being ManySortedSet of X holds
( b1 = b1 + b2 iff for x being set holds b1 . x = (b1 . x) + (b2 . x) )
proofend;
end;

:: deftheorem Def5 defines + PRE_POLY:def_5_:_
 for X being set
for b1, b2 being complex-valued ManySortedSet of X
for b4 being ManySortedSet of X holds
( b4 = b1 + b2 iff for x being set holds b4 . x = (b1 . x) + (b2 . x) );

definition
let X be set ;
let b1, b2 be natural-valued ManySortedSet of X;
funcb1 -' b2 ->  ManySortedSet of X means :Def6: :: PRE_POLY:def 6
 for x being set holds it . x = (b1 . x) -' (b2 . x);
existence
 ex b1 being ManySortedSet of X st
for x being set holds b1 . x = (b1 . x) -' (b2 . x)
proofend;
uniqueness
 for b1, b2 being ManySortedSet of X st ( for x being set holds b1 . x = (b1 . x) -' (b2 . x) ) &amp; ( for x being set holds b2 . x = (b1 . x) -' (b2 . x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines -' PRE_POLY:def_6_:_
 for X being set
for b1, b2 being natural-valued ManySortedSet of X
for b4 being ManySortedSet of X holds
( b4 = b1 -' b2 iff for x being set holds b4 . 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
proofend;

theorem Th34: :: 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
proofend;

registration
let X be set ;
let b1, b2 be natural-valued ManySortedSet of X;
clusterb1 + b2 ->  natural-valued ;
coherence
 b1 + b2 is natural-valued ;
clusterb1 -' b2 ->  natural-valued ;
coherence
 b1 -' b2 is natural-valued
proofend;
end;

theorem Th35: :: PRE_POLY:35
for X being set
for b1, b2, b3 being real-valued ManySortedSet of X holds (b1 + b2) + b3 = b1 + (b2 + b3)
proofend;

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)
proofend;

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 b1 being set st
for x being set holds
( x in b1 iff f . x <> 0 )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff f . x <> 0 ) ) &amp; ( for x being set holds
( x in b2 iff f . x <> 0 ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines support PRE_POLY:def_7_:_
 for f being Function
for b2 being set holds
( b2 = support f iff for x being set holds
( x in b2 iff f . x <> 0 ) );

theorem Th37: :: PRE_POLY:37
for f being Function holds support f c= dom f
proofend;

definition
let f be Function;
attrf 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 for set ;
coherence
 for b1 being Function st b1 is finite holds
b1 is finite-support
proofend;
end;

registration
cluster Relation-like Function-like non empty natural-valued finite-support for set ;
existence
 ex b1 being Function st
( b1 is natural-valued &amp; b1 is finite-support &amp; not b1 is empty )
proofend;
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 natural-valued finite-support for Element of bool [:X,NAT:];
existence
 ex b1 being Function of X,NAT st b1 is finite-support
proofend;
end;

registration
let f be finite-support Function;
let x, y be set ;
clusterf +* (x,y) ->  finite-support ;
coherence
 f +* (x,y) is finite-support
proofend;
end;

registration
let X be set ;
cluster Relation-like X -defined Function-like total natural-valued finite-support for set ;
existence
 ex b1 being ManySortedSet of X st
( b1 is natural-valued &amp; b1 is finite-support )
proofend;
end;

theorem Th38: :: PRE_POLY:38
for X being set
for b1, b2 being natural-valued ManySortedSet of X holds support (b1 + b2) = (support b1) \/ (support b2)
proofend;

theorem Th39: :: PRE_POLY:39
for X being set
for b1, b2 being natural-valued ManySortedSet of X holds support (b1 -' b2) c= support b1
proofend;

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 for set ;
coherence
 for b1 being ManySortedSet of X holds b1 is finite-support
proofend;
end;

registration
let X be set ;
let b1, b2 be bag of X;
clusterb1 + b2 ->  finite-support ;
coherence
 b1 + b2 is finite-support
proofend;
clusterb1 -' b2 ->  finite-support ;
coherence
 b1 -' b2 is finite-support
proofend;
end;

theorem Th40: :: PRE_POLY:40
for X being set holds X --> 0 is bag of X
proofend;

definition
let n be Ordinal;
let p, q be bag of n;
predp < q means :Def9: :: PRE_POLY:def 9
 ex k being Ordinal st
( p . k < q . k &amp; ( 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 &amp; ( 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 &amp; not q . l = p . l ) )
proofend;
end;

:: deftheorem Def9 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 &amp; ( for l being Ordinal st l in k holds
p . l = q . l ) ) );

theorem Th41: :: PRE_POLY:41
for n being Ordinal
for p, q, r being bag of n st p < q &amp; q < r holds
p < r
proofend;

definition
let n be Ordinal;
let p, q be bag of n;
predp <=' q means :Def10: :: PRE_POLY:def 10
( p < q or p = q );
reflexivity
 for p being bag of n holds
( p < p or p = p ) ;
end;

:: deftheorem Def10 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 Th42: :: PRE_POLY:42
for n being Ordinal
for p, q, r being bag of n st p <=' q &amp; q <=' r holds
p <=' r
proofend;

theorem :: PRE_POLY:43
for n being Ordinal
for p, q, r being bag of n st p < q &amp; q <=' r holds
p < r
proofend;

theorem :: PRE_POLY:44
for n being Ordinal
for p, q, r being bag of n st p <=' q &amp; q < r holds
p < r
proofend;

theorem Th45: :: PRE_POLY:45
for n being Ordinal
for p, q being bag of n holds
( p <=' q or q <=' p )
proofend;

definition
let X be set ;
let d, b be bag of X;
predd divides b means :Def11: :: 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 Def11 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 Th46: :: 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
proofend;

theorem Th47: :: PRE_POLY:47
for n being Ordinal
for b1, b2 being bag of n st b1 divides b2 holds
(b2 -' b1) + b1 = b2
proofend;

theorem Th48: :: PRE_POLY:48
for X being set
for b1, b2 being bag of X holds (b2 + b1) -' b1 = b2
proofend;

theorem Th49: :: PRE_POLY:49
for n being Ordinal
for d, b being bag of n st d divides b holds
d <=' b
proofend;

theorem Th50: :: PRE_POLY:50
for n being set
for b, b1, b2 being bag of n st b = b1 + b2 holds
b1 divides b
proofend;

definition
let X be set ;
func Bags X ->  set  means :Def12: :: PRE_POLY:def 12
 for x being set holds
( x in it iff x is bag of X );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is bag of X )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is bag of X ) ) &amp; ( for x being set holds
( x in b2 iff x is bag of X ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines Bags PRE_POLY:def_12_:_
 for X being set
for b2 being set holds
( b2 = Bags X iff for x being set holds
( x in b2 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)
proofend;
end;

theorem :: PRE_POLY:51
Bags {} = {{}}
proofend;

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

registration
let X be set ;
cluster  ->  functional for Element of bool (Bags X);
coherence
 for b1 being Subset of (Bags X) holds b1 is functional
proofend;
end;

registration
let X be set ;
let B be Subset of (Bags X);
cluster  -> X -defined for Element of B;
coherence
 for b1 being Element of B holds b1 is X -defined
proofend;
end;

registration
let X be set ;
let B be non empty Subset of (Bags X);
cluster  ->  total natural-valued finite-support for Element of B;
coherence
 for b1 being Element of B holds
( b1 is total &amp; b1 is natural-valued &amp; b1 is finite-support ) by Def12;
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
proofend;
end;

:: deftheorem  defines EmptyBag PRE_POLY:def_13_:_
 for X being set holds EmptyBag X = X --> 0;

theorem Th52: :: PRE_POLY:52
for X, x being set holds (EmptyBag X) . x = 0
proofend;

theorem :: PRE_POLY:53
for X being set
for b being bag of X holds b + (EmptyBag X) = b
proofend;

theorem Th54: :: PRE_POLY:54
for X being set
for b being bag of X holds b -' (EmptyBag X) = b
proofend;

theorem :: PRE_POLY:55
for X being set
for b being bag of X holds (EmptyBag X) -' b = EmptyBag X
proofend;

theorem Th56: :: PRE_POLY:56
for X being set
for b being bag of X holds b -' b = EmptyBag X
proofend;

theorem Th57: :: PRE_POLY:57
for n being set
for b1, b2 being bag of n st b1 divides b2 &amp; b2 -' b1 = EmptyBag n holds
b2 = b1
proofend;

theorem Th58: :: PRE_POLY:58
for n being set
for b being bag of n st b divides EmptyBag n holds
EmptyBag n = b
proofend;

theorem Th59: :: PRE_POLY:59
for n being set
for b being bag of n holds EmptyBag n divides b
proofend;

theorem :: PRE_POLY:60
for n being Ordinal
for b being bag of n holds EmptyBag n <=' b by Th49, Th59;

definition
let n be Ordinal;
func BagOrder n ->  Order of (Bags n) means :Def14: :: PRE_POLY:def 14
 for p, q being bag of n holds
( [p,q] in it iff p <=' q );
existence
 ex b1 being Order of (Bags n) st
for p, q being bag of n holds
( [p,q] in b1 iff p <=' q )
proofend;
uniqueness
 for b1, b2 being Order of (Bags n) st ( for p, q being bag of n holds
( [p,q] in b1 iff p <=' q ) ) &amp; ( for p, q being bag of n holds
( [p,q] in b2 iff p <=' q ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def14 defines BagOrder PRE_POLY:def_14_:_
 for n being Ordinal
for b2 being Order of (Bags n) holds
( b2 = BagOrder n iff for p, q being bag of n holds
( [p,q] in b2 iff p <=' q ) );

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

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

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

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

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

definition
let X be set ;
let f be Function of X,NAT;
func NatMinor f ->  Subset of (Funcs (X,NAT)) means :Def15: :: 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 b1 being Subset of (Funcs (X,NAT)) st
for g being natural-valued ManySortedSet of X holds
( g in b1 iff for x being set st x in X holds
g . x <= f . x )
proofend;
uniqueness
 for b1, b2 being Subset of (Funcs (X,NAT)) st ( for g being natural-valued ManySortedSet of X holds
( g in b1 iff for x being set st x in X holds
g . x <= f . x ) ) &amp; ( for g being natural-valued ManySortedSet of X holds
( g in b2 iff for x being set st x in X holds
g . x <= f . x ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def15 defines NatMinor PRE_POLY:def_15_:_
 for X being set
for f being Function of X,NAT
for b3 being Subset of (Funcs (X,NAT)) holds
( b3 = NatMinor f iff for g being natural-valued ManySortedSet of X holds
( g in b3 iff for x being set st x in X holds
g . x <= f . x ) );

theorem Th61: :: PRE_POLY:61
for X being set
for f being Function of X,NAT holds f in NatMinor f
proofend;

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

registration
let X be set ;
let f be Function of X,NAT;
cluster  ->  natural-valued for Element of NatMinor f;
coherence
 for b1 being Element of NatMinor f holds b1 is natural-valued
proofend;
end;

theorem Th62: :: PRE_POLY:62
for X being set
for f being finite-support Function of X,NAT holds NatMinor f c= Bags X
proofend;

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
proofend;
end;

theorem Th63: :: 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)))
proofend;

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

definition
let n be Ordinal;
let b be bag of n;
func divisors b ->  FinSequence of Bags n means :Def16: :: PRE_POLY:def 16
 ex S being non empty finite Subset of (Bags n) st
( it = SgmX ((BagOrder n),S) &amp; ( for p being bag of n holds
( p in S iff p divides b ) ) );
existence
 ex b1 being FinSequence of Bags n ex S being non empty finite Subset of (Bags n) st
( b1 = SgmX ((BagOrder n),S) &amp; ( for p being bag of n holds
( p in S iff p divides b ) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of Bags n st ex S being non empty finite Subset of (Bags n) st
( b1 = SgmX ((BagOrder n),S) &amp; ( for p being bag of n holds
( p in S iff p divides b ) ) ) &amp; ex S being non empty finite Subset of (Bags n) st
( b2 = SgmX ((BagOrder n),S) &amp; ( for p being bag of n holds
( p in S iff p divides b ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def16 defines divisors PRE_POLY:def_16_:_
 for n being Ordinal
for b being bag of n
for b3 being FinSequence of Bags n holds
( b3 = divisors b iff ex S being non empty finite Subset of (Bags n) st
( b3 = SgmX ((BagOrder n),S) &amp; ( 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 &amp; divisors b is one-to-one )
proofend;
end;

theorem Th64: :: 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
proofend;

theorem Th65: :: PRE_POLY:65
for n being Ordinal
for b being bag of n holds
( (divisors b) /. 1 = EmptyBag n &amp; (divisors b) /. (len (divisors b)) = b )
proofend;

theorem Th66: :: PRE_POLY:66
for n being Ordinal
for i being Nat
for b, b1, b2 being bag of n st i > 1 &amp; i < len (divisors b) holds
( (divisors b) /. i <> EmptyBag n &amp; (divisors b) /. i <> b )
proofend;

theorem Th67: :: PRE_POLY:67
for n being Ordinal holds divisors (EmptyBag n) = <*(EmptyBag n)*>
proofend;

definition
let n be Ordinal;
let b be bag of n;
func decomp b ->  FinSequence of 2 -tuples_on (Bags n) means :Def17: :: PRE_POLY:def 17
( dom it = dom (divisors b) &amp; ( for i being Element of NAT
for p being bag of n st i in dom it &amp; p = (divisors b) /. i holds
it /. i = <*p,(b -' p)*> ) );
existence
 ex b1 being FinSequence of 2 -tuples_on (Bags n) st
( dom b1 = dom (divisors b) &amp; ( for i being Element of NAT
for p being bag of n st i in dom b1 &amp; p = (divisors b) /. i holds
b1 /. i = <*p,(b -' p)*> ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of 2 -tuples_on (Bags n) st dom b1 = dom (divisors b) &amp; ( for i being Element of NAT
for p being bag of n st i in dom b1 &amp; p = (divisors b) /. i holds
b1 /. i = <*p,(b -' p)*> ) &amp; dom b2 = dom (divisors b) &amp; ( for i being Element of NAT
for p being bag of n st i in dom b2 &amp; p = (divisors b) /. i holds
b2 /. i = <*p,(b -' p)*> ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines decomp PRE_POLY:def_17_:_
 for n being Ordinal
for b being bag of n
for b3 being FinSequence of 2 -tuples_on (Bags n) holds
( b3 = decomp b iff ( dom b3 = dom (divisors b) &amp; ( for i being Element of NAT
for p being bag of n st i in dom b3 &amp; p = (divisors b) /. i holds
b3 /. i = <*p,(b -' p)*> ) ) );

theorem Th68: :: 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*> &amp; b = b1 + b2 )
proofend;

theorem Th69: :: 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) &amp; (decomp b) /. i = <*b1,b2*> )
proofend;

theorem Th70: :: 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) &amp; (decomp b) /. i = <*b1,b2*> holds
b1 = (divisors b) /. i
proofend;

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 &amp; decomp b is one-to-one &amp; decomp b is FinSequence-yielding )
proofend;
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 &amp; decomp b is one-to-one &amp; 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*> &amp; (decomp b) /. (len (decomp b)) = <*b,(EmptyBag n)*> )
proofend;

theorem :: PRE_POLY:72
for n being Ordinal
for i being Nat
for b, b1, b2 being bag of n st i > 1 &amp; i < len (decomp b) &amp; (decomp b) /. i = <*b1,b2*> holds
( b1 <> EmptyBag n &amp; b2 <> EmptyBag n )
proofend;

theorem :: PRE_POLY:73
for n being Ordinal holds decomp (EmptyBag n) = <*<*(EmptyBag n),(EmptyBag n)*>*>
proofend;

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) &amp; dom g = dom (decomp b) &amp; ( 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)*>) ) &amp; ( 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
proofend;

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)
proofend;

registration
let D be non empty set ;
let n be Element of NAT ;
cluster  ->  FinSequence-yielding for FinSequence of n -tuples_on D;
coherence
 for b1 being FinSequence of n -tuples_on D holds b1 is FinSequence-yielding
proofend;
end;

registration
let k be Element of NAT ;
let D be non empty set ;
let M be FinSequence of k -tuples_on D;
let x be set ;
clusterM /. x ->  Relation-like Function-like ;
coherence
 ( M /. x is Function-like &amp; M /. x is Relation-like ) ;
end;

registration
let k be Element of NAT ;
let D be non empty set ;
let M be FinSequence of k -tuples_on D;
let x be set ;
clusterM /. x -> D -valued FinSequence-like ;
coherence
 ( M /. x is D -valued &amp; M /. x is FinSequence-like ) ;
end;