:: Preliminaries to Polynomials
:: by Andrzej Trybulec
::
:: Copyright (c) 2009-2021 Association of Mizar Users

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

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) = () ^ ()
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;

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

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:8
canceled;

::$CT 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 Th9: :: 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 Th10: :: 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; theorem Th11: :: 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 M being FinSequence st M <> {} 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 object 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 object st x in dom IT holds IT . x is FinSequence ); registration existence ex b1 being Function st b1 is FinSequence-yielding proof end; end; definition let F, G be FinSequence-yielding Function; func F ^^ G -> 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 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 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 being FinSequence-yielding Function for b3 being 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 ) ) ); registration let F, G be FinSequence-yielding Function; coherence proof end; end; 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 Th15: :: PRE_POLY:16 for V, C being set holds PFuncs (V,C) c= bool [:V,C:] proof end; theorem Th16: :: PRE_POLY:17 for V, C being set st V is finite & C is finite holds PFuncs (V,C) is finite proof end; registration existence ex b1 being set st ( b1 is functional & b1 is finite & not b1 is empty ) proof end; end; registration let D be set ; coherence for b1 being FinSequence of D * holds b1 is FinSequence-yielding ; end; registration coherence for b1 being Function st b1 is FinSequence-yielding holds b1 is Function-yielding proof end; end; theorem Th17: :: 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 object ; 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 object ; 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 Th18: :: 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 ; existence ex b1 being Order of X st ( b1 is being_linear-order & b1 is well-ordering ) proof end; end; theorem Th19: :: 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 Th20: :: 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 coherence for b1 being Function st b1 is empty holds b1 is FinSequence-yielding ; end; registration let F, G be FinSequence-yielding FinSequence; coherence proof end; end; registration let i be Element of NAT ; let f be FinSequence; coherence by FUNCOP_1:7; end; registration let F be FinSequence-yielding Function; let x be object ; coherence proof end; end; registration let F be FinSequence; coherence proof end; end; registration existence ex b1 being FinSequence st b1 is Cardinal-yielding proof end; end; theorem Th21: :: 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; coherence proof end; end; registration coherence for b1 being FinSequence of NAT holds b1 is Cardinal-yielding ; end; registration 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 proof end; end; registration let F be FinSequence of NAT ; let i be Element of NAT ; coherence ; end; theorem Th22: :: 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 Th23: :: PRE_POLY:24 for p being set holds Card <*p*> = <*(card p)*> proof end; theorem Th24: :: PRE_POLY:25 for F, G being FinSequence holds Card (F ^ G) = (Card F) ^ (Card G) proof end; registration let X be set ; coherence ; end; registration let f be FinSequence; coherence proof end; end; theorem Th25: :: 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; coherence proof end; end; registration let D be set ; let F be empty FinSequence of D * ; coherence proof end; end; theorem Th26: :: PRE_POLY:27 for D being set for F being FinSequence of D * holds len () = Sum (Card F) proof end; theorem Th27: :: 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 () = len () proof end; theorem Th28: :: PRE_POLY:29 for D being set for F being FinSequence of D * for k being set st k in dom () holds ex i, j being Nat st ( i in dom F & j in dom (F . i) & k = (Sum (Card (F | (i -' 1)))) + j & (F . i) . j = () . k ) proof end; theorem Th29: :: 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 () & (F . i) . j = () . ((Sum (Card (F | (i -' 1)))) + j) ) proof end; theorem Th30: :: 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 ) proof end; registration let f be natural-valued Function; let x be object ; 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 object ; let n be Real; 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 object 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 object 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 object 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 object holds it . x = (b1 . x) -' (b2 . x); existence ex b1 being ManySortedSet of X st for x being object holds b1 . x = (b1 . x) -' (b2 . x) proof end; uniqueness for b1, b2 being ManySortedSet of X st ( for x being object holds b1 . x = (b1 . x) -' (b2 . x) ) & ( for x being object 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 object 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 object st x in X holds b . x = (b1 . x) + (b2 . x) ) holds b = b1 + b2 proof end; theorem Th33: :: PRE_POLY:34 for X being set for b, b1, b2 being natural-valued ManySortedSet of X st ( for x being object 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 Th34: :: 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; definition let f be Function; func support f -> set means :Def7: :: PRE_POLY:def 7 for x being object holds ( x in it iff f . x <> 0 ); existence ex b1 being set st for x being object holds ( x in b1 iff f . x <> 0 ) proof end; uniqueness for b1, b2 being set st ( for x being object holds ( x in b1 iff f . x <> 0 ) ) & ( for x being object 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 object holds ( x in b2 iff f . x <> 0 ) ); theorem Th36: :: 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 coherence for b1 being Function st b1 is finite holds b1 is finite-support proof end; end; registration 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; coherence by Def8; end; registration let X be set ; 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 ; existence ex b1 being ManySortedSet of X st ( b1 is natural-valued & b1 is finite-support ) proof end; end; theorem Th37: :: 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 Th38: :: 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; definition end; registration let X be finite 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 Th39: :: 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 :: 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 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 Th40: :: 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 :: PRE_POLY:def 10 ( p < q or p = q ); reflexivity for p being bag of n holds ( p < p or p = p ) ; end; :: deftheorem 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 Th41: :: PRE_POLY:42 for n being Ordinal for p, q, r being bag of n st p <=' q & q <=' r holds p <=' r by Th40; theorem :: PRE_POLY:43 for n being Ordinal for p, q, r being bag of n st p < q & q <=' r holds p < r by Th40; theorem :: PRE_POLY:44 for n being Ordinal for p, q, r being bag of n st p <=' q & q < r holds p < r by Th40; theorem Th44: :: 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 :: PRE_POLY:def 11 for k being object holds d . k <= b . k; reflexivity for d being bag of X for k being object holds d . k <= d . k ; end; :: deftheorem 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 object holds d . k <= b . k ); theorem Th45: :: PRE_POLY:46 for n being set for d, b being bag of n st ( for k being object st k in n holds d . k <= b . k ) holds d divides b proof end; theorem Th46: :: PRE_POLY:47 for n being set for b1, b2 being bag of n st b1 divides b2 holds (b2 -' b1) + b1 = b2 proof end; theorem Th47: :: PRE_POLY:48 for X being set for b1, b2 being bag of X holds (b2 + b1) -' b1 = b2 proof end; theorem Th48: :: PRE_POLY:49 for n being Ordinal for d, b being bag of n st d divides b holds d <=' b proof end; theorem Th49: :: 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, 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 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 by Def12; 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); coherence for b1 being Element of B holds ( b1 is total & b1 is natural-valued & b1 is finite-support ) by Def12; end; notation let X be set ; synonym EmptyBag X for EmptyMS X; end; definition let X be set ; :: original: EmptyBag redefine func EmptyBag X -> Element of Bags X; coherence EmptyBag X is Element of Bags X proof end; end; :: deftheorem PRE_POLY:def 13 : canceled; ::$CD
theorem :: PRE_POLY:52
canceled;

::$CT theorem :: PRE_POLY:53 for X being set for b being bag of X holds b + () = b proof end; theorem Th52: :: PRE_POLY:54 for X being set for b being bag of X holds b -' () = b proof end; theorem :: PRE_POLY:55 for X being set for b being bag of X holds () -' b = EmptyBag X proof end; theorem Th54: :: PRE_POLY:56 for X being set for b being bag of X holds b -' b = EmptyBag X proof end; theorem Th55: :: 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 :: PRE_POLY:58 for n being set for b being bag of n st b divides EmptyBag n holds EmptyBag n = b ; theorem Th57: :: PRE_POLY:59 for n being set for b being bag of n holds EmptyBag n divides b ; theorem :: PRE_POLY:60 for n being Ordinal for b being bag of n holds EmptyBag n <=' b by ; definition let n be Ordinal; func BagOrder n -> Order of (Bags n) means :Def13: :: 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 Def13 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 by Def13; 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; coherence proof end; end; definition let X be set ; let f be Function of X,NAT; func NatMinor f -> Subset of (Funcs (X,NAT)) means :Def14: :: 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 Def14 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 Th59: :: 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; coherence ( not NatMinor f is empty & NatMinor f is functional ) by Th59; 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 by FUNCT_2:92; end; theorem Th60: :: 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 Th61: :: PRE_POLY:63 for X being non empty set for f being finite-support Function of X,NAT holds card () = multnat$\$ ((),(addnat [:] (f,1)))
proof end;

registration
let X be set ;
let f be finite-support Function of X,NAT;
coherence
proof end;
end;

definition
let n be Ordinal;
let b be bag of n;
func divisors b -> FinSequence of Bags n means :Def15: :: PRE_POLY:def 16
ex S being non empty finite Subset of (Bags n) st
( it = SgmX ((),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 ((),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 ((),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 ((),S) & ( for p being bag of n holds
( p in S iff p divides b ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 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 ((),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;
coherence
( not divisors b is empty & divisors b is one-to-one )
proof end;
end;

theorem Th62: :: PRE_POLY:64
for n being Ordinal
for i being Element of NAT
for b being bag of n st i in dom () holds
() /. i divides b
proof end;

theorem Th63: :: PRE_POLY:65
for n being Ordinal
for b being bag of n holds
( () /. 1 = EmptyBag n & () /. (len ()) = b )
proof end;

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

theorem Th65: :: PRE_POLY:67
for n being Ordinal holds divisors () = <*()*>
proof end;

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

:: deftheorem Def16 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 () & ( for i being Element of NAT
for p being bag of n st i in dom b3 & p = () /. i holds
b3 /. i = <*p,(b -' p)*> ) ) );

theorem Th66: :: PRE_POLY:68
for n being Ordinal
for i being Element of NAT
for b being bag of n st i in dom () holds
ex b1, b2 being bag of n st
( () /. i = <*b1,b2*> & b = b1 + b2 )
proof end;

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

theorem Th68: :: 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 () & () /. i = <*b1,b2*> holds
b1 = () /. i
proof end;

registration
let n be Ordinal;
let b be bag of n;
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;
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
( () /. 1 = <*(),b*> & () /. (len ()) = <*b,()*> )
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 () & () /. i = <*b1,b2*> holds
( b1 <> EmptyBag n & b2 <> EmptyBag n )
proof end;

theorem :: PRE_POLY:73
for n being Ordinal holds decomp () = <*<*(),()*>*>
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 () & dom g = dom () & ( for k being Nat st k in dom f holds
f . k = (decomp ((() /. k) /. 1)) ^^ ((len (decomp ((() /. k) /. 1))) |-> <*((() /. k) /. 2)*>) ) & ( for k being Nat st k in dom g holds
g . k = ((len (decomp ((() /. k) /. 2))) |-> <*((() /. k) /. 1)*>) ^^ (decomp ((() /. k) /. 2)) ) holds
ex p being Permutation of (dom ()) st FlattenSeq g = () * 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 Nat;
coherence
for b1 being FinSequence of n -tuples_on D holds b1 is FinSequence-yielding
;
end;

registration
let k be Nat;
let D be non empty set ;
let M be FinSequence of k -tuples_on D;
let x be set ;
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 ;
coherence
( M /. x is D -valued & M /. x is FinSequence-like )
;
end;

theorem :: PRE_POLY:76
for X being set
for A being empty Subset of X
for R being Order of X st R linearly_orders A holds
SgmX (R,A) = {}
proof end;

theorem Th75: :: PRE_POLY:77
for X being set
for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
for i, j being Element of NAT st i in dom (SgmX (R,A)) & j in dom (SgmX (R,A)) & (SgmX (R,A)) /. i = (SgmX (R,A)) /. j holds
i = j
proof end;

Lm5: for D being set
for p being FinSequence of D st dom p <> {} holds
1 in dom p

proof end;

Lm6: for X being set
for A being finite Subset of X
for a being Element of X
for R being Order of X st R linearly_orders {a} \/ A holds
R linearly_orders A

proof end;

theorem Th76: :: PRE_POLY:78
for X being set
for A being finite Subset of X
for a being Element of X st not a in A holds
for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k in dom (SgmX (R,B)) & (SgmX (R,B)) /. k = a holds
for i being Element of NAT st 1 <= i & i <= k - 1 holds
(SgmX (R,B)) /. i = (SgmX (R,A)) /. i
proof end;

theorem Th77: :: PRE_POLY:79
for X being set
for A being finite Subset of X
for a being Element of X st not a in A holds
for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k in dom (SgmX (R,B)) & (SgmX (R,B)) /. k = a holds
for i being Element of NAT st k <= i & i <= len (SgmX (R,A)) holds
(SgmX (R,B)) /. (i + 1) = (SgmX (R,A)) /. i
proof end;

theorem :: PRE_POLY:80
for X being non empty set
for A being finite Subset of X
for a being Element of X st not a in A holds
for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k + 1 in dom (SgmX (R,B)) & (SgmX (R,B)) /. (k + 1) = a holds
SgmX (R,B) = Ins ((SgmX (R,A)),k,a)
proof end;

theorem :: PRE_POLY:81
for X being set
for b being bag of X st support b = {} holds
b = EmptyBag X by Def7;

Lm7: for X being set
for b being bag of X holds b is PartFunc of X,NAT

proof end;

definition
let X be set ;
let b be bag of X;
:: original: empty-yielding
redefine attr b is empty-yielding means :: PRE_POLY:def 18
b = EmptyBag X;
compatibility
( b is empty-yielding iff b = EmptyBag X )
;
end;

:: deftheorem defines empty-yielding PRE_POLY:def 18 :
for X being set
for b being bag of X holds
( b is empty-yielding iff b = EmptyBag X );

registration
let X be non empty set ;
existence
not for b1 being bag of X holds b1 is V3()
proof end;
end;

definition
let X be set ;
let b be bag of X;
:: original: support
redefine func support b -> finite Subset of X;
coherence
support b is finite Subset of X
proof end;
end;

Lm8: for X being set
for A being Subset of X
for O being Order of X holds
( O is_reflexive_in A & O is_antisymmetric_in A & O is_transitive_in A )

proof end;

theorem :: PRE_POLY:82
for n being Ordinal
for b being bag of n holds RelIncl n linearly_orders support b
proof end;

definition
let X be set ;
let x be FinSequence of X;
let b be bag of X;
:: original: *
redefine func b * x -> PartFunc of NAT,NAT;
coherence
x * b is PartFunc of NAT,NAT
proof end;
end;

registration
let X be set ;
cluster support () -> empty ;
coherence
support () is empty
proof end;
end;