:: 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 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 for Element of D * ;
existence
ex b1 being Element of D * st b1 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 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 ) & 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 ) & b1 = g "**" F )
proof end;
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 ) & b1 = g "**" F ) & ex g being BinOp of (D *) st
( ( for p, q being Element of D * holds g . (p,q) = p ^ q ) & b2 = g "**" F ) holds
b1 = b2
proof end;
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 ) & b3 = g "**" F ) );

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

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

theorem Th3: :: 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;

:: 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
proof end;

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() & P1[k + 1] holds
P1[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 for Element of bool (Fin X);
existence
not for b1 being Subset of (Fin X) holds b1 is empty
proof end;
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 & b1 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 for Element of F;
existence
not for b1 being Element of F holds b1 is empty
proof end;
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
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{ 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() & B c= F2() & P1[B] holds
P1[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 for Element of F;
existence
ex b1 being Element of F st
( b1 is finite & not b1 is empty )
proof end;
end;

theorem Th8: :: 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 :Def2: :: 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 b1 being FinSequence of X st
( rng b1 = A & ( for n, m being Nat st n in dom b1 & m in dom b1 & n < m holds
( b1 /. n <> b1 /. m & [(b1 /. n),(b1 /. m)] in R ) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of X st rng b1 = A & ( for n, m being Nat st n in dom b1 & m in dom b1 & n < m holds
( b1 /. n <> b1 /. m & [(b1 /. n),(b1 /. m)] in R ) ) & rng b2 = A & ( for n, m being Nat st n in dom b2 & m in dom b2 & n < m holds
( b2 /. n <> b2 /. m & [(b2 /. n),(b2 /. m)] in R ) ) holds
b1 = b2
proof end;
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 & ( for n, m being Nat st n in dom b4 & m in dom b4 & n < m holds
( b4 /. n <> b4 /. m & [(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 & ( 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 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
proof end;
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
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 Th12: :: 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 :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
proof end;
end;

definition
let F, G be FinSequence-yielding Function;
func F ^^ G -> FinSequence-yielding Function means :Def4: :: 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 b1 being FinSequence-yielding Function st
( dom b1 = (dom F) /\ (dom G) & ( for i being set st i in dom b1 holds
for f, g being FinSequence st f = F . i & g = G . i holds
b1 . i = f ^ g ) )
proof end;
uniqueness
for b1, b2 being FinSequence-yielding Function st dom b1 = (dom F) /\ (dom G) & ( for i being set st i in dom b1 holds
for f, g being FinSequence st f = F . i & g = G . i holds
b1 . i = f ^ g ) & dom b2 = (dom F) /\ (dom G) & ( for i being set st i in dom b2 holds
for f, g being FinSequence st f = F . i & g = G . i holds
b2 . i = f ^ g ) holds
b1 = b2
proof end;
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) & ( for i being set st i in dom b3 holds
for f, g being FinSequence st f = F . i & 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 <> {}
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 Th16: :: PRE_POLY:16
for V, C being set holds PFuncs (V,C) c= bool [:V,C:]
proof end;

theorem Th17: :: 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 for set ;
existence
ex b1 being set st
( b1 is functional & b1 is finite & not b1 is empty )
proof end;
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
proof end;
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
proof end;
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
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 for X -defined Function;
coherence
for b1 being X -defined Function st b1 = f +* (x,y) holds
b1 is total
proof end;
end;

theorem Th19: :: 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 non empty FinSequenceSet 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 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 & b1 is well-ordering )
proof end;
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 & 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 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 & 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 for set ;
coherence
for b1 being Function st b1 is empty holds
b1 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 NAT -defined Function-like finite Cardinal-yielding countable FinSequence-like FinSubsequence-like for set ;
existence
ex b1 being FinSequence st b1 is Cardinal-yielding
proof end;
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 )
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 for FinSequence of NAT ;
coherence
for b1 being FinSequence of NAT holds b1 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 natural-valued for FinSequence of NAT ;
existence
ex b1 being FinSequence of NAT st b1 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 Th23: :: 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 Th24: :: PRE_POLY:24
for p being set holds Card <*p*> = <*(card p)*>
proof end;

theorem Th25: :: 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 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 )
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 Th27: :: PRE_POLY:27
for D being set
for F being FinSequence of D * holds len (FlattenSeq F) = Sum (Card F)
proof end;

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)
proof end;

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 & j in dom (F . i) & k = (Sum (Card (F | (i -' 1)))) + j & (F . i) . j = (FlattenSeq F) . k )
proof end;

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 & 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 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 *
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 Nat;
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;

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 ;
compatibility
for b1 being ManySortedSet of X holds
( b1 = b1 + b2 iff for x being set holds b1 . 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 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;
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 b1 being ManySortedSet of X st
for x being set holds b1 . x = (b1 . x) -' (b2 . x)
proof end;
uniqueness
for b1, b2 being ManySortedSet of X st ( for x being set holds b1 . x = (b1 . x) -' (b2 . x) ) & ( for x being set holds b2 . x = (b1 . x) -' (b2 . x) ) holds
b1 = b2
proof end;
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
proof end;

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
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 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)
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 b1 being set st
for x being set holds
( x in b1 iff f . x <> 0 )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff f . x <> 0 ) ) & ( for x being set holds
( x in b2 iff f . x <> 0 ) ) holds
b1 = b2
proof end;
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
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 for set ;
coherence
for b1 being Function st b1 is finite holds
b1 is finite-support
proof end;
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 & b1 is finite-support & not b1 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 natural-valued finite-support for Element of bool [:X,NAT:];
existence
ex b1 being Function of X,NAT st b1 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 for set ;
existence
ex b1 being ManySortedSet of X st
( b1 is natural-valued & b1 is finite-support )
proof end;
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)
proof end;

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
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 for set ;
coherence
for b1 being ManySortedSet of X holds b1 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 Th40: :: 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 :Def9: :: 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 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 & ( 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 & q < r holds
p < r
proof end;

definition
let n be Ordinal;
let p, q be bag of n;
pred p <=' 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 & 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 Th45: :: 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 :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
proof end;

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

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

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

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

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 )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is bag of X ) ) & ( for x being set holds
( x in b2 iff x is bag of X ) ) holds
b1 = b2
proof end;
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)
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 ;
cluster -> functional for Element of bool (Bags X);
coherence
for b1 being Subset of (Bags X) holds b1 is functional
proof end;
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
proof end;
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 & b1 is natural-valued & 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
proof end;
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
proof end;

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

theorem Th54: :: 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 Th56: :: PRE_POLY:56
for X being set
for b being bag of X holds b -' b = EmptyBag X
proof end;

theorem Th57: :: 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 Th58: :: 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 Th59: :: 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 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 )
proof end;
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 ) ) & ( for p, q being bag of n holds
( [p,q] in b2 iff p <=' q ) ) holds
b1 = b2
proof end;
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
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 :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 )
proof end;
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 ) ) & ( 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
proof end;
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
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 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
proof end;
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
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 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)))
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 :Def16: :: 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 b1 being FinSequence of Bags n ex S being non empty finite Subset of (Bags n) st
( b1 = SgmX ((BagOrder n),S) & ( for p being bag of n holds
( p in S iff p divides b ) ) )
proof end;
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) & ( 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
( b2 = SgmX ((BagOrder n),S) & ( for p being bag of n holds
( p in S iff p divides b ) ) ) holds
b1 = b2
proof end;
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) & ( 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 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
proof end;

theorem Th65: :: 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 Th66: :: 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 Th67: :: 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 :Def17: :: 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 b1 being FinSequence of 2 -tuples_on (Bags n) st
( dom b1 = dom (divisors b) & ( for i being Element of NAT
for p being bag of n st i in dom b1 & p = (divisors b) /. i holds
b1 /. i = <*p,(b -' p)*> ) )
proof end;
uniqueness
for b1, b2 being FinSequence of 2 -tuples_on (Bags n) st dom b1 = dom (divisors b) & ( for i being Element of NAT
for p being bag of n st i in dom b1 & p = (divisors b) /. i holds
b1 /. i = <*p,(b -' p)*> ) & dom b2 = dom (divisors b) & ( for i being Element of NAT
for p being bag of n st i in dom b2 & p = (divisors b) /. i holds
b2 /. i = <*p,(b -' p)*> ) holds
b1 = b2
proof end;
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) & ( for i being Element of NAT
for p being bag of n st i in dom b3 & 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*> & b = b1 + b2 )
proof end;

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) & (decomp b) /. i = <*b1,b2*> )
proof end;

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) & (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;

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
proof end;
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 ;
cluster M /. x -> Relation-like Function-like ;
coherence
( M /. x is Function-like & 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 ;
cluster M /. x -> D -valued FinSequence-like ;
coherence
( M /. x is D -valued & M /. x is FinSequence-like ) ;
end;