:: Preliminaries to Polynomials
:: by Andrzej Trybulec
::
:: Received August 7, 2009
:: Copyright (c) 2009-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, RELAT_1, ORDINAL4, FINSEQ_1, XBOOLE_0,
BINOP_1, FUNCT_1, FINSOP_1, SETWISEO, XXREAL_0, TARSKI, NAT_1, ARYTM_3,
WELLORD1, FINSUB_1, SETFAM_1, ORDERS_1, FINSET_1, ZFMISC_1, CARD_1,
PARTFUN1, ARROW, ORDINAL2, ORDINAL1, RELAT_2, ARYTM_1, FINSEQ_3,
FUNCOP_1, PBOOLE, FUNCT_4, FINSEQ_2, CARD_3, MEMBER_1, VALUED_0, FUNCT_2,
BINOP_2, CLASSES1, PRE_POLY, FINSEQ_5, XCMPLX_0, WELLORD2, REAL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
WELLORD2, RELAT_1, XXREAL_0, XCMPLX_0, RELAT_2, FUNCT_1, PBOOLE,
RELSET_1, FINSET_1, FINSUB_1, SETWISEO, PARTFUN1, FUNCT_2, BINOP_2,
FINSOP_1, FINSEQ_1, FINSEQ_4, FUNCT_3, BINOP_1, XREAL_0, FINSEQ_2,
FUNCT_4, FINSEQ_5, WELLORD1, ORDERS_1, CARD_3, WSIERP_1, FUNCOP_1,
FUNCT_7, NAT_D, INT_1, NAT_1, CLASSES1, VALUED_0, VALUED_1, ORDINAL2,
SETFAM_1, DOMAIN_1, ARROW, FINSEQOP;
constructors WELLORD2, BINOP_1, SETWISEO, CARD_3, FINSEQOP, FINSOP_1,
FINSEQ_4, RFINSEQ, RFUNCT_3, NAT_D, WSIERP_1, FUNCT_7, RECDEF_1, BINOP_2,
CLASSES1, BINARITH, ARROW, TOLER_1, ORDINAL2, RELSET_1, ORDERS_1,
RELAT_2, WELLORD1, DOMAIN_1, SETFAM_1, ORDINAL3, PBOOLE, FINSEQ_5,
REAL_1, FUNCT_4, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
ORDINAL3, FINSET_1, XXREAL_0, XREAL_0, NAT_1, BINOP_2, CARD_1, FINSEQ_1,
FINSEQ_2, CARD_3, PARTFUN1, VALUED_0, VALUED_1, RELSET_1, FUNCT_2,
SETFAM_1, FINSUB_1, INT_1, PBOOLE;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, CARD_3, RELAT_2, WELLORD2, RELAT_1, VALUED_0,
FUNCOP_1, SETFAM_1, FUNCT_1;
equalities PBOOLE, BINOP_1, FINSEQ_2, FUNCOP_1, WELLORD1, ORDINAL1;
expansions TARSKI, XBOOLE_0, CARD_3, RELAT_2, PBOOLE, RELAT_1, BINOP_1,
VALUED_0, WELLORD1, FUNCT_1;
theorems FUNCT_1, FINSET_1, FINSEQ_3, FINSEQ_4, ZFMISC_1, FINSEQ_1, FUNCT_2,
FUNCOP_1, TARSKI, FUNCT_7, BINOP_1, RELAT_1, FINSEQ_2, CARD_3, RFINSEQ,
RELSET_1, CARD_1, ORDINAL1, RVSUM_1, FINSEQ_5, NAT_1, PBOOLE, NAT_2,
SUBSET_1, ORDERS_1, WELLSET1, RELAT_2, ORDINAL3, FINSEQ_6, SETWISEO,
SETWOP_2, CARD_2, FUNCT_5, FINSUB_1, PARTFUN2, XBOOLE_0, XBOOLE_1,
PARTFUN1, BINOP_2, XREAL_1, XXREAL_0, VALUED_0, VALUED_1, NAT_D,
SETFAM_1, ARROW, WELLORD2, FINSOP_1, INT_1, XTUPLE_0, FUNCT_4;
schemes SETWISEO, FUNCT_2, FINSEQ_2, FINSEQ_1, PBOOLE, RELSET_1, FINSEQ_4,
ORDINAL1, FUNCT_7, SUBSET_1, XBOOLE_0, BINOP_1, NAT_1, PRE_CIRC,
CLASSES1, INT_1, XFAMILY;
begin :: from LANG1
definition
let D be set;
let p, q be Element of D*;
redefine func p^q -> Element of D*; :: redefines ^ (FINSEQ_1, definition)
coherence
proof
p^q is FinSequence of D;
hence thesis by FINSEQ_1:def 11;
end;
end;
registration
let D be set;
cluster empty for Element of D*;
existence
proof
<*> D is Element of D* by FINSEQ_1:def 11;
hence thesis;
end;
end;
definition
let D be set;
redefine func <*> D -> empty Element of D*; :: redefines <*> (FINSEQ_1, definition)
coherence by FINSEQ_1:def 11;
end;
definition
let D be non empty set;
let d be Element of D;
redefine func <*d*> -> Element of D*; :: redefines <* (FINSEQ_1, definition)
coherence
proof
<*d*> is FinSequence of D;
hence thesis by FINSEQ_1:def 11;
end;
let e be Element of D;
redefine func <*d,e*> -> Element of D*; :: redefines <* (FINSEQ_1, definition)
coherence
proof
<*d,e*> = <*d*>^<*e*> by FINSEQ_1:def 9;
hence thesis by FINSEQ_1:def 11;
end;
end;
begin :: from DTCONSTR
registration
let X be set;
cluster -> FinSequence-like for Element of X*;
coherence;
end;
definition
let D be set, F be FinSequence of D*;
func FlattenSeq F -> Element of D* means
:Def1:
ex g being BinOp of D* st
(for p, q being Element of D* holds g.(p,q) = p^q) & it = g "**" F;
existence
proof
deffunc F(Element of D*,Element of D*) = $1^$2;
consider g being BinOp of D* such that
A1: for a, b being Element of D* holds g.(a,b) = F(a,b) from BINOP_1:sch 4;
take g "**" F, g;
thus thesis by A1;
end;
uniqueness
proof
let it1, it2 be Element of D*;
given g1 being BinOp of D* such that
A2: for p, q being Element of D* holds g1.(p,q) = p^q and
A3: it1 = g1 "**" F;
given g2 being BinOp of D* such that
A4: for p, q being Element of D* holds g2.(p,q) = p^q and
A5: it2 = g2 "**" F;
now
let a, b be Element of D*;
thus g1.(a,b) = a^b by A2
.= g2.(a,b) by A4;
end;
hence thesis by A3,A5,BINOP_1:2;
end;
end;
theorem Th1:
for D being set, d be Element of D* holds FlattenSeq <*d*> = d
proof
let D be set, d be Element of D*;
ex g being BinOp of D* st
(for p, q being Element of D* holds g.(p,q) = p^q) &
FlattenSeq <*d*> = g "**" <* d *> by Def1;
hence thesis by FINSOP_1:11;
end;
:: from SCMFSA_7, 2006.03.14, A.T.
theorem Th2:
for D being set holds FlattenSeq <*>(D*) = <*>D
proof
let D be set;
consider g being BinOp of D* such that
A1: for d1,d2 being Element of D* holds g.(d1,d2) = d1^d2 and
A2: FlattenSeq <*>(D*) = g "**" <*>(D*) by Def1;
A3: {} is Element of D* by FINSEQ_1:49;
reconsider p = {} as Element of D* by FINSEQ_1:49;
now
let a be Element of D*;
thus g.({},a) = {} ^ a by A1,A3
.= a by FINSEQ_1:34;
thus g.(a,{}) = a ^ {} by A1,A3
.= a by FINSEQ_1:34;
end;
then
A4: p is_a_unity_wrt g by BINOP_1:3;
then g "**" <*>(D*) = the_unity_wrt g by FINSOP_1:10,SETWISEO:def 2;
hence thesis by A2,A4,BINOP_1:def 8;
end;
theorem Th3:
for D being set, F,G be FinSequence of D* holds
FlattenSeq (F ^ G) = FlattenSeq F ^ FlattenSeq G
proof
let D be set, F,G be FinSequence of D*;
consider g being BinOp of D* such that
A1: for d1,d2 being Element of D* holds g.(d1,d2) = d1^d2 and
A2: FlattenSeq (F ^ G) = g "**" F ^ G by Def1;
now
let a,b,c be Element of D*;
thus g.(a,g.(b,c)) = a ^ g.(b,c) by A1
.= a ^ (b ^ c) by A1
.= a ^ b ^ c by FINSEQ_1:32
.= g.(a,b) ^ c by A1
.= g.(g.(a,b),c) by A1;
end;
then
A3: g is associative;
A4: {} is Element of D* by FINSEQ_1:49;
reconsider p = {} as Element of D* by FINSEQ_1:49;
now
let a be Element of D*;
thus g.({},a) = {} ^ a by A1,A4
.= a by FINSEQ_1:34;
thus g.(a,{}) = a ^ {} by A1,A4
.= a by FINSEQ_1:34;
end;
then p is_a_unity_wrt g by BINOP_1:3;
hence FlattenSeq (F ^ G) = g.(g "**" F,g "**" G)
by A2,A3,FINSOP_1:5,SETWISEO:def 2
.= (g "**" F) ^ (g "**" G) by A1
.= FlattenSeq F ^ (g "**" G) by A1,Def1
.= FlattenSeq F ^ FlattenSeq G by A1,Def1;
end;
theorem
for D being set, p,q be Element of D* holds FlattenSeq <* p,q *> = p ^ q
proof
let D be set, p,q be Element of D*;
consider g being BinOp of D* such that
A1: for d1,d2 being Element of D* holds g.(d1,d2) = d1^d2 and
A2: FlattenSeq <* p,q *> = g "**" <* p,q *> by Def1;
thus FlattenSeq <* p,q *> = g.(p,q) by A2,FINSOP_1:12
.= p ^ q by A1;
end;
theorem
for D being set, p,q,r be Element of D* holds
FlattenSeq <* p,q,r *> = p ^ q ^ r
proof
let D be set, p,q,r be Element of D*;
consider g being BinOp of D* such that
A1: for d1,d2 being Element of D* holds g.(d1,d2) = d1^d2 and
A2: FlattenSeq <* p,q,r *> = g "**" <* p,q,r *> by Def1;
thus FlattenSeq <* p,q,r *> = g.(g.(p,q),r) by A2,FINSOP_1:14
.= g.(p,q) ^ r by A1
.= p ^ q ^ r by A1;
end;
:: from SCMFSA_7, 2007.07.22, A.T.
theorem
for D being set, F,G be FinSequence of D* holds
F c= G implies FlattenSeq F c= FlattenSeq G
proof
let D be set, F,G be FinSequence of D*;
assume F c= G;
then consider F9 being FinSequence of D* such that
A1: F ^ F9 = G by FINSEQ_4:82;
FlattenSeq F ^ FlattenSeq F9 = FlattenSeq G by A1,Th3;
hence thesis by FINSEQ_6:10;
end;
begin :: from TRIANG_1
reserve A for set, x,y,z for object,
k for Element of NAT;
scheme
Regr1 { n() -> Nat, P[set] }: for k st k <= n() holds P[k]
provided
A1: P[n()] and
A2: for k st k < n() & P[k+1] holds P[k]
proof
reconsider n9=n() as Element of NAT by ORDINAL1:def 12;
defpred X[Nat] means $1 <= n() & not P[$1];
assume not thesis;
then
A3: ex k be Nat st X[k];
A4: for l be Nat st X[l] holds l <= n9;
consider l being Nat such that
A5: X[l] and
A6: for n being Nat st X[n] holds n <= l from NAT_1:sch 6(A4,A3);
A7: l in NAT by ORDINAL1:def 12;
A8: l < n() by A1,A5,XXREAL_0:1;
then l + 1 <= n() by NAT_1:13;
then P[l+1] by A6,XREAL_1:29;
hence contradiction by A2,A5,A8,A7;
end;
registration
let n be Nat;
cluster Seg (n+1) -> non empty;
coherence;
end;
theorem
{}|_2 A = {};
registration
let X be set;
cluster non empty for Subset of Fin X;
existence
proof
{{}} is Subset of Fin X by FINSUB_1:7,ZFMISC_1:31;
hence thesis;
end;
end;
registration
let X be non empty set;
cluster non empty with_non-empty_elements for Subset of Fin X;
existence
proof
set x = the Element of X;
{x} in Fin X by FINSUB_1:def 5;
then reconsider s = {{x}} as Subset of Fin X by SUBSET_1:33;
take s;
thus s is non empty;
assume {} in s;
hence contradiction;
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
proof
the Element of F <> {};
hence thesis;
end;
end;
registration
let X be non empty set;
cluster with_non-empty_element for Subset of Fin X;
existence
proof
set x = the Element of X;
{x} in Fin X by FINSUB_1:def 5;
then reconsider s = {{x}} as Subset of Fin X by SUBSET_1:33;
take s;
thus thesis;
end;
end;
definition
let X be non empty set, R be Order of X, A be Subset of X;
redefine func R|_2 A -> Order of A; :: redefines |_2 (WELLORD1, definition)
coherence
proof
R partially_orders X by ORDERS_1:44;
hence R |_2 A is Order of A by ORDERS_1:35,45;
end;
end;
scheme
SubFinite{D()->set, A()->Subset of D(), P[set]}: P[A()]
provided
A1: A() is finite and
A2: P[{}(D())] and
A3: for x being Element of D(), B being Subset of D() st x in A() & B c=
A() & P[B] holds P[B \/ {x}]
proof
now
defpred X[set] means ex B be set st B=$1 & P[B];
assume A() <> {};
consider G being set such that
A4: for x be set holds x in G iff x in bool A() & X[x] from XFAMILY:
sch 1;
G c= bool A()
by A4;
then reconsider GA=G as Subset-Family of A();
{} c= A();
then GA <> {} by A2,A4;
then consider B be set such that
A5: B in GA and
A6: for X being set st X in GA holds B c= X implies B=X by A1,FINSET_1:6;
A7: ex A st A = B & P[A] by A4,A5;
now
set x = the Element of A() \ B;
assume B <> A();
then not A() c= B by A5;
then
A8: A() \ B <> {} by XBOOLE_1:37;
then not x in B by XBOOLE_0:def 5;
then
A9: B \/ {x} <> B by XBOOLE_1:7,ZFMISC_1:31;
A10: x in A() by A8,XBOOLE_0:def 5;
then {x} c= A() by ZFMISC_1:31;
then
A11: B \/ {x} c= A() by A5,XBOOLE_1:8;
B is Subset of D() by A5,XBOOLE_1:1;
then B \/ {x} in GA by A4,A11,A3,A5,A7,A10;
hence contradiction by A6,A9,XBOOLE_1:7;
end;
hence thesis by A7;
end;
hence thesis by A2;
end;
registration
let X be non empty set, F be with_non-empty_element Subset of Fin X;
cluster finite non empty for Element of F;
existence
proof
consider x be non empty set such that
A1: x in F by SETFAM_1:def 10;
reconsider x1 = x as Element of F by A1;
take x1;
thus thesis;
end;
end;
definition
let X be set, A be finite Subset of X, R be Order of X;
assume
A1: R linearly_orders A;
func SgmX (R,A) -> FinSequence of X means
:Def2:
rng it = A & for n,m be Nat st n in dom it & m in dom it & n < m holds
it/.n <> it/.m & [it/.n,it/.m] in R;
existence
proof
per cases;
suppose
A2: A is empty;
take <*>X;
thus thesis by A2;
end;
suppose
A3: A is non empty;
then reconsider X9 = X as non empty set;
reconsider A1 = A as non empty finite Subset of X9 by A3;
reconsider R9 = R as Order of X9;
deffunc F(set) = $1;
deffunc V(Element of A1) =
{ F(x) where x is Element of A1: x <=_R9,$1 & x <> $1 };
deffunc U(Element of A1) = card V($1) +^ 1;
A4: for x being Element of A1 holds U(x) is Element of NAT
proof let a be Element of A1;
defpred P[Element of A1] means $1 <=_R9,a & $1 <> a;
{ F(x) where x is Element of A1: P[x] } is finite from PRE_CIRC:sch 1;
then reconsider X = { F(x) where x is Element of A1: P[x] }
as finite set;
reconsider n = card X as Element of NAT;
n +^ 1 = n + 1 by CARD_2:36;
hence U(a) is Element of NAT;
end;
consider f being Function of A1,NAT such that
A5: for x being Element of A1 holds f.x = U(x) from FUNCT_2:sch 9(A4);
A6: for x being Element of A1 holds not x in V(x)
proof let a be Element of A1;
assume a in V(a);
then ex x being Element of A1 st x = a & x <=_R9,a & x <> a;
hence thesis;
end;
A7: for x being Element of A1 holds V(x) c= A1 proof let a be Element of A1;
let y be object;
assume y in V(a);
then ex x being Element of A1 st x = y & x <=_R9,a & x <> a;
hence thesis;
end;
rng f c= Seg card A1
proof
let y be object;
assume y in rng f;
then consider x1 being object such that
A8: x1 in dom f and
A9: y = f.x1 by FUNCT_1:def 3;
reconsider y1 = y as Nat by A9;
reconsider x2 = x1 as Element of A1 by A8;
defpred P[Element of A1] means $1 <=_R9,x2 & $1 <> x2;
{ F(x) where x is Element of A1: P[x] } is finite from PRE_CIRC:sch 1;
then reconsider Vx2 = V(x2) as finite set;
Vx2 <> A1 by A6;
then
A10: card Vx2 <> card A1 by A7,CARD_2:102;
(card Vx2) <= card A1 by A7,NAT_1:43;
then (card Vx2) < card A1 by A10,XXREAL_0:1;
then
A11: (card Vx2) + 1 <= card A1 by NAT_1:13;
A12: y = (card Vx2) +^ 1 by A5,A9
.= (card Vx2) + 1 by CARD_2:36;
then (0 qua Nat) + 1 <= y1 by XREAL_1:6;
hence thesis by A11,A12,FINSEQ_1:1;
end;
then reconsider f1 = f as Function of A1,Seg card A1 by FUNCT_2:6;
A13: R |_2 A c= R by XBOOLE_1:17;
A14: R is_connected_in A by A1,ORDERS_1:def 9;
then
A15: R|_2 A is connected by ORDERS_1:75;
A16: field (R9|_2 A1) = A by ORDERS_1:15;
A17: R9 is_transitive_in A by A1,ORDERS_1:def 9;
A18: R9 is_antisymmetric_in A by A1,ORDERS_1:def 9;
for x1,x2 be object st x1 in A1 & x2 in A1 & f.x1 = f.x2 holds x1 = x2
proof
let x1,x2 be object;
assume that
A19: x1 in A1 and
A20: x2 in A1 and
A21: f.x1 = f.x2;
reconsider x29 = x2 as Element of A1 by A20;
reconsider x19 = x1 as Element of A1 by A19;
defpred P[Element of A1] means $1 <=_R9,x19 & $1 <> x19;
{ F(x) where x is Element of A1: P[x] } is finite from PRE_CIRC:sch 1;
then reconsider Vx1 = V(x19) as finite set;
defpred P[Element of A1] means $1 <=_R9,x29 & $1 <> x29;
{ F(x) where x is Element of A1: P[x] } is finite from PRE_CIRC:sch 1;
then reconsider Vx2 = V(x29) as finite set;
A22: for x1,x2 being Element of A1 st x1 <=_R|_2 A, x2 holds V(x1) c= V(x2)
proof let x1,x2 be Element of A1;
assume x1 <=_R|_2 A, x2;
then
A23: [x1,x2] in R|_2 A by ARROW:def 4;
let x be object;
assume x in V(x1);
then consider a being Element of A such that
A24: a =x and
A25: a <=_R9,x1 and
A26: a <> x1;
A27: [a,x1] in R9 by A25,ARROW:def 4;
then [a,x2] in R9 by A23,A13,A17;
then
A28: a <=_R9,x2 by ARROW:def 4;
a <> x2 by A26,A27,A23,A13,A18;
hence x in V(x2) by A24,A28;
end;
f.x19 = (card Vx1) +^ 1 by A5
.= (card Vx1) + 1 by CARD_2:36;
then
A29: (card Vx1) + 1 = (card Vx2) +^ 1 by A5,A21
.= (card Vx2) + 1 by CARD_2:36;
now
per cases;
suppose
x19 = x29;
hence thesis;
end;
suppose
x19 <> x29;
then
A30: [x19,x29] in R|_2 A or [x29,x19] in R|_2 A
by A16,A15,RELAT_2:def 6;
A31: for x1,x2 being Element of A1 st x1<>x2 & x1<=_R|_2 A, x2
holds x1 in V(x2)
proof let x1,x2 be Element of A1 such that
A32: x1<>x2;
assume x1<=_R|_2 A, x2;
then [x1,x2] in R|_2 A by ARROW:def 4;
then x1 <=_R9, x2 by A13,ARROW:def 4;
hence x1 in V(x2) by A32;
end;
A33: now
per cases by A30,ARROW:def 4;
suppose x19 <=_R|_2 A, x29;
hence Vx1 = Vx2 by A29,A22,CARD_2:102;
end;
suppose x29 <=_R|_2 A, x19;
hence Vx1 = Vx2 by A29,A22,CARD_2:102;
end;
end;
now
assume
A34: x19 <> x29;
then
A35: [x19,x29] in R|_2 A or [x29,x19] in R|_2 A
by A16,A15,RELAT_2:def 6;
per cases by A35,ARROW:def 4;
suppose
x19<=_R|_2 A, x29;
hence contradiction by A33,A6,A34,A31;
end;
suppose
x29<=_R|_2 A, x19;
hence contradiction by A33,A6,A34,A31;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then
A36: f1 is one-to-one by FUNCT_2:19;
A37: for x1,x2 be Element of A1 st f.x1 qua Nat < f.x2
holds x1 <=_R9,x2 & x1 <> x2
proof
let x1,x2 be Element of A1;
defpred P[Element of A1] means $1 <=_R9,x1 & $1 <> x1;
{ F(x) where x is Element of A1: P[x] } is finite from PRE_CIRC:sch 1;
then reconsider Vx1 = V(x1) as finite set;
defpred P[Element of A1] means $1 <=_R9,x2 & $1 <> x2;
{ F(x) where x is Element of A1: P[x] } is finite from PRE_CIRC:sch 1;
then reconsider Vx2 = V(x2) as finite set;
assume
A38: f.x1 < f.x2;
A39: f.x1 = (card Vx1) +^ 1 by A5
.= (card Vx1) + 1 by CARD_2:36;
f.x2 = (card Vx2) +^ 1 by A5
.= (card Vx2) + 1 by CARD_2:36;
then
A40: (card Vx1)+1-1 < (card Vx2)+1-1 by A39,A38,XREAL_1:9;
reconsider Cx2 = card Vx2 as Cardinal;
reconsider Cx1 = card Vx1 as Cardinal;
A41: card Segm card Vx2 = card Vx2;
card Segm card Vx1 = card Vx1;
then Vx2 \ Vx1 <> {} by A41,A40,CARD_1:68,NAT_1:41;
then consider a be object such that
A42: a in (Vx2 \ Vx1) by XBOOLE_0:def 1;
A43: not a in Vx1 by A42,XBOOLE_0:def 5;
A44: a in Vx2 by A42;
Vx2 c= A1 by A7;
then reconsider a as Element of A1 by A44;
A45: ex x being Element of A1 st a=x & x <=_R9,x2 & x <> x2 by A44;
then
A46: [a,x2] in R9 by ARROW:def 4;
per cases by A43;
suppose
not a <=_R9, x1;
then
A47: not [a,x1] in R9 by ARROW:def 4;
per cases;
suppose
x1 = a;
hence thesis by A45;
end;
suppose
A48: x1 <> a;
then
A49: [x1,a] in R9 by A14,A47;
then [x1,x2] in R9 by A46,A17;
hence x1 <=_R9,x2 by ARROW:def 4;
assume x1 = x2;
hence contradiction by A48,A49,A46,A18;
end;
end;
suppose
a = x1;
hence thesis by A45;
end;
end;
card Seg card A1 = card A1 by FINSEQ_1:57; then
f1 is onto by A36,FINSEQ_4:63;
then rng f1 = Seg card A1 by FUNCT_2:def 3;
then dom ((f1 qua Function)") = Seg card A1 by A36,FUNCT_1:33;
then reconsider g1 = (f1 qua Function)" as FinSequence by FINSEQ_1:def 2;
A50: dom f1 = A by FUNCT_2:def 1;
then
A51: rng g1 = A by A36,FUNCT_1:33;
then reconsider g = g1 as FinSequence of X by FINSEQ_1:def 4;
take g;
thus rng g = A by A36,A50,FUNCT_1:33;
let n,m be Nat;
assume that
A52: n in dom g and
A53: m in dom g and
A54: n < m;
reconsider gn = g.n as Element of A1 by A51,A52,FUNCT_1:def 3;
n in rng f by A36,A52,FUNCT_1:33;
then
A55: n = f.(gn) by A36,FUNCT_1:35;
reconsider gm = g.m as Element of A1 by A51,A53,FUNCT_1:def 3;
A56: gm = g/.m by A53,PARTFUN1:def 6;
A57: m in rng f by A36,A53,FUNCT_1:33;
then m = f.(gm) by A36,FUNCT_1:35;
then
A58: [gn,gm] in R by A37,A54,A55,ARROW:def 4;
gn = g/.n by A52,PARTFUN1:def 6;
hence thesis by A36,A54,A57,A55,A58,A56,FUNCT_1:35;
end;
end;
uniqueness
proof
let p9,q9 be FinSequence of X;
assume that
A59: rng p9 = A and
A60: for n,m being Nat st n in dom p9 & m in dom p9 & n < m holds p9/.
n <> p9/.m & [p9/.n,p9/.m] in R and
A61: rng q9 = A and
A62: for n,m being Nat st n in dom q9 & m in dom q9 & n < m holds q9/.
n <> q9/.m & [q9/.n,q9/.m] in R;
per cases;
suppose
A63: A is empty;
then p9 is empty by A59;
hence thesis by A61,A63;
end;
suppose
A64: A is non empty;
then reconsider X9 = X as non empty set;
reconsider A9 = A as non empty finite Subset of X9 by A64;
set E = <*>(A9);
defpred X[FinSequence of A9] means ($1 is FinSequence
of A9 & for n,m being Nat st n in dom $1 & m in dom $1 & n <
m holds $1/.n <> $1/.m & [$1/.n,$1/.m] in R) implies for q being FinSequence of
A9 st rng q = rng $1 & for n,m be Nat st n in dom q & m in
dom q & n < m holds q/.n <> q/.m & [q/.n,q/.m] in R holds q=$1;
reconsider p = p9, q = q9 as FinSequence of A9 by A59,A61,FINSEQ_1:def 4;
A65: for p being FinSequence of A9 for x being
Element of A9 st X[p] holds X[p^<*x*> qua FinSequence of A9]
proof
let p be FinSequence of A9, x be Element of A9;
assume
A66: X[p];
assume p^<*x*> is FinSequence of A9;
assume
A67: for n,m be Nat st n in dom (p^<*x*>) & m in dom (p^<*x*>) & n < m
holds (p^<*x*> qua FinSequence of A9)/.n
<> (p^<*x*> qua FinSequence of A9)/.m
& [(p^<*x*> qua FinSequence of A9)/.n,
(p^<*x*> qua FinSequence of A9)/.m] in R;
let q be FinSequence of A9;
assume that
A68: rng q = rng (p^<*x*>) and
A69: for n,m be Nat st n in dom q & m in dom q & n < m holds q/.n
<> q /.m & [q/.n,q/.m] in R;
deffunc V(Nat) = q.$1;
A70: q <> 0 by A68;
then consider n be Nat such that
A71: len q = n+1 by NAT_1:6;
reconsider n as Element of NAT by ORDINAL1:def 12;
ex q9 being FinSequence st len q9 = n & for m be Nat st m in dom
q9 holds q9.m = V(m) from FINSEQ_1:sch 2;
then consider q9 being FinSequence such that
A72: len q9 = n and
A73: for m be Nat st m in dom q9 holds q9.m = q.m;
1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then
A74: 1 in dom <*x*> by FINSEQ_1:def 8;
A75: ex m be Element of A9 st m=x & for l be
Element of A9 st l in rng (p^<*x*>) & l <> x holds [l,m] in R
proof
reconsider m = x as Element of A9;
take m;
thus m=x;
thus for l be Element of A9 st l in rng (p^<*x*>)
& l <> x holds [l,m] in R
proof
let l be Element of A9;
assume that
A76: l in rng (p^<*x*>) and
A77: l <> x;
consider y being object such that
A78: y in dom (p^<*x*>) and
A79: l=(p^<*x*>).y by A76,FUNCT_1:def 3;
A80: l = (p^<*x*> qua FinSequence of A9)/.y by A78,A79,PARTFUN1:def 6;
reconsider k=y as Element of NAT by A78;
A81: k <> len p + 1
proof
assume k = len p + 1;
then (p^<*x*>).k = <*x*>.1 by A74,FINSEQ_1:def 7
.= x;
hence contradiction by A77,A79;
end;
A82: y in Seg len (p^<*x*>) by A78,FINSEQ_1:def 3;
then k <= len (p^<*x*>) by FINSEQ_1:1;
then k <= len p + len <*x*> by FINSEQ_1:22;
then k <= len p + 1 by FINSEQ_1:39;
then k < len p + 1 by A81,XXREAL_0:1;
then k < len p + len <*x*> by FINSEQ_1:39;
then
A83: k < len(p^<*x*>) by FINSEQ_1:22;
1 <= k by A82,FINSEQ_1:1;
then 1 - len(p^<*x*>) < k - k by A83,XREAL_1:15;
then 1 < len(p^<*x*>) by XREAL_1:48;
then len(p^<*x*>) in Seg len(p^<*x*>) by FINSEQ_1:1;
then
A84: len(p^<*x*>) in dom (p^<*x*>) by FINSEQ_1:def 3;
m = (p^<*x*>).(len p + 1) by FINSEQ_1:42
.= (p^<*x*>).(len p + len <*x*>) by FINSEQ_1:39
.= (p^<*x*>).(len(p^<*x*>)) by FINSEQ_1:22;
then m = (p^<*x*> qua FinSequence of A9)/.(len(p^<*x*>))
by A84,PARTFUN1:def 6;
hence thesis by A67,A78,A80,A83,A84;
end;
end;
A85: for m be Nat st m in dom <*x*> holds q.(len q9 + m) = <*x*>.m
proof
let m be Nat;
assume m in dom <*x*>;
then
A86: m in {1} by FINSEQ_1:2,def 8;
A87: q.(len q9 + m) = x
proof
consider d1 being Element of A9 such that
A88: d1=x and
A89: for l being Element of A9 st l in rng
(p^<*x*>) & l<>x holds [l,d1] in R by A75;
reconsider d = d1 as Element of A9;
len q in Seg len q by A70,FINSEQ_1:3;
then
A90: len q in dom q by FINSEQ_1:def 3;
then q.len q in rng q by FUNCT_1:def 3;
then reconsider
k = q.len q as Element of A9;
A91: k = q/.len q by A90,PARTFUN1:def 6;
A92: field R = X by ORDERS_1:12;
assume q.(len q9 + m) <> x;
then
A93: q.len q <> x by A71,A72,A86,TARSKI:def 1;
x in {x} by TARSKI:def 1;
then x in rng <*x*> by FINSEQ_1:38;
then x in rng p \/ rng <*x*> by XBOOLE_0:def 3;
then x in rng q by A68,FINSEQ_1:31;
then consider y being object such that
A94: y in dom q and
A95: x=q.y by FUNCT_1:def 3;
A96: y in Seg len q by A94,FINSEQ_1:def 3;
reconsider y as Element of NAT by A94;
y <= len q by A96,FINSEQ_1:1;
then
A97: y < len q by A93,A95,XXREAL_0:1;
q.len q in rng (p^<*x*>) by A68,A90,FUNCT_1:def 3;
then
A98: [k,d] in R by A93,A89;
A99: d = q/.y by A88,A94,A95,PARTFUN1:def 6;
then
A100: [d,k] in R by A69,A94,A90,A97,A91;
k <> d by A69,A94,A90,A97,A91,A99;
hence contradiction by A98,A100,A92,RELAT_2:def 4,def 12;
end;
m=1 by A86,TARSKI:def 1;
hence thesis by A87;
end;
now
let x be object;
A101: n <= n + 1 by NAT_1:11;
assume x in rng q9;
then consider y being object such that
A102: y in dom q9 and
A103: x=q9.y by FUNCT_1:def 3;
A104: y in Seg len q9 by A102,FINSEQ_1:def 3;
reconsider y as Element of NAT by A102;
y <= n by A72,A104,FINSEQ_1:1;
then
A105: y <= n+1 by A101,XXREAL_0:2;
1 <= y by A104,FINSEQ_1:1;
then y in dom q by A71,A105,FINSEQ_3:25;
then q.y in rng q by FUNCT_1:def 3;
then q.y in A9;
hence x in A9 by A73,A102,A103;
end;
then reconsider f=q9 as FinSequence of A9
by FINSEQ_1:def 4,TARSKI:def 3;
dom q = Seg (n+1) by A71,FINSEQ_1:def 3
.= Seg (len q9 + len <*x*>) by A72,FINSEQ_1:39;
then
A106: q9^<*x*> = q by A73,A85,FINSEQ_1:def 7;
A107: not x in rng p
proof
len p + 1 = len p + len <*x*> by FINSEQ_1:39
.= len (p^<*x*>) by FINSEQ_1:22;
then (len p + 1) in Seg (len(p^<*x*>)) by FINSEQ_1:4;
then
A108: (len p + 1) in dom (p^<*x*>) by FINSEQ_1:def 3;
assume x in rng p;
then consider y being object such that
A109: y in dom p and
A110: x=p.y by FUNCT_1:def 3;
A111: y in Seg len p by A109,FINSEQ_1:def 3;
A112: dom p c= dom (p^<*x*>) by FINSEQ_1:26;
reconsider y as Element of NAT by A109;
x = (p^<*x*> qua FinSequence of A9).y by A109,A110,FINSEQ_1:def 7;
then
A113: x = (p^<*x*> qua FinSequence of A9)/.y by A109,A112,PARTFUN1:def 6;
y <= len p by A111,FINSEQ_1:1;
then
A114: y < len p + 1 by NAT_1:13;
x = (p^<*x*> qua FinSequence of A9).(len p + 1 ) by FINSEQ_1:42;
then (p^<*x*> qua FinSequence of A9)/.y
= (p^<*x*> qua FinSequence of A9)/.(len p + 1 ) by A108,A113,
PARTFUN1:def 6;
hence contradiction by A67,A109,A108,A112,A114;
end;
A115: for z being object holds z in rng p \/ {x} \ {x} iff z in rng p
proof
let z be object;
thus z in rng p \/ {x} \ {x} implies z in rng p
proof
assume
A116: z in rng p \/ {x} \ {x};
then
A117: not z in {x} by XBOOLE_0:def 5;
z in rng p \/ {x} by A116,XBOOLE_0:def 5;
hence thesis by A117,XBOOLE_0:def 3;
end;
assume
A118: z in rng p;
then
A119: z in rng p \/ {x} by XBOOLE_0:def 3;
not z in {x} by A107,A118,TARSKI:def 1;
hence thesis by A119,XBOOLE_0:def 5;
end;
rng (p^<*x*>) = rng p \/ rng <*x*> by FINSEQ_1:31
.= rng p \/ {x} by FINSEQ_1:39;
then
A120: rng p = rng (p^<*x*>) \ {x} by A115,TARSKI:2;
A121: rng f = rng p & for l,m be Nat st l in dom f & m in dom f & l <
m holds f/.l <> f/.m & [f/.l,f/.m] in R
proof
A122: not x in rng f
proof
len f + 1 = len f + len <*x*> by FINSEQ_1:39
.= len (f^<*x*>) by FINSEQ_1:22;
then (len f + 1) in Seg (len(f^<*x*>)) by FINSEQ_1:4;
then
A123: (len f + 1) in dom (f^<*x*>) by FINSEQ_1:def 3;
assume x in rng f;
then consider y being object such that
A124: y in dom f and
A125: x=f.y by FUNCT_1:def 3;
A126: y in Seg len f by A124,FINSEQ_1:def 3;
A127: dom f c= dom (f^<*x*>) by FINSEQ_1:26;
reconsider y as Element of NAT by A124;
x = q.y by A73,A124,A125;
then
A128: x = q/.y by A106,A124,A127,PARTFUN1:def 6;
y <= len f by A126,FINSEQ_1:1;
then
A129: y < len f + 1 by NAT_1:13;
x = q.(len f + 1) by A106,FINSEQ_1:42;
then q/.y = q/.(len f + 1) by A106,A123,A128,PARTFUN1:def 6;
hence contradiction by A69,A106,A124,A123,A127,A129;
end;
A130: for z being object holds z in rng f \/ {x} \ {x} iff z in rng f
proof
let z be object;
hereby
assume
A131: z in rng f \/ {x} \ {x};
then
A132: not z in {x} by XBOOLE_0:def 5;
z in rng f \/ {x} by A131,XBOOLE_0:def 5;
hence z in rng f by A132,XBOOLE_0:def 3;
end;
assume
A133: z in rng f;
then
A134: z in rng f \/ {x} by XBOOLE_0:def 3;
not z in {x} by A122,A133,TARSKI:def 1;
hence thesis by A134,XBOOLE_0:def 5;
end;
rng (f^<*x*>) = rng f \/ rng <*x*> by FINSEQ_1:31
.= rng f \/ {x} by FINSEQ_1:39;
hence rng f = rng p by A68,A106,A120,A130,TARSKI:2;
let l,m be Nat;
assume that
A135: l in dom f and
A136: m in dom f and
A137: l < m;
A138: f.m = f/.m by A136,PARTFUN1:def 6;
A139: dom f c= dom q by A106,FINSEQ_1:26;
then q.m = q/.m by A136,PARTFUN1:def 6;
then
A140: f/.m = q/.m by A73,A136,A138;
A141: f.l = f/.l by A135,PARTFUN1:def 6;
q.l = q/.l by A139,A135,PARTFUN1:def 6;
then f/.l = q/.l by A73,A135,A141;
hence thesis by A69,A139,A135,A136,A137,A140;
end;
p is FinSequence of A9 & for l,m be Nat st l
in dom p & m in dom p & l < m holds p/.l <> p/.m & [p/.l,p/.m] in R
proof
thus p is FinSequence of A9;
let l,m be Nat;
assume that
A142: l in dom p and
A143: m in dom p and
A144: l < m;
A145: dom p c= dom (p^<*x*>) by FINSEQ_1:26;
p.m = (p^<*x*>).m by A143,FINSEQ_1:def 7;
then p.m = (p^<*x*> qua FinSequence of A9)/.m
by A143,A145,PARTFUN1:def 6;
then
A146: p/.m = (p^<*x*> qua FinSequence of A9)/.m by A143,PARTFUN1:def 6;
p.l = (p^<*x*>).l by A142,FINSEQ_1:def 7;
then p.l = (p^<*x*> qua FinSequence of A9)/.l
by A142,A145,PARTFUN1:def 6;
then p/.l = (p^<*x*> qua FinSequence of A9)/.l
by A142,PARTFUN1:def 6;
hence thesis by A67,A142,A143,A144,A145,A146;
end;
hence thesis by A66,A106,A121;
end;
A147: now
let n,m be Nat;
assume that
A148: n in dom p and
A149: m in dom p and
A150: n < m;
A151: p/.m = p.m by A149,PARTFUN1:def 6
.= p9/.m by A149,PARTFUN1:def 6;
p/.n = p.n by A148,PARTFUN1:def 6
.= p9/.n by A148,PARTFUN1:def 6;
hence p/.n <> p/.m & [p/.n,p/.m] in R by A60,A148,A149,A150,A151;
end;
A152: now
let n,m be Nat;
assume that
A153: n in dom q and
A154: m in dom q and
A155: n < m;
A156: q/.m = q.m by A154,PARTFUN1:def 6
.= q9/.m by A154,PARTFUN1:def 6;
q/.n = q.n by A153,PARTFUN1:def 6
.= q9/.n by A153,PARTFUN1:def 6;
hence q/.n <> q/.m & [q/.n,q/.m] in R by A62,A153,A154,A155,A156;
end;
A157: X[E];
for p be FinSequence of A9 holds X [p] from
FINSEQ_2:sch 2(A157,A65);
hence thesis by A59,A61,A147,A152;
end;
end;
end;
::$CT
theorem
for X be set, A be finite Subset of X, R be Order of X, f be
FinSequence of X st rng f = A & for n,m be 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
let X be set, A be finite Subset of X, R be Order of X, f be FinSequence of
X;
assume that
A1: rng f = A and
A2: for n,m be Nat st n in dom f & m in dom f & n < m holds f/.n <> f/.m
& [f/.n,f/.m] in R;
now
let a,b be object;
assume that
A3: a in A and
A4: b in A and
A5: a <> b;
consider n being Nat such that
A6: n in dom f and
A7: f.n = a by A1,A3,FINSEQ_2:10;
consider m being Nat such that
A8: m in dom f and
A9: f.m = b by A1,A4,FINSEQ_2:10;
A10: f/.m = f.m by A8,PARTFUN1:def 6;
A11: f/.n = f.n by A6,PARTFUN1:def 6;
now
assume that
A12: not [a,b] in R and
A13: not [b,a] in R;
per cases;
suppose
n = m;
hence contradiction by A5,A7,A9;
end;
suppose
A14: n <> m;
now
per cases by A14,XXREAL_0:1;
suppose
n > m;
hence contradiction by A2,A6,A7,A8,A9,A11,A10,A13;
end;
suppose
m > n;
hence contradiction by A2,A6,A7,A8,A9,A11,A10,A12;
end;
end;
hence contradiction;
end;
end;
hence [a,b] in R or [b,a] in R;
end;
then
A15: R is_connected_in A;
A16: field R = X by ORDERS_1:12;
then
A17: R is_antisymmetric_in A by ORDERS_1:9,RELAT_2:def 12;
R is_transitive_in X by A16,RELAT_2:def 16;
then
A18: R is_transitive_in A;
R is_reflexive_in X by A16,RELAT_2:def 9;
then R is_reflexive_in A;
then R linearly_orders A by A17,A18,A15,ORDERS_1:def 9;
hence thesis by A1,A2,Def2;
end;
registration
let X be set, F be non empty Subset of Fin X;
cluster -> finite for Element of F;
coherence;
end;
definition
let X be set, F be non empty Subset of Fin X;
redefine mode Element of F -> Subset of X; :: redefines Element (SUBSET_1, definition)
coherence
proof
let a be Element of F;
thus thesis by FINSUB_1:16;
end;
end;
theorem Th9:
for X being set, A being finite Subset of X, R being Order of X
st R linearly_orders A holds SgmX(R,A) is one-to-one
proof
let X be set, A be finite Subset of X, R be Order of X;
set f = (SgmX(R, A));
assume
A1: R linearly_orders A;
then rng f = A by Def2;
then reconsider f as FinSequence of A by FINSEQ_1:def 4;
f is one-to-one
proof
let k,l be object;
assume that
A2: k in dom f and
A3: l in dom f and
A4: f.k = f.l;
reconsider k,l as Element of NAT by A2,A3;
reconsider fk = f.k as Element of A by A2,FINSEQ_2:11;
reconsider fl = f.l as Element of A by A3,FINSEQ_2:11;
A5: fl = f/.l by A3,PARTFUN1:def 6;
A6: fk = f/.k by A2,PARTFUN1:def 6;
now
A7: f/.l = f.l by A3,PARTFUN1:def 6
.= SgmX(R,A)/.l by A3,PARTFUN1:def 6;
A8: f/.k = f.k by A2,PARTFUN1:def 6
.= SgmX(R,A)/.k by A2,PARTFUN1:def 6;
assume
A9: k <> l;
per cases by A9,XXREAL_0:1;
suppose
k < l;
hence contradiction by A1,A2,A3,A4,A6,A5,A8,A7,Def2;
end;
suppose
l < k;
hence contradiction by A1,A2,A3,A4,A6,A5,A8,A7,Def2;
end;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th10:
for X being set, A being finite Subset of X, R being Order of X
st R linearly_orders A holds len(SgmX(R, A)) = card A
proof
let X be set, A be finite Subset of X, R be Order of X;
set f = SgmX(R, A);
A1: dom f = Seg(len f) by FINSEQ_1:def 3;
A2: card Seg(len f) = card (len f) by CARD_1:5,FINSEQ_1:54;
assume
A3: R linearly_orders A;
then
A4: f is one-to-one by Th9;
rng f = A by A3,Def2;
hence thesis by A2,A1,A4,CARD_1:5,WELLORD2:def 4;
end;
begin :: from MATRLIN
reserve n for Nat,
x for object;
theorem Th11:
for M be FinSequence st len M = n+1 holds len Del(M,n+1) = n
proof
let M be FinSequence;
assume
A1: len M = n+1;
then n+1 in Seg len M by FINSEQ_1:4;
then n+1 in dom M by FINSEQ_1:def 3;
hence thesis by A1,FINSEQ_3:109;
end;
theorem
for M being FinSequence st M <> {} holds
M = Del(M,len M) ^ <*M.(len M)*>
proof
let M be FinSequence;
assume M <> {};
then consider q be FinSequence,x being object such that
A1: M = q ^ <*x*> by FINSEQ_1:46;
A2: len M = len q + len <*x*> by A1,FINSEQ_1:22
.= len q + 1 by FINSEQ_1:39;
then
A3: len Del(M,len M) = len q by Th11;
A4: dom q = Seg len q by FINSEQ_1:def 3;
A5: now
let i be Nat;
assume
A6: i in dom q;
then i<=len q by A4,FINSEQ_1:1;
then i in NAT & i<len M by A2,NAT_1:13,ORDINAL1:def 12;
hence Del(M,len M).i = M.i by FINSEQ_3:110
.= q.i by A1,A6,FINSEQ_1:def 7;
end;
M.(len M) = x by A1,A2,FINSEQ_1:42;
hence thesis by A1,A3,A5,FINSEQ_2:9;
end;
definition
let IT be Function;
attr IT is FinSequence-yielding means
:Def3:
for x being object st x in dom IT holds IT.x is FinSequence;
end;
registration
cluster FinSequence-yielding for Function;
existence
proof
set f = the FinSequence, I = the set;
take F = I --> f;
let x;
assume x in dom F;
hence thesis by FUNCOP_1:7;
end;
end;
registration
let D be set;
cluster -> FinSequence-yielding for FinSequence of D*;
coherence;
end;
registration
cluster FinSequence-yielding -> Function-yielding for Function;
coherence
proof
let f be Function;
assume
A1: f is FinSequence-yielding;
let x be object;
thus thesis by A1;
end;
end;
registration
let F be FinSequence-yielding Function, x be object;
cluster F.x -> FinSequence-like;
coherence
proof
per cases;
suppose not x in dom F;
hence thesis by FUNCT_1:def 2;
end;
suppose x in dom F;
hence thesis by Def3;
end;
end;
end;
definition
let F,G be FinSequence-yielding Function;
func F^^G -> Function means
:Def4:
dom it = dom F /\ dom G &
for i being object st i in dom it holds it.i = (F.i)^(G.i);
existence
proof
defpred P[object,object] means
for f be FinSequence, g be FinSequence st f = F.
$1 & g = G.$1 holds $2 = f^g;
A1: for i be object st i in dom F /\ dom G
ex u be object st P[i,u]
proof
let i be object;
assume i in dom F /\ dom G;
reconsider f = F.i, g = G.i as FinSequence;
take f^g;
thus thesis;
end;
consider H being Function such that
A2: dom H = dom F /\ dom G &
for i be object st i in dom F /\ dom G holds
P[i,H.i] from CLASSES1:sch 1(A1);
take H;
thus thesis by A2;
end;
uniqueness
proof
let F1,F2 be Function such that
A3: dom F1 = dom F /\ dom G and
A4: for i be object st i in dom F1 holds F1.i = (F.i)^(G.i) and
A5: dom F2 = dom F /\ dom G and
A6: for i be object st i in dom F2 holds F2.i = (F.i)^(G.i);
now
let x be object;
assume
A7: x in dom F1;
reconsider f = F.x, g = G.x as FinSequence;
thus F1.x = f^g by A4,A7
.= F2.x by A3,A5,A6,A7;
end;
hence thesis by A3,A5;
end;
end;
registration
let F,G be FinSequence-yielding Function;
cluster F^^G -> FinSequence-yielding;
coherence
proof
let x be object;
assume x in dom(F^^G);
then (F^^G).x = (F.x)^(G.x) by Def4;
hence thesis;
end;
end;
begin :: HEYTING2
reserve V, C for set;
theorem
for V, C being non empty set ex f be Element of PFuncs (V, C) st f <> {}
proof
let V, C be non empty set;
consider a be object such that
A1: a in V by XBOOLE_0:def 1;
consider b be object such that
A2: b in C by XBOOLE_0:def 1;
set f = {[a,b]};
{a} c= V by A1,ZFMISC_1:31;
then
A3: dom f c= V by RELAT_1:9;
{b} c= C by A2,ZFMISC_1:31;
then rng f c= C by RELAT_1:9;
then reconsider f as Element of PFuncs (V, C) by A3,PARTFUN1:def 3;
f <> {};
hence thesis;
end;
theorem
for f being Element of PFuncs (V, C), g being set st g c= f holds
g in PFuncs (V, C)
proof
let f be Element of PFuncs (V, C), g be set;
consider f1 be Function such that
A1: f1 = f and
A2: dom f1 c= V and
A3: rng f1 c= C by PARTFUN1:def 3;
assume
A4: g c= f;
then reconsider g9 = g as Function;
rng g9 c= rng f1 by A4,A1,RELAT_1:11;
then
A5: rng g9 c= C by A3;
dom g9 c= dom f1 by A4,A1,RELAT_1:11;
then dom g9 c= V by A2;
hence thesis by A5,PARTFUN1:def 3;
end;
theorem Th15:
PFuncs(V,C) c= bool [:V,C:]
proof
let x be object;
assume x in PFuncs(V,C);
then consider f being Function such that
A1: x = f and
A2: dom f c= V and
A3: rng f c= C by PARTFUN1:def 3;
A4: f c= [: dom f, rng f:] by RELAT_1:7;
[:dom f, rng f:] c= [:V,C:] by A2,A3,ZFMISC_1:96;
then f c= [:V,C:] by A4;
hence thesis by A1;
end;
theorem Th16:
V is finite & C is finite implies PFuncs (V, C) is finite
proof
assume that
A1: V is finite and
A2: C is finite;
PFuncs(V,C) c= bool [:V,C:] by Th15;
hence thesis by A1,A2;
end;
registration
cluster functional finite non empty for set;
existence
proof
set A = the finite non empty set;
take P = PFuncs(A,A);
thus P is functional;
thus P is finite by Th16;
thus thesis;
end;
end;
begin :: POLYNOM1
theorem Th17:
for X being set, R being Relation st field R c= X holds R is Relation of X
proof
let X be set, R be Relation;
assume
A1: field R c= X;
R c= [:X,X:]
proof
let x,y be object;
assume [x,y] in R;
then x in field R & y in field R by RELAT_1:15;
hence thesis by A1,ZFMISC_1:def 2;
end;
hence thesis;
end;
registration
let X be set, f be ManySortedSet of X, x, y be object;
cluster f+*(x,y) -> X-defined;
coherence
proof
dom (f+*(x,y)) = dom f by FUNCT_7:30
.= X by PARTFUN1:def 2;
hence thesis;
end;
end;
registration
let X be set, f be ManySortedSet of X, x, y be object;
cluster f+*(x,y) -> total for X-defined Function;
coherence
proof
dom (f+*(x,y)) = dom f by FUNCT_7:30
.= X by PARTFUN1:def 2;
hence thesis by PARTFUN1:def 2;
end;
end;
theorem Th18:
for f being one-to-one Function holds card f = card rng f
proof
let f be one-to-one Function;
A1: rng f = dom(f") & dom f = rng(f") by FUNCT_1:33;
card rng f c= card dom f & card rng (f") c= card dom (f") by CARD_2:61;
then card rng f = card dom f by A1;
hence thesis by CARD_1:62;
end;
definition
let A be set;
let X be set, D be non empty FinSequenceSet of A,
p be PartFunc of X,D, i be set;
redefine func p/.i -> Element of D; :: redefines /. (PARTFUN1, definition)
coherence;
end;
registration
let X be set;
cluster being_linear-order well-ordering for Order of X;
existence
proof
consider R being Relation such that
A1: R is well-ordering and
A2: field R = X by WELLSET1:6;
reconsider R as Relation of X by A2,Th17;
R is reflexive by A1;
then R is_reflexive_in X by A2;
then dom R = X by ORDERS_1:13;
then reconsider R as Order of X by A1,PARTFUN1:def 2;
take R;
thus thesis by A1,ORDERS_1:def 6;
end;
end;
theorem Th19:
for X being non empty set, A being non empty finite Subset of X,
R being Order of X, 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
let X be non empty set, A be non empty finite Subset of X, R be Order of X,
x be Element of X;
assume that
A1: x in A and
A2: R linearly_orders A and
A3: for y being Element of X st y in A holds [x,y] in R and
A4: SgmX (R,A)/.1 <> x;
A5: A = rng SgmX (R,A) by A2,Def2;
then consider i being Element of NAT such that
A6: i in dom SgmX (R,A) and
A7: SgmX (R,A)/.i = x by A1,PARTFUN2:2;
SgmX (R,A) is non empty by A2,Def2,RELAT_1:38;
then
A8: 1 in dom SgmX (R,A) by FINSEQ_5:6;
then
A9: [x, SgmX (R,A)/.1] in R by A3,A5,PARTFUN2:2;
A10: field R = X by ORDERS_1:12;
1 <= i by A6,FINSEQ_3:25;
then 1 < i by A4,A7,XXREAL_0:1;
then [SgmX (R,A)/.1, x] in R by A2,A6,A7,A8,Def2;
hence contradiction by A4,A9,A10,RELAT_2:def 4,def 12;
end;
theorem Th20:
for X being non empty set, A being non empty finite Subset of X,
R being Order of X, 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
let X be non empty set, A be non empty finite Subset of X, R be Order of X,
x be Element of X;
assume that
A1: x in A and
A2: R linearly_orders A and
A3: for y being Element of X st y in A holds [y,x] in R and
A4: SgmX (R,A)/.len SgmX (R,A) <> x;
set L = len SgmX (R,A);
A5: A = rng SgmX (R,A) by A2,Def2;
then consider i being Element of NAT such that
A6: i in dom SgmX (R,A) and
A7: SgmX (R,A)/.i = x by A1,PARTFUN2:2;
SgmX (R,A) is non empty by A2,Def2,RELAT_1:38;
then
A8: L in dom SgmX (R,A) by FINSEQ_5:6;
then
A9: [SgmX (R,A)/.L,x] in R by A3,A5,PARTFUN2:2;
A10: field R = X by ORDERS_1:12;
i <= L by A6,FINSEQ_3:25;
then i < L by A4,A7,XXREAL_0:1;
then [x, SgmX (R,A)/.L] in R by A2,A6,A7,A8,Def2;
hence contradiction by A4,A9,A10,RELAT_2:def 4,def 12;
end;
registration
let X be non empty set, A be non empty finite Subset of X;
let R be being_linear-order Order of X;
cluster SgmX(R, A) -> non empty one-to-one;
coherence
proof
field R = X by ORDERS_1:15;
then R linearly_orders A by ORDERS_1:37,38;
hence thesis by Th9,Def2,RELAT_1:38;
end;
end;
registration
cluster empty -> FinSequence-yielding for Function;
coherence;
end;
registration
let F, G be FinSequence-yielding FinSequence;
cluster F^^G -> FinSequence-like;
coherence
proof
dom (F^^G) = dom F /\ dom G by Def4
.= Seg len F /\ dom G by FINSEQ_1:def 3
.= Seg len F /\ Seg len G by FINSEQ_1:def 3
.= Seg min(len F, len G) by FINSEQ_2:2;
hence thesis by FINSEQ_1:def 2;
end;
end;
registration
let i be Nat, f be FinSequence;
cluster i |-> f -> FinSequence-yielding;
coherence by FUNCOP_1:7;
end;
registration
let F be FinSequence;
cluster Card F -> FinSequence-like;
coherence
proof
dom Card F = dom F by CARD_3:def 2
.= Seg len F by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 2;
end;
end;
registration
cluster Cardinal-yielding for FinSequence;
existence
proof
take {};
thus thesis;
end;
end;
theorem Th21:
for f being Function holds f is Cardinal-yielding iff
for y being set st y in rng f holds y is Cardinal
proof
let f be Function;
hereby
assume
A1: f is Cardinal-yielding;
let y be set;
assume y in rng f;
then ex x being object st x in dom f & y = f.x by FUNCT_1:def 3;
hence y is Cardinal by A1;
end;
assume
A2: for y being set st y in rng f holds y is Cardinal;
let x be object;
assume x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis by A2;
end;
registration
let F, G be Cardinal-yielding FinSequence;
cluster F^G -> Cardinal-yielding;
coherence
proof
A1: rng (F^G) = rng F \/ rng G by FINSEQ_1:31;
now
let y be set;
assume y in rng (F^G);
then y in rng F or y in rng G by A1,XBOOLE_0:def 3;
hence y is Cardinal by Th21;
end;
hence thesis by Th21;
end;
end;
registration
cluster -> Cardinal-yielding for FinSequence of NAT;
coherence;
end;
registration
cluster Cardinal-yielding for FinSequence of NAT;
existence
proof
take <*>NAT;
thus thesis;
end;
end;
definition
let D be set;
let F be FinSequence of D*;
redefine func Card F -> Cardinal-yielding FinSequence of NAT; :: redefines Card (CARD_3, definition)
coherence
proof
rng Card F c= NAT
proof
let y be object;
assume y in rng Card F;
then consider x being object such that
A1: x in dom Card F and
A2: y = (Card F).x by FUNCT_1:def 3;
reconsider Fx = F.x as finite set;
x in dom F by A1,CARD_3:def 2;
then y = card Fx by A2,CARD_3:def 2;
hence thesis;
end;
hence thesis by FINSEQ_1:def 4;
end;
end;
registration
let F be FinSequence of NAT, i be Element of NAT;
cluster F|i -> Cardinal-yielding;
coherence;
end;
theorem Th22:
for F being Function, X being set holds Card (F|X) = (Card F)|X
proof
let F be Function, X be set;
A1: dom ((Card F)|X) = dom (Card F) /\ X by RELAT_1:61
.= dom F /\ X by CARD_3:def 2
.= dom (F|X) by RELAT_1:61;
now
let x be object;
A2: dom (F|X) c= dom F by RELAT_1:60;
assume
A3: x in dom (F|X);
hence ((Card F)|X).x = (Card F).x by A1,FUNCT_1:47
.= card (F.x) by A3,A2,CARD_3:def 2
.= card ((F|X).x) by A3,FUNCT_1:47;
end;
hence thesis by A1,CARD_3:def 2;
end;
registration
let F be empty Function;
cluster Card F -> empty;
coherence
proof
dom F is empty;
then dom Card F is empty by CARD_3:def 2;
hence thesis;
end;
end;
theorem Th23:
for p being set holds Card <*p*> = <*card p*>
proof
let p be set;
set Cp = <*card p*>;
A1: dom Cp = {1} by FINSEQ_1:2,38;
now
let x be object;
assume x in dom Cp;
then x = 1 by A1,TARSKI:def 1;
hence Cp.x is Cardinal;
end;
then reconsider Cp as Cardinal-Function by CARD_3:def 1;
A2: dom <*p*> = {1} by FINSEQ_1:2,38;
now
let x be object;
assume x in dom <*p*>;
then
A3: x = 1 by A2,TARSKI:def 1;
hence <*card p*>.x = card p
.= card (<*p*>.x) by A3;
end;
then Card <*p*> = Cp by A1,A2,CARD_3:def 2;
hence thesis;
end;
theorem Th24:
for F, G be FinSequence holds Card (F^G) = Card F ^ Card G
proof
let F, G be FinSequence;
A1: dom Card G = dom G by CARD_3:def 2;
then
A2: len Card G = len G by FINSEQ_3:29;
A3: dom Card F = dom F by CARD_3:def 2;
then
A4: len Card F = len F by FINSEQ_3:29;
A5: now
let x be object;
assume
A6: x in dom (F^G);
then reconsider k = x as Element of NAT;
x in Seg (len F + len G) by A6,FINSEQ_1:def 7;
then
A7: 1 <= k by FINSEQ_1:1;
per cases;
suppose
k <= len F;
then
A8: k in dom F by A7,FINSEQ_3:25;
hence (Card F ^ Card G).x = (Card F).k by A3,FINSEQ_1:def 7
.= card (F.k) by A8,CARD_3:def 2
.= card ((F^G).x) by A8,FINSEQ_1:def 7;
end;
suppose
len F < k;
then not k in dom F by FINSEQ_3:25;
then consider n being Nat such that
A9: n in dom G and
A10: k = len F + n by A6,FINSEQ_1:25;
thus (Card F ^ Card G).x = (Card G).n by A1,A4,A9,A10,FINSEQ_1:def 7
.= card (G.n) by A9,CARD_3:def 2
.= card ((F^G).x) by A9,A10,FINSEQ_1:def 7;
end;
end;
dom (Card F ^ Card G) = Seg (len Card F + len Card G) by FINSEQ_1:def 7
.= dom (F ^ G) by A4,A2,FINSEQ_1:def 7;
hence thesis by A5,CARD_3:def 2;
end;
registration
let X be set;
cluster <*>X -> FinSequence-yielding;
coherence;
end;
registration
let f be FinSequence;
cluster <*f*> -> FinSequence-yielding;
coherence
proof
let x be object;
assume x in dom <*f*>;
then x in {1} by FINSEQ_1:2,38;
then x = 1 by TARSKI:def 1;
hence thesis;
end;
end;
theorem Th25:
for f being Function holds f is FinSequence-yielding iff for y
being set st y in rng f holds y is FinSequence
proof
let f be Function;
hereby
assume
A1: f is FinSequence-yielding;
let y be set;
assume y in rng f;
then ex x being object st x in dom f & y = f.x by FUNCT_1:def 3;
hence y is FinSequence by A1;
end;
assume
A2: for y being set st y in rng f holds y is FinSequence;
let x be object;
assume x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis by A2;
end;
registration
let F, G be FinSequence-yielding FinSequence;
cluster F^G -> FinSequence-yielding;
coherence
proof
A1: rng (F^G) = rng F \/ rng G by FINSEQ_1:31;
now
let y be set;
assume y in rng (F^G);
then y in rng F or y in rng G by A1,XBOOLE_0:def 3;
hence y is FinSequence by Th25;
end;
hence thesis by Th25;
end;
end;
registration
let D be set, F be empty FinSequence of D*;
cluster FlattenSeq F -> empty;
coherence
proof
F = <*>(D*);
then FlattenSeq F = <*>D by Th2;
hence thesis;
end;
end;
theorem Th26:
for D being set, F being FinSequence of D* holds len FlattenSeq
F = Sum Card F
proof
let D be set;
defpred P[FinSequence of D*] means len FlattenSeq $1 = Sum Card $1;
A1: now
let F be FinSequence of D*, p be Element of D* such that
A2: P[F];
len FlattenSeq (F^<*p*>) = len (FlattenSeq F ^ FlattenSeq <*p*>) by Th3
.= (Sum Card F) + len FlattenSeq <*p*> by A2,FINSEQ_1:22
.= (Sum Card F) + len p by Th1
.= Sum ((Card F)^<*len p*>) by RVSUM_1:74
.= Sum ((Card F) ^ Card <*p*>) by Th23
.= Sum Card (F^<*p*>) by Th24;
hence P[F^<*p*>];
end;
A3: P[<*>(D*)] by RVSUM_1:72;
thus for F be FinSequence of D* holds P[F] from FINSEQ_2:sch 2(A3, A1);
end;
theorem Th27:
for D, E being set, F being FinSequence of D*, G being
FinSequence of E* st Card F = Card G holds len FlattenSeq F = len FlattenSeq G
proof
let D, E be set, F be FinSequence of D*, G be FinSequence of E*;
assume Card F = Card G;
hence len FlattenSeq F = Sum Card G by Th26
.= len FlattenSeq G by Th26;
end;
theorem Th28:
for D being set, F being FinSequence of D*, k being set st k in
dom FlattenSeq F 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 = (FlattenSeq F).k
proof
let D be set;
set F = <*>(D*);
defpred P[FinSequence of D*] means for k being set st k in dom FlattenSeq $1
ex i,j be Nat st i in dom $1 & j in dom ($1.i) & k = (Sum Card ($1|(
i-'1))) + j & ($1.i).j = (FlattenSeq $1).k;
A1: for F be FinSequence of D*, p be Element of D* st P[F] holds P[F^<*p*>]
proof
let F be FinSequence of D*, p be Element of D*;
assume
A2: P[F];
let k be set;
A3: FlattenSeq (F^<*p*>) = FlattenSeq F ^ FlattenSeq <*p*> by Th3
.= FlattenSeq F ^ p by Th1;
A4: Sum Card F = len FlattenSeq F & (F^<*p*>)|len F = F by Th26,FINSEQ_5:23;
assume
A5: k in dom FlattenSeq (F^<*p*>);
then reconsider m = k as Element of NAT;
per cases;
suppose
A6: not k in dom FlattenSeq F;
take i = len F + 1;
take j = m-'Sum Card ((F^<*p*>)|(i-'1));
A7: 1 <= len F +1 by NAT_1:11;
len (F^<*p*>) = len F + len <*p*> by FINSEQ_1:22
.= len F +1 by FINSEQ_1:39;
hence i in dom (F^<*p*>) by A7,FINSEQ_3:25;
A8: (Sum Card ((F^<*p*>)|(i-'1))) = len FlattenSeq F by A4,NAT_D:34;
m <= len (FlattenSeq F ^ p) by A5,A3,FINSEQ_3:25;
then m <= len FlattenSeq F + len p by FINSEQ_1:22;
then
A9: j <= len p by A8,NAT_D:53;
1 in dom <*p*> by FINSEQ_5:6;
then
A10: (F^<*p*>).i = <*p*>.1 by FINSEQ_1:def 7
.= p;
1 <= m by A5,FINSEQ_3:25;
then
A11: len FlattenSeq F < m by A6,FINSEQ_3:25;
then len FlattenSeq F +1 <= m by NAT_1:13;
hence
A12: j in dom ((F^<*p*>).i) by A10,A9,A8,FINSEQ_3:25,NAT_D:55;
thus k = (Sum Card ((F^<*p*>)|(i-'1))) + j by A8,A11,XREAL_1:235;
hence thesis by A3,A8,A10,A12,FINSEQ_1:def 7;
end;
suppose
A13: k in dom FlattenSeq F;
then consider i, j being Nat such that
A14: i in dom F and
A15: j in dom (F.i) and
A16: k = (Sum Card (F|(i-'1))) + j and
A17: (F.i).j = (FlattenSeq F).k by A2;
take i, j;
dom F c= dom (F^<*p*>) by FINSEQ_1:26;
hence i in dom (F^<*p*>) by A14;
thus j in dom ((F^<*p*>).i) by A14,A15,FINSEQ_1:def 7;
A18: i-'1 <= i by NAT_D:35;
i <= len F by A14,FINSEQ_3:25;
hence k = (Sum Card ((F^<*p*>)|(i-'1))) + j by A16,A18,FINSEQ_5:22
,XXREAL_0:2;
(F^<*p*>).i = (F.i) by A14,FINSEQ_1:def 7;
hence thesis by A3,A13,A17,FINSEQ_1:def 7;
end;
end;
A19: P[F];
thus for F being FinSequence of D* holds P[F] from FINSEQ_2:sch 2(A19, A1);
end;
theorem Th29:
for D being set, F being FinSequence of D*, 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
let D be set;
set F = <*>(D*);
defpred P[FinSequence of D*] means for i, j be Element of NAT st i in dom $1
& j in dom ($1.i) holds (Sum Card ($1|(i-'1))) + j in dom FlattenSeq $1 & ($1.i
).j = (FlattenSeq $1).((Sum Card ($1|(i-'1))) + j);
A1: for F be FinSequence of D*, p be Element of D* st P[F] holds P[F^<*p*>]
proof
let F be FinSequence of D*, p be Element of D*;
assume
A2: 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);
let i, j be Element of NAT;
assume that
A3: i in dom (F^<*p*>) and
A4: j in dom ((F^<*p*>).i);
A5: FlattenSeq (F^<*p*>) = FlattenSeq F ^ FlattenSeq <*p*> by Th3
.= FlattenSeq F ^ p by Th1;
per cases;
suppose
A6: not i in dom F;
1 <= i by A3,FINSEQ_3:25;
then len F < i by A6,FINSEQ_3:25;
then
A7: len F + 1 <= i by NAT_1:13;
A8: len (F^<*p*>) = len F + len <*p*> by FINSEQ_1:22
.= len F + 1 by FINSEQ_1:40;
i <= len (F^<*p*>) by A3,FINSEQ_3:25;
then
A9: i = len F + 1 by A8,A7,XXREAL_0:1;
then i-'1 = len F by NAT_D:34;
then
A10: (F^<*p*>)|(i-'1) = F by FINSEQ_5:23;
A11: Sum Card F = len FlattenSeq F by Th26;
1 in dom <*p*> by FINSEQ_5:6;
then
A12: (F^<*p*>).i = <*p*>.1 by A9,FINSEQ_1:def 7
.= p;
hence
(Sum Card ((F^<*p*>)|(i-'1))) + j in dom FlattenSeq (F^<*p*>) by A4,A5
,A10,A11,FINSEQ_1:28;
thus thesis by A4,A5,A12,A10,A11,FINSEQ_1:def 7;
end;
suppose
A13: i in dom F;
then
A14: j in dom (F.i) by A4,FINSEQ_1:def 7;
then
A15: (Sum Card (F|(i-'1))) + j in dom FlattenSeq F by A2,A13;
A16: i-'1 <= i by NAT_D:35;
i <= len F by A13,FINSEQ_3:25;
then
A17: (F^<*p*>)|(i-'1) = F|(i-'1) by A16,FINSEQ_5:22,XXREAL_0:2;
dom FlattenSeq F c= dom FlattenSeq (F^<*p*>) by A5,FINSEQ_1:26;
hence (Sum Card ((F^<*p*>)|(i-'1))) + j in dom FlattenSeq (F^<*p*>) by
A17,A15;
thus ((F^<*p*>).i).j = (F.i).j by A13,FINSEQ_1:def 7
.= (FlattenSeq F).((Sum Card (F|(i-'1))) + j) by A2,A13,A14
.= (FlattenSeq (F^<*p*>)).((Sum Card ((F^<*p*>)|(i-'1)))+j) by A5,A17
,A15,FINSEQ_1:def 7;
end;
end;
A18: P[F];
thus for F being FinSequence of D* holds P[F] from FINSEQ_2:sch 2(A18, A1);
end;
theorem Th30:
for X, Y being non empty set, f being FinSequence of X*, v being
Function of X, Y holds (dom f --> v)**f is FinSequence of Y*
proof
let X, Y be non empty set, f be FinSequence of X*, v be Function of X, Y;
set F = (dom f --> v)**f;
A1: dom F = dom (dom f --> v) /\ dom f by PBOOLE:def 19
.= dom f /\ dom f
.= dom f;
A2: rng F c= Y*
proof
let y be object;
assume y in rng F;
then consider x being object such that
A3: x in dom F and
A4: y = F.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A1,A3;
f.x in X* by A1,A3,FINSEQ_2:11;
then
A5: f.x is FinSequence of X by FINSEQ_1:def 11;
y = (dom f --> v).x * (f.x) by A3,A4,PBOOLE:def 19
.= v*(f.x) by A1,A3,FUNCOP_1:7;
then y is FinSequence of Y by A5,FINSEQ_2:32;
hence thesis by FINSEQ_1:def 11;
end;
dom F = Seg len f by A1,FINSEQ_1:def 3;
then F is FinSequence-like by FINSEQ_1:def 2;
hence thesis by A2,FINSEQ_1:def 4;
end;
theorem
for X, Y being non empty set, f being FinSequence of X*, v being
Function of X, Y ex F being FinSequence of Y* st F = (dom f --> v)**f & v*
FlattenSeq f = FlattenSeq F
proof
let X, Y be non empty set, f be FinSequence of X*, v be Function of X, Y;
reconsider F = (dom f --> v)**f as FinSequence of Y* by Th30;
take F;
thus F = (dom f --> v)**f;
set Fl = FlattenSeq F;
set fl = FlattenSeq f;
reconsider vfl = v*fl as FinSequence of Y;
now
len fl = len vfl by FINSEQ_2:33;
hence
A1: dom fl = dom vfl by FINSEQ_3:29;
A2: dom F = dom (dom f --> v) /\ dom f by PBOOLE:def 19
.= dom f /\ dom f
.= dom f;
A3: now
let k be object;
assume
A4: k in dom f;
then reconsider k1=k as Element of NAT;
A5: F.k = ((dom f --> v).k)*(f.k) by A2,A4,PBOOLE:def 19
.= v*(f.k) by A4,FUNCOP_1:7;
f.k1 in X* by A4,FINSEQ_2:11;
then reconsider fk = f.k as FinSequence of X by FINSEQ_1:def 11;
thus (Card f).k = len fk by A4,CARD_3:def 2
.= len (F.k1) by A5,FINSEQ_2:33
.= (Card F).k by A2,A4,CARD_3:def 2;
end;
A6: dom f = dom Card f & dom f = dom Card F by A2,CARD_3:def 2;
then
A7: Card f = Card F by A3;
len fl = len Fl by A6,A3,Th27,FUNCT_1:2;
hence dom fl = dom Fl by FINSEQ_3:29;
let k be Nat;
assume
A8: k in dom fl;
then consider i, j being Nat such that
A9: i in dom f and
A10: j in dom (f.i) and
A11: k = (Sum Card (f|(i-'1))) + j and
A12: (f.i).j = fl.k by Th28;
f.i in X* by A9,FINSEQ_2:11;
then reconsider fi = f.i as FinSequence of X by FINSEQ_1:def 11;
F.i = ((dom f --> v).i)*(f.i) by A2,A9,PBOOLE:def 19
.= v*(f.i) by A9,FUNCOP_1:7;
then len fi = len (F.i) by FINSEQ_2:33;
then
A13: j in dom (F.i) by A10,FINSEQ_3:29;
f.i in X* by A9,FINSEQ_2:11;
then dom v = X & f.i is FinSequence of X by FINSEQ_1:def 11,FUNCT_2:def 1;
then rng (f.i) c= dom v by FINSEQ_1:def 4;
then
A14: j in dom (v*(f.i)) by A10,RELAT_1:27;
Card (F|(i-'1)) = Card (F|Seg (i-'1)) by FINSEQ_1:def 16
.= (Card f)|Seg (i-'1) by A7,Th22
.= Card (f|Seg(i-'1)) by Th22
.= Card (f|(i-'1)) by FINSEQ_1:def 16;
then Fl.k = (F.i).j by A2,A9,A11,A13,Th29
.= (((dom f --> v).i)*(f.i)).j by A2,A9,PBOOLE:def 19
.= (v*(f.i)).j by A9,FUNCOP_1:7
.= v.((f.i).j) by A14,FUNCT_1:12;
hence vfl.k = Fl.k by A1,A8,A12,FUNCT_1:12;
end;
hence thesis;
end;
begin :: Functions yielding natural and real numbers -------------------------
registration
let f be natural-valued Function, x be object, n be Nat;
cluster f+*(x,n) -> natural-valued;
coherence
proof
set F = f+*(x,n);
let a be object such that
a in dom F;
per cases;
suppose
x in dom f & x = a;
hence thesis by FUNCT_7:31;
end;
suppose
x in dom f & x <> a;
then F.a = f.a by FUNCT_7:32;
hence thesis;
end;
suppose
not x in dom f;
then F.a = f.a by FUNCT_7:def 3;
hence thesis;
end;
end;
end;
registration
let f be real-valued Function, x be object, n be Real;
cluster f+*(x,n) -> real-valued;
coherence
proof
set F = f+*(x,n);
let a be object such that
a in dom F;
per cases;
suppose
x in dom f & x = a;
hence thesis by FUNCT_7:31;
end;
suppose
x in dom f & x <> a;
then F.a = f.a by FUNCT_7:32;
hence thesis;
end;
suppose
not x in dom f;
then F.a = f.a by FUNCT_7:def 3;
hence thesis;
end;
end;
end;
definition
let X be set, b1, b2 be complex-valued ManySortedSet of X;
redefine func b1+b2 -> ManySortedSet of X means :: redefines + (VALUED_1, definition)
:Def5:
for x being object holds it.x = b1.x+b2.x;
coherence;
compatibility
proof
let f be ManySortedSet of X;
A1: dom b1 = X & dom b2 = X by PARTFUN1:def 2;
then
A2: dom f = dom b1 /\ dom b2 by PARTFUN1:def 2;
thus f = b1+b2 implies for x being object holds f.x = b1.x+b2.x
proof
assume
A3: f = b1+b2;
let x be object;
per cases;
suppose
x in X;
hence thesis by A1,A2,A3,VALUED_1:def 1;
end;
suppose
A4: not x in X;
then b1.x = 0 & b2.x = 0 by A1,FUNCT_1:def 2;
hence thesis by A1,A2,A4,FUNCT_1:def 2;
end;
end;
assume for x being object holds f.x = b1.x+b2.x;
then for c being object st c in dom f holds f.c = b1.c+b2.c;
hence thesis by A2,VALUED_1:def 1;
end;
end;
definition
let X be set, b1, b2 be natural-valued ManySortedSet of X;
func b1 -' b2 -> ManySortedSet of X means
:Def6:
for x being object holds it.x = b1.x -' b2.x;
existence
proof
deffunc F(object) = b1.$1 -' b2.$1;
consider f being ManySortedSet of X such that
A1: for i being object st i in X holds f.i = F(i) from PBOOLE:sch 4;
take f;
let x be object;
per cases;
suppose
x in X;
hence thesis by A1;
end;
suppose
A2: not x in X;
A3: dom b2 = X by PARTFUN1:def 2;
A4: dom b1 = X by PARTFUN1:def 2;
dom f = X by PARTFUN1:def 2;
hence f.x = 0 by A2,FUNCT_1:def 2
.= 0-'0 by XREAL_1:232
.= 0-'b2.x by A2,A3,FUNCT_1:def 2
.= b1.x-'b2.x by A2,A4,FUNCT_1:def 2;
end;
end;
uniqueness
proof
let it1, it2 be ManySortedSet of X such that
A5: for x being object holds it1.x = b1.x-'b2.x and
A6: for x being object holds it2.x = b1.x-'b2.x;
now
let x be object;
assume x in X;
thus it1.x = b1.x-'b2.x by A5
.= it2.x by A6;
end;
hence it1 = it2;
end;
end;
theorem
for X being set, 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
let X be set, b, b1, b2 be real-valued ManySortedSet of X;
assume
A1: for x being object st x in X holds b.x = b1.x+b2.x;
now
let x be object;
per cases;
suppose
x in X;
hence b.x = b1.x+b2.x by A1;
end;
suppose
A2: not x in X;
A3: dom b2 = X by PARTFUN1:def 2;
A4: dom b1 = X by PARTFUN1:def 2;
dom b = X by PARTFUN1:def 2;
hence b.x = 0 qua Nat + (0 qua Nat) by A2,FUNCT_1:def 2
.= 0 qua Nat+b2.x by A2,A3,FUNCT_1:def 2
.= b1.x+b2.x by A2,A4,FUNCT_1:def 2;
end;
end;
hence thesis by Def5;
end;
theorem Th33:
for X being set, 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
let X be set, b, b1, b2 be natural-valued ManySortedSet of X;
assume
A1: for x being object st x in X holds b.x = b1.x-'b2.x;
now
let x be object;
per cases;
suppose
x in X;
hence b.x = b1.x -' b2.x by A1;
end;
suppose
A2: not x in X;
A3: dom b2 = X by PARTFUN1:def 2;
A4: dom b1 = X by PARTFUN1:def 2;
dom b = X by PARTFUN1:def 2;
hence b.x = 0 by A2,FUNCT_1:def 2
.= 0-'0 by XREAL_1:232
.= 0-'b2.x by A2,A3,FUNCT_1:def 2
.= b1.x-'b2.x by A2,A4,FUNCT_1:def 2;
end;
end;
hence thesis by Def6;
end;
registration
let X be set, b1, b2 be natural-valued ManySortedSet of X;
cluster b1+b2 -> natural-valued;
coherence;
cluster b1-'b2 -> natural-valued;
coherence
proof
set f = b1 -' b2;
rng f c= NAT
proof
let y be object;
assume y in rng f;
then consider x being object such that
x in dom f and
A1: y = f.x by FUNCT_1:def 3;
f.x = b1.x -' b2.x by Def6;
hence thesis by A1;
end;
hence thesis;
end;
end;
theorem Th34:
for X being set, b1, b2, b3 being real-valued ManySortedSet of X
holds (b1+b2)+b3 = b1+(b2+b3)
proof
let X be set, b1, b2, b3 be real-valued ManySortedSet of X;
now
let x be object;
assume x in X;
thus ((b1+b2)+b3).x = (b1+b2).x+b3.x by Def5
.= b1.x+b2.x+b3.x by Def5
.= b1.x+(b2.x+b3.x)
.= b1.x+(b2+b3).x by Def5
.= (b1+(b2+b3)).x by Def5;
end;
hence thesis;
end;
theorem
for X being set, b, c, d being natural-valued ManySortedSet of X holds
b-'c-'d = b-'(c+d)
proof
let X be set, b, c, d be natural-valued ManySortedSet of X;
now
let x be object;
assume x in X;
thus (b-'c-'d).x = (b-'c).x -' d.x by Def6
.= b.x-'c.x-'d.x by Def6
.= b.x-'(c.x+d.x) by NAT_2:30
.= b.x-'(c+d).x by Def5;
end;
hence thesis by Th33;
end;
begin :: The support of a function --------------------------------------------
definition
let f be Function;
func support f -> set means
:Def7:
for x being object holds x in it iff f.x <> 0;
existence
proof
defpred P[object] means f.$1 <> 0;
consider A being set such that
A1: for x being object holds x in A iff x in dom f & P[x] from XBOOLE_0:
sch 1;
take A;
let x be object;
thus x in A implies f.x <> 0 by A1;
assume
A2: f.x <> 0;
then x in dom f by FUNCT_1:def 2;
hence thesis by A1,A2;
end;
uniqueness
proof
let A,B be set such that
A3: for x being object holds x in A iff f.x <> 0 and
A4: for x being object holds x in B iff f.x <> 0;
for x being object holds x in A iff x in B
proof
let x be object;
x in A iff f.x <> 0 by A3;
hence thesis by A4;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th36:
for f being Function holds support f c= dom f
proof
let f be Function, x be object;
assume x in support f;
then f.x <> 0 by Def7;
hence thesis by FUNCT_1:def 2;
end;
definition
let f be Function;
attr f is finite-support means
:Def8:
support f is finite;
end;
registration
cluster finite -> finite-support for Function;
coherence
proof
let f be Function;
assume f is finite;
then dom f is finite;
hence support f is finite by Th36,FINSET_1:1;
end;
end;
registration
cluster natural-valued finite-support non empty for Function;
existence
proof
take f = 0 .--> 1;
thus f is natural-valued;
thus f is finite-support;
thus thesis;
end;
end;
registration
let f be finite-support Function;
cluster support f -> finite;
coherence by Def8;
end;
registration
let X be set;
cluster finite-support for Function of X, NAT;
existence
proof
set f = X --> 0;
reconsider f as Function of X, NAT;
take f;
now
assume support f <> {};
then consider x being object such that
A3: x in support f by XBOOLE_0:def 1;
f.x <> 0 by A3,Def7;
hence contradiction;
end;
hence support f is finite;
end;
end;
registration
let f be finite-support Function, x, y be set;
cluster f+*(x,y) -> finite-support;
coherence
proof
set F = f+*(x,y);
support F c= support f \/ {x}
proof
let a be object;
assume a in support F;
then
A1: F.a <> 0 by Def7;
per cases;
suppose
x in dom f & a = x;
then a in {x} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x in dom f & a <> x;
then F.a = f.a by FUNCT_7:32;
then a in support f by A1,Def7;
hence thesis by XBOOLE_0:def 3;
end;
suppose
not x in dom f;
then F.a = f.a by FUNCT_7:def 3;
then a in support f by A1,Def7;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence support (f+*(x,y)) is finite;
end;
end;
registration
let X be set;
cluster natural-valued finite-support for ManySortedSet of X;
existence
proof
set f = X --> 0;
reconsider f as ManySortedSet of X;
take f;
thus f is natural-valued;
support f = {}
proof
assume not thesis;
then consider x being object such that
A2: x in support f by XBOOLE_0:def 1;
f.x = 0;
hence contradiction by A2,Def7;
end;
hence thesis;
end;
end;
theorem Th37:
for X being set, b1, b2 being natural-valued ManySortedSet of X
holds support (b1+b2) = support b1 \/ support b2
proof
let X be set, b1, b2 be natural-valued ManySortedSet of X;
now
let x be object;
hereby
assume x in support b1 \/ support b2;
then x in support b1 or x in support b2 by XBOOLE_0:def 3;
then b1.x <> 0 or b2.x <> 0 by Def7;
then b1.x + b2.x <> 0;
hence (b1+b2).x <> 0 by Def5;
end;
assume
A1: (b1+b2).x <> 0;
assume
A2: not x in support b1 \/ support b2;
then not x in support b1 by XBOOLE_0:def 3;
then
A3: b1.x = 0 by Def7;
not x in support b2 by A2,XBOOLE_0:def 3;
then b1.x+b2.x = 0 by A3,Def7;
hence contradiction by A1,Def5;
end;
hence thesis by Def7;
end;
theorem Th38:
for X being set, b1, b2 being natural-valued ManySortedSet of X
holds support (b1-'b2) c= support b1
proof
let X be set, b1, b2 be natural-valued ManySortedSet of X;
thus support (b1-'b2) c= support b1
proof
let x be object;
assume
A1: x in support (b1-'b2);
assume not x in support b1;
then b1.x = 0 by Def7;
then b1.x-'b2.x = 0 by NAT_2:8;
then (b1-'b2).x = 0 by Def6;
hence contradiction by A1,Def7;
end;
end;
begin :: Bags -----------------------------------------------------------------
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 -> finite-support for ManySortedSet of X;
coherence
proof
let f be ManySortedSet of X;
support f c= dom f & dom f = X by Th36,PARTFUN1:def 2;
hence support f is finite;
end;
end;
registration
let X be set, b1, b2 be bag of X;
cluster b1+b2 -> finite-support;
coherence
proof
support (b1+b2) = support b1 \/ support b2 by Th37;
hence support (b1+b2) is finite;
end;
cluster b1-'b2 -> finite-support;
coherence
proof
support (b1-'b2) c= support b1 by Th38;
hence support (b1-'b2) is finite;
end;
end;
theorem Th39:
for X being set holds X--> 0 is bag of X
proof
let X be set;
set f = X --> 0;
support f = {}
proof
assume not thesis;
then consider x being object such that
A2: x in support f by XBOOLE_0:def 1;
f.x = 0;
hence contradiction by A2,Def7;
end;
hence thesis by Def8;
end;
definition
let n be Ordinal, p, q be bag of n;
pred p < q means
ex k being Ordinal st p.k < q.k & for l being
Ordinal st l in k holds p.l = q.l;
asymmetry
proof
let p, q be bag of n;
given k being Ordinal such that
A1: p.k < q.k and
A2: for l being Ordinal st l in k holds p.l = q.l;
given k1 being Ordinal such that
A3: q.k1 < p.k1 and
A4: for l being Ordinal st l in k1 holds q.l = p.l;
per cases by ORDINAL1:14;
suppose
k in k1;
hence contradiction by A1,A4;
end;
suppose
k1 in k;
hence contradiction by A2,A3;
end;
suppose
k1 = k;
hence contradiction by A1,A3;
end;
end;
end;
theorem Th40:
for n being Ordinal, p, q, r being bag of n st p < q & q < r holds p < r
proof
let n be Ordinal, p, q, r be bag of n;
assume that
A1: p < q and
A2: q < r;
consider k being Ordinal such that
A3: p.k < q.k and
A4: for l being Ordinal st l in k holds p.l = q.l by A1;
consider m being Ordinal such that
A5: q.m < r.m and
A6: for l being Ordinal st l in m holds q.l = r.l by A2;
take n = k /\ m;
A7: n c= m & n <> m iff n c< m;
A8: n c= k & n <> k iff n c< k;
now
per cases by ORDINAL1:14;
suppose
k in m;
hence p.n < r.n by A3,A6,A8,A7,ORDINAL1:11,ORDINAL3:13,XBOOLE_1:17;
end;
suppose
m in k;
hence p.n < r.n by A4,A5,A8,A7,ORDINAL1:11,ORDINAL3:13,XBOOLE_1:17;
end;
suppose
m = k;
hence p.n < r.n by A3,A5,XXREAL_0:2;
end;
end;
hence p.n < r.n;
let l be Ordinal;
A9: n c= m by XBOOLE_1:17;
assume
A10: l in n;
n c= k by XBOOLE_1:17;
hence p.l = q.l by A4,A10
.= r.l by A6,A9,A10;
end;
definition
let n be Ordinal, p, q be bag of n;
pred p <=' q means
p < q or p = q;
reflexivity;
end;
theorem Th41:
for n being Ordinal, p, q, r being bag of n st p <=' q & q <=' r
holds p <=' r
by Th40;
theorem
for n being Ordinal, p, q, r being bag of n st p < q & q <=' r holds p < r
by Th40;
theorem
for n being Ordinal, p, q, r being bag of n st p <=' q & q < r holds p < r
by Th40;
theorem Th44:
for n being Ordinal, p, q being bag of n holds p <=' q or q <=' p
proof
let n be Ordinal, p, q be bag of n;
assume
A1: not p <=' q;
then consider i being object such that
A2: i in n and
A3: p.i <> q.i by PBOOLE:3;
A4: not p < q by A1;
defpred P[set] means p.$1 <> q.$1;
A5: ex i being Ordinal st P[i] by A2,A3;
consider m being Ordinal such that
A6: P[m] and
A7: for n being Ordinal st P[n] holds m c= n from ORDINAL1:sch 1(A5);
A8: for l being Ordinal st l in m holds q.l = p.l by A7,ORDINAL1:5;
per cases by A6,XXREAL_0:1;
suppose
p.m < q.m;
hence thesis by A4,A8;
end;
suppose
p.m > q.m;
then q < p by A8;
hence thesis;
end;
end;
definition
let X be set, d, b be bag of X;
pred d divides b means
for k being object holds d.k <= b.k;
reflexivity;
end;
theorem Th45:
for n being set, 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
let n be set, d, b be bag of n;
assume
A1: for k being object st k in n holds d.k <= b.k;
let k be object;
per cases;
suppose
k in dom d;
then k in n;
hence thesis by A1;
end;
suppose
not k in dom d;
hence thesis by FUNCT_1:def 2;
end;
end;
theorem Th46:
for n being set, b1, b2 being bag of n st b1 divides b2
holds b2 -' b1 + b1 = b2
proof
let n be set, b1, b2 be bag of n such that
A1: b1 divides b2;
now
let k be object;
assume k in n;
A2: b1.k <= b2.k by A1;
thus (b2 -' b1 + b1).k = (b2-'b1).k + b1.k by Def5
.= b2.k -' b1.k + b1.k by Def6
.= b2.k + b1.k -' b1.k by A2,NAT_D:38
.= b2.k by NAT_D:34;
end;
hence thesis;
end;
theorem Th47:
for X being set, b1, b2 being bag of X holds b2 + b1 -' b1 = b2
proof
let X be set, b1, b2 be bag of X;
now
let k be object;
assume k in X;
thus (b2 + b1 -' b1).k = (b2+b1).k -' b1.k by Def6
.= b2.k+b1.k -' b1.k by Def5
.= b2.k by NAT_D:34;
end;
hence thesis;
end;
theorem Th48:
for n being Ordinal, d, b being bag of n st d divides b holds d <=' b
proof
let n be Ordinal, d, b be bag of n;
assume that
A1: d divides b and
A2: not d < b;
now
defpred P[set] means d.$1 < b.$1;
let p be object;
assume p in n;
then reconsider p9 = p as Ordinal;
assume
A3: d.p <> b.p;
d.p9 <= b.p9 by A1;
then d.p9 < b.p9 by A3,XXREAL_0:1;
then
A4: ex p being Ordinal st P[p];
consider k being Ordinal such that
A5: P[k] and
A6: for m being Ordinal st P[m] holds k c= m from ORDINAL1:sch 1(A4);
now
let l be Ordinal;
assume l in k;
then
A7: b.l <= d.l by A6,ORDINAL1:5;
d.l <= b.l by A1;
hence d.l = b.l by A7,XXREAL_0:1;
end;
hence contradiction by A2,A5;
end;
hence thesis;
end;
theorem Th49:
for n being set, b,b1,b2 being bag of n st b = b1 + b2 holds b1 divides b
proof
let n be set, b,b1,b2 be bag of n;
assume
A1: b = b1 + b2;
now
let k be object;
assume k in n;
b.k = b1.k+b2.k by A1,Def5;
hence b1.k <= b.k by NAT_1:11;
end;
hence thesis by Th45;
end;
definition
let X be set;
func Bags X -> set means
:Def12:
for x being set holds x in it iff x is bag of X;
existence
proof
defpred P[object] means $1 is bag of X;
consider A being set such that
A1: for x being object holds x in A iff x in Funcs(X,NAT) & P[x] from
XBOOLE_0:sch 1;
take A;
let x be set;
thus x in A implies x is bag of X by A1;
assume
A2: x is bag of X;
then reconsider b = x as bag of X;
dom b = X & rng b c= NAT by PARTFUN1:def 2;
then x in Funcs(X,NAT) by FUNCT_2:def 2;
hence thesis by A1,A2;
end;
uniqueness
proof
let A,B be set such that
A3: for x being set holds x in A iff x is bag of X and
A4: for x being set holds x in B iff x is bag of X;
now
let x be object;
x in A iff x is bag of X by A3;
hence x in A iff x in B by A4;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let X be set;
redefine func Bags X -> Subset of Bags X; :: redefines Bags (PRE_POLY, definition)
coherence
proof
Bags X c= Bags X;
hence thesis;
end;
end;
theorem
Bags {} = {{}}
proof
now
let x be set;
hereby
assume x in {{}};
then x = {} by TARSKI:def 1;
hence x is bag of {} by PARTFUN1:def 2,RELAT_1:38,def 18;
end;
assume x is bag of {};
then reconsider x9 = x as ManySortedSet of {};
x9 = {};
hence x in {{}} by TARSKI:def 1;
end;
hence thesis by Def12;
end;
registration
let X be set;
cluster Bags X -> non empty;
coherence
proof
X --> 0 is bag of X by Th39;
hence thesis by Def12;
end;
end;
registration
let X be set;
cluster -> functional for Subset of Bags X;
coherence
by Def12;
end;
registration
let X be set, B be Subset of Bags X;
cluster -> X-defined for Element of B;
coherence
proof
let E be Element of B;
per cases;
suppose B is non empty;
then reconsider B as non empty Subset of Bags X;
reconsider E as Element of B;
E is bag of X by Def12;
hence thesis;
end;
suppose B is empty;
then E is empty by SUBSET_1:def 1;
hence thesis by RELAT_1:171;
end;
end;
end;
registration
let X be set, B be non empty Subset of Bags X;
cluster -> total natural-valued finite-support for Element of B;
coherence by Def12;
end;
notation
let X be set;
synonym EmptyBag X for EmptyMS X;
end;
definition
let X be set;
redefine func EmptyBag X -> Element of Bags X; :: redefines EmptyBag (PRE_POLY, synonym) → EmptyMS (PBOOLE, definition)
coherence
proof
X --> 0 is bag of X by Th39;
hence thesis by Def12;
end;
::$CD
end;
::$CT
theorem
for X be set, b being bag of X holds b+EmptyBag X = b
proof
let X be set, b be bag of X;
now
let x be object;
assume
x in X;
thus (b+EmptyBag X).x = b.x+((EmptyBag X).x qua Nat) by Def5
.= b.x;
end;
hence thesis;
end;
theorem Th52:
for X be set, b being bag of X holds b-'EmptyBag X = b
proof
let X be set, b be bag of X;
now
let x be object;
assume x in X;
thus (b-'EmptyBag X).x = b.x-'(EmptyBag X).x by Def6
.= b.x by NAT_D:40;
end;
hence thesis;
end;
theorem
for X be set, b being bag of X holds (EmptyBag X) -' b = EmptyBag X
proof
let X be set, b be bag of X;
now
let x be object;
assume x in X;
thus ((EmptyBag X)-'b).x = (EmptyBag X).x-'b.x by Def6
.= (EmptyBag X).x by NAT_2:8;
end;
hence thesis;
end;
theorem Th54:
for X being set, b being bag of X holds b-'b = EmptyBag X
proof
let X be set, b be bag of X;
now
let x be object;
assume x in X;
thus (b-'b).x = b.x -' b.x by Def6
.= 0 by XREAL_1:232
.= (EmptyBag X).x;
end;
hence thesis;
end;
theorem Th55:
for n being set, b1, b2 be bag of n st b1 divides b2 & b2 -' b1
= EmptyBag n holds b2 = b1
proof
let n be set, b1, b2 be bag of n such that
A1: b1 divides b2 and
A2: b2 -' b1 = EmptyBag n;
now
let k be object;
assume k in n;
0 = (b2-'b1).k by A2
.= b2.k -' b1.k by Def6;
then
A3: b2.k <= b1.k by NAT_D:36;
b1.k <= b2.k by A1;
hence b2.k = b1.k by A3,XXREAL_0:1;
end;
hence thesis;
end;
theorem
for n being set, b being bag of n st b divides EmptyBag n holds
EmptyBag n = b;
theorem Th57:
for n being set, b being bag of n holds EmptyBag n divides b;
theorem
for n being Ordinal, b being bag of n holds EmptyBag n <=' b by Th48,Th57;
definition
let n be Ordinal;
func BagOrder n -> Order of Bags n means
:Def13:
for p, q being bag of n holds [p, q] in it iff p <=' q;
existence
proof
defpred P[object,object] means
ex b1,b2 be Element of Bags n st $1 = b1 & $2 =
b2 & b1 <=' b2;
consider BO being Relation of Bags n, Bags n such that
A1: for x, y being object holds [x,y] in BO iff x in Bags n & y in Bags n
& P[x,y] from RELSET_1:sch 1;
A2: BO is_antisymmetric_in Bags n
proof
let x, y be object;
assume that
x in Bags n and
y in Bags n and
A3: [x,y] in BO and
A4: [y,x] in BO;
A5: ex b19, b29 being Element of Bags n st y = b19 & x = b29 & b19 <='
b29 by A1,A4;
consider b1, b2 being Element of Bags n such that
A6: x = b1 & y = b2 and
A7: b1 <=' b2 by A1,A3;
b1 < b2 or b1 = b2 by A7;
hence thesis by A6,A5;
end;
A8: BO is_reflexive_in Bags n
by A1;
then
A9: dom BO = Bags n & field BO = Bags n by ORDERS_1:13;
BO is_transitive_in Bags n
proof
let x, y, z be object such that
x in Bags n and
y in Bags n and
z in Bags n and
A10: [x,y] in BO and
A11: [y,z] in BO;
consider b1, b2 being Element of Bags n such that
A12: x = b1 and
A13: y = b2 & b1 <=' b2 by A1,A10;
consider b19, b29 being Element of Bags n such that
A14: y = b19 and
A15: z = b29 and
A16: b19 <=' b29 by A1,A11;
reconsider B1 = b1, B29 = b29 as bag of n;
B1 <=' B29 by A13,A14,A16,Th41;
hence thesis by A1,A12,A15;
end;
then reconsider BO as Order of Bags n by A8,A2,A9,PARTFUN1:def 2
,RELAT_2:def 9,def 12,def 16;
take BO;
let p, q be bag of n;
hereby
assume [p, q] in BO;
then ex b1, b2 being Element of Bags n st p = b1 & q = b2 & b1 <=' b2 by
A1;
hence p <=' q;
end;
p in Bags n & q in Bags n by Def12;
hence thesis by A1;
end;
uniqueness
proof
let B1, B2 be Order of Bags n such that
A17: for p, q being bag of n holds [p, q] in B1 iff p <=' q and
A18: for p, q being bag of n holds [p, q] in B2 iff p <=' q;
let a, b be object;
hereby
assume
A19: [a,b] in B1;
then consider b1, b2 being object such that
A20: [a,b] = [b1,b2] and
A21: b1 in Bags n & b2 in Bags n by RELSET_1:2;
reconsider b1, b2 as bag of n by A21;
b1 <=' b2 by A17,A19,A20;
hence [a,b] in B2 by A18,A20;
end;
assume
A22: [a,b] in B2;
then consider b1, b2 being object such that
A23: [a,b] = [b1,b2] and
A24: b1 in Bags n & b2 in Bags n by RELSET_1:2;
reconsider b1, b2 as bag of n by A24;
b1 <=' b2 by A18,A22,A23;
hence thesis by A17,A23;
end;
end;
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
let n be Ordinal;
set BO = BagOrder n;
let x, y be object;
assume that
A1: x in Bags n & y in Bags n and
A2: [x,y] in BO and
A3: [y,x] in BO;
reconsider b1 = x, b2 = y as bag of n by A1;
b1 <=' b2 by A2,Def13;
then
A4: b1 < b2 or b1 = b2;
reconsider b19 = y, b29 = x as bag of n by A1;
b19 <=' b29 by A3,Def13;
hence thesis by A4;
end;
Lm3: for n being Ordinal holds BagOrder n is_transitive_in Bags n
proof
let n be Ordinal;
set BO = BagOrder n;
let x, y, z be object such that
A1: x in Bags n and
A2: y in Bags n and
A3: z in Bags n and
A4: [x,y] in BO & [y,z] in BO;
reconsider b19= y, b29 = z as bag of n by A2,A3;
reconsider b1 = x, b2 = y as bag of n by A1,A2;
reconsider B1 = b1, B29 = b29 as bag of n;
b1 <=' b2 & b19 <=' b29 by A4,Def13;
then B1 <=' B29 by Th41;
hence thesis by Def13;
end;
Lm4: for n being Ordinal holds BagOrder n linearly_orders Bags n
proof
let n be Ordinal;
set BO = BagOrder n;
A1: BO is_transitive_in Bags n by Lm3;
A2: BO is_connected_in Bags n
proof
let x, y be object;
assume that
A3: x in Bags n & y in Bags n and
x <> y and
A4: not [x,y] in BO;
reconsider p = x, q = y as bag of n by A3;
not p <=' q by A4,Def13;
then q <=' p by Th44;
hence thesis by Def13;
end;
BO is_reflexive_in Bags n & BO is_antisymmetric_in Bags n by Lm1,Lm2;
hence thesis by A1,A2,ORDERS_1:def 9;
end;
registration
let n be Ordinal;
cluster BagOrder n -> being_linear-order;
coherence
proof
set BO = BagOrder n;
BO linearly_orders Bags n by Lm4;
then field BO = Bags n & BO is_connected_in Bags n by ORDERS_1:15,def 9;
then BO is connected;
hence thesis by ORDERS_1:def 6;
end;
end;
definition
let X be set, f be Function of X, NAT;
func NatMinor f -> Subset of Funcs(X, NAT) means
:Def14:
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
proof
defpred P[set] means ex g being natural-valued ManySortedSet of X st $1 =
g & for x being set st x in X holds g.x <= f.x;
consider IT being Subset of Funcs(X, NAT) such that
A1: for h being set holds h in IT iff h in Funcs(X, NAT) & P[h] from
SUBSET_1:sch 1;
take IT;
let g be natural-valued ManySortedSet of X;
hereby
assume g in IT;
then
ex g1 being natural-valued ManySortedSet of X st g1 = g & for x being
set st x in X holds g1.x <= f.x by A1;
hence for x being set st x in X holds g.x <= f.x;
end;
dom g = X & rng g c= NAT by PARTFUN1:def 2;
then g is Function of X, NAT by RELSET_1:4;
then
A2: g in Funcs(X, NAT) by FUNCT_2:8;
assume for x being set st x in X holds g.x <= f.x;
hence thesis by A1,A2;
end;
uniqueness
proof
let it1, it2 be Subset of Funcs(X, NAT) such that
A3: for g being natural-valued ManySortedSet of X holds g in it1 iff
for x being set st x in X holds g.x <= f.x and
A4: for g being natural-valued ManySortedSet of X holds g in it2 iff
for x being set st x in X holds g.x <= f.x;
now
let h be Element of Funcs(X, NAT);
hereby
assume h in it1;
then for x being set st x in X holds h.x <= f.x by A3;
hence h in it2 by A4;
end;
assume h in it2;
then for x being set st x in X holds h.x <= f.x by A4;
hence h in it1 by A3;
end;
hence thesis by SUBSET_1:3;
end;
end;
theorem Th59:
for X being set, f being Function of X, NAT holds f in NatMinor f
proof
let X be set, f be Function of X, NAT;
for x being set st x in X holds f.x <= f.x;
hence thesis by Def14;
end;
registration
let X be set, f be Function of X, NAT;
cluster NatMinor f -> non empty functional;
coherence by Th59;
end;
registration
let X be set, f be Function of X, NAT;
cluster -> natural-valued for Element of NatMinor f;
coherence
by FUNCT_2:92;
end;
theorem Th60:
for X being set, f being finite-support Function of X, NAT holds
NatMinor f c= Bags X
proof
let X be set, f be finite-support Function of X, NAT;
let x be object;
assume x in NatMinor f;
then reconsider x9 = x as Element of NatMinor f;
A1: dom x9 = X by FUNCT_2:92;
then
A2: x9 is ManySortedSet of X by PARTFUN1:def 2,RELAT_1:def 18;
support x9 c= support f
proof
let a be object;
A3: support x9 c= dom x9 by Th36;
assume
A4: a in support x9;
then x9.a <> 0 by Def7;
then f.a <> 0 by A1,A2,A4,A3,Def14;
hence thesis by Def7;
end;
then x is bag of X by A1,Def8,PARTFUN1:def 2,RELAT_1:def 18;
hence thesis by Def12;
end;
definition
let X be set, f be finite-support Function of X, NAT;
redefine func support f -> Element of Fin X; :: redefines support (PRE_POLY, definition)
coherence
proof
dom f = X by FUNCT_2:def 1;
then support f c= X by Th36;
hence thesis by FINSUB_1:def 5;
end;
end;
theorem Th61:
for X being non empty set, f being finite-support Function of X,
NAT holds card NatMinor f = multnat $$ (support f, addnat[:](f,1))
proof
let X be non empty set;
defpred P[Element of Fin X] means for f being Function of X, NAT st for x
being Element of X st not x in $1 holds f.x = 0 holds card NatMinor f = multnat
$$ ($1, addnat[:](f,1));
let f be finite-support Function of X, NAT;
A1: for x being Element of X holds not x in support f implies f.x = 0 by Def7;
A2: for B being Element of Fin X, b being Element of X holds P[B] & not b in
B implies P[B \/ {.b.}]
proof
let B be Element of Fin X, b be Element of X such that
A3: P[B] and
A4: not b in B;
let f be Function of X, NAT such that
A5: for x being Element of X st not x in B \/ {b} holds f.x = 0;
reconsider g = f+*(b,0) as Function of X, NAT;
g|B = f|B by A4,FUNCT_7:92;
then addnat[:](g,1)|B = addnat[:](f,1)|B by FUNCOP_1:28;
then
A6: (multnat $$ (B, addnat[:](g,1))) = (multnat $$ (B, addnat[:](f,1) ))
by SETWOP_2:7;
A7: dom f = X by FUNCT_2:def 1;
for x being Element of X st not x in B holds g.x = 0
proof
let x be Element of X such that
A8: not x in B;
per cases;
suppose
x = b;
hence thesis by A7,FUNCT_7:31;
end;
suppose
A9: x <> b;
A10: now
assume x in B \/ {b};
then x in B or x in {b} by XBOOLE_0:def 3;
hence contradiction by A8,A9,TARSKI:def 1;
end;
thus g.x = f.x by A9,FUNCT_7:32
.= 0 by A5,A10;
end;
end;
then
A11: card NatMinor g = (multnat $$ (B, addnat[:](g,1))) by A3;
then reconsider ng = NatMinor g as functional finite non empty set;
reconsider fb1 = f.b+1 as non zero Nat;
dom (addnat[:](f,1)) = X by FUNCT_2:def 1;
then
A12: addnat[:](f,1).b = addnat.(f.b,1) by FUNCOP_1:27
.= f.b+1 by BINOP_2:def 23;
set cng = card ng;
A13: f.b < f.b+1 by XREAL_1:29;
[:ng,f.b+1 :],NatMinor f are_equipotent
proof
deffunc F(Element of ng,Element of fb1) = $1+*(b,$2);
A14: for p being Element of ng, l being Element of fb1 holds F(p,l) in
NatMinor f
proof
let p be Element of ng, l be Element of fb1;
reconsider q = p as Element of NatMinor g;
fb1 c= NAT & l in fb1;
then reconsider k = l as Element of NAT;
p in NatMinor g;
then
A15: dom p = X by FUNCT_2:92;
then dom(p+*(b,l)) = X by FUNCT_7:30;
then reconsider
pbl = q+*(b,k) as natural-valued ManySortedSet of X by PARTFUN1:def 2
,RELAT_1:def 18;
for x being set st x in X holds pbl.x <= f.x
proof
let x be set;
assume
A16: x in X;
per cases;
suppose
A17: x = b;
k in Segm fb1;
then
A18: k < fb1 by NAT_1:44;
pbl.x = k by A15,A17,FUNCT_7:31;
hence thesis by A17,A18,NAT_1:13;
end;
suppose
A19: x <> b;
q is ManySortedSet of X by A15,PARTFUN1:def 2,RELAT_1:def 18;
then
A20: q.x <= g.x by A16,Def14;
pbl.x = q.x by A19,FUNCT_7:32;
hence thesis by A19,A20,FUNCT_7:32;
end;
end;
hence thesis by Def14;
end;
consider r being Function of [:ng,fb1:], NatMinor f such that
A21: for p being Element of ng, l being Element of fb1 holds r.(p,l)
= F(p,l) from FUNCT_7:sch 1(A14);
take r;
thus r is one-to-one
proof
let x1,x2 be object;
assume that
A22: x1 in dom r and
A23: x2 in dom r and
A24: r.x1 = r.x2;
consider p2, l2 being object such that
A25: x2 = [p2,l2] by A23,RELAT_1:def 1;
reconsider p2 as Element of NatMinor g by A23,A25,ZFMISC_1:87;
A26: dom p2 = X by FUNCT_2:92;
A27: l2 in fb1 by A23,A25,ZFMISC_1:87;
consider p1, l1 being object such that
A28: x1 = [p1,l1] by A22,RELAT_1:def 1;
reconsider p1 as Element of NatMinor g by A22,A28,ZFMISC_1:87;
A29: dom p1 = X by FUNCT_2:92;
then reconsider
p19 = p1, p29 = p2 as natural-valued ManySortedSet of X by A26,
PARTFUN1:def 2,RELAT_1:def 18;
l1 in fb1 by A22,A28,ZFMISC_1:87;
then
A30: p1+*(b,l1) = r.(p1,l1) by A21
.= r.(p2,l2) by A24,A28,A25
.= p2+*(b,l2) by A21,A27;
A31: now
let x be object;
assume x in X;
per cases;
suppose
A32: x = b;
A33: g.b = 0 by A7,FUNCT_7:31;
hence p19.x = 0 by A32,Def14
.= p29.x by A32,A33,Def14;
end;
suppose
A34: x <> b;
hence p19.x = (p1+*(b,l1)).x by FUNCT_7:32
.= p29.x by A30,A34,FUNCT_7:32;
end;
end;
l1 = (p1+*(b,l1)).b by A29,FUNCT_7:31
.= l2 by A30,A26,FUNCT_7:31;
hence thesis by A28,A25,A31,PBOOLE:3;
end;
thus
A35: dom r = [:ng,f.b+1 :] by FUNCT_2:def 1;
thus rng r c= NatMinor f;
thus NatMinor f c= rng r
proof
let x be object;
assume x in NatMinor f;
then reconsider e = x as Element of NatMinor f;
A36: dom e = X by FUNCT_2:92;
then dom (e+*(b,0)) = X by FUNCT_7:30;
then reconsider
eb0 = e+*(b,0) as natural-valued ManySortedSet of X by PARTFUN1:def 2
,RELAT_1:def 18;
A37: e is ManySortedSet of X by A36,PARTFUN1:def 2,RELAT_1:def 18;
now
let x be set;
assume
A38: x in X;
per cases;
suppose
x = b;
hence eb0.x <= g.x by A36,FUNCT_7:31;
end;
suppose
A39: x <> b;
then
A40: eb0.x = e.x by FUNCT_7:32;
e.x <= f.x by A37,A38,Def14;
hence eb0.x <= g.x by A39,A40,FUNCT_7:32;
end;
end;
then reconsider eb0 as Element of NatMinor g by Def14;
e.b <= f.b by A37,Def14;
then e.b < fb1 by A13,XXREAL_0:2;
then
A41: e.b in Segm fb1 by NAT_1:44;
then
A42: [eb0,e.b] in dom r by A35,ZFMISC_1:87;
e = e+*(b,e.b) by FUNCT_7:35
.= eb0+*(b,e.b) by FUNCT_7:34;
then e = r.(eb0,e.b) by A21,A41;
hence thesis by A42,FUNCT_1:def 3;
end;
end;
hence card NatMinor f = card [:ng,f.b+1 :] by CARD_1:5
.= cng * card(f.b+1) by CARD_2:46
.= cng * (f.b+1)
.= multnat.(multnat $$ (B, addnat[:](f,1)), f.b+1) by A11,A6,
BINOP_2:def 24
.= multnat $$ (B \/ {.b.}, addnat[:](f,1)) by A4,A12,SETWOP_2:2;
end;
A43: P[{}.X]
proof
let f be Function of X, NAT such that
A44: for x being Element of X st not x in {}.X holds f.x = 0;
now
let x be object;
hereby
assume
A45: x in NatMinor f;
then reconsider x9 = x as Function of X, NAT by FUNCT_2:66;
now
let c be Element of X;
f.c = 0 by A44;
hence x9.c = f.c by A45,Def14;
end;
hence x = f by FUNCT_2:63;
end;
thus x = f implies x in NatMinor f by Th59;
end;
then NatMinor f = {f} by TARSKI:def 1;
hence card NatMinor f = 1 by CARD_1:30
.= multnat $$ ({}.X, addnat[:](f,1)) by BINOP_2:10,SETWISEO:31;
end;
for B being Element of Fin X holds P[B] from SETWISEO:sch 2(A43,A2);
hence thesis by A1;
end;
registration
let X be set, f be finite-support Function of X, NAT;
cluster NatMinor f -> finite;
coherence
proof
per cases;
suppose
X is empty;
then NatMinor f c= Funcs({},NAT);
then NatMinor f c= {{}} by FUNCT_5:57;
hence thesis;
end;
suppose
X is not empty;
then reconsider X as non empty set;
reconsider f as finite-support Function of X, NAT;
card NatMinor f = multnat $$ (support f, addnat[:](f,1)) by Th61;
hence thesis;
end;
end;
end;
definition
let n be Ordinal, b be bag of n;
func divisors b -> FinSequence of Bags n means
:Def15:
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
proof
dom b = n & rng b c= NAT by PARTFUN1:def 2;
then reconsider f = b as finite-support Function of n, NAT by RELSET_1:4;
reconsider S = NatMinor f as non empty finite Subset of Bags n by Th60;
take IT = SgmX(BagOrder n, S);
take S;
thus IT = SgmX(BagOrder n, S);
let p be bag of n;
thus p in S implies p divides b
proof
assume p in S;
then for x being object st x in n holds p.x <= b.x by Def14;
hence thesis by Th45;
end;
assume p divides b;
then for x being set st x in n holds p.x <= b.x;
hence thesis by Def14;
end;
uniqueness
proof
let it1, it2 be FinSequence of Bags n;
given S1 being non empty finite Subset of Bags n such that
A1: it1 = SgmX(BagOrder n, S1) and
A2: for p being bag of n holds p in S1 iff p divides b;
given S2 being non empty finite Subset of Bags n such that
A3: it2 = SgmX(BagOrder n, S2) and
A4: for p being bag of n holds p in S2 iff p divides b;
for x being object holds x in S1 iff x in S2 by A2,A4;
hence thesis by A1,A3,TARSKI:2;
end;
end;
registration
let n be Ordinal, b be bag of n;
cluster divisors b -> non empty one-to-one;
coherence
proof
ex S being non empty finite Subset of Bags n st divisors b = SgmX(
BagOrder n, S) & for p being bag of n holds p in S iff p divides b by Def15;
hence thesis;
end;
end;
theorem Th62:
for n being Ordinal,i being Element of NAT, b being bag of n st
i in dom divisors b holds ((divisors b)/.i) qua Element of Bags n divides b
proof
let n be Ordinal,i be Element of NAT, b be bag of n;
assume i in dom divisors b;
then
A1: (divisors b)/.i = (divisors b).i & (divisors b).i in rng divisors b by
FUNCT_1:def 3,PARTFUN1:def 6;
reconsider pid = (divisors b)/.i as bag of n;
consider S being non empty finite Subset of Bags n such that
A2: divisors b = SgmX(BagOrder n, S) and
A3: for p being bag of n holds p in S iff p divides b by Def15;
BagOrder n linearly_orders S by Lm4,ORDERS_1:38;
then pid in S by A2,A1,Def2;
hence thesis by A3;
end;
theorem Th63:
for n being Ordinal, b being bag of n holds (divisors b)/.1 =
EmptyBag n & (divisors b)/.len divisors b = b
proof
let n be Ordinal, b be bag of n;
consider S being non empty finite Subset of Bags n such that
A1: divisors b = SgmX(BagOrder n, S) and
A2: for p being bag of n holds p in S iff p divides b by Def15;
A3: now
let y be Element of Bags n;
assume y in S;
then y divides b by A2;
then y <=' b by Th48;
hence [y,b] in BagOrder n by Def13;
end;
A4: now
let y be Element of Bags n;
assume y in S;
EmptyBag n <=' y by Th48,Th57;
hence [EmptyBag n, y] in BagOrder n by Def13;
end;
A5: BagOrder n linearly_orders S by Lm4,ORDERS_1:38;
EmptyBag n divides b;
then EmptyBag n in S by A2;
hence (divisors b)/.1 = EmptyBag n by A1,A5,A4,Th19;
b in S by A2;
hence thesis by A1,A5,A3,Th20;
end;
theorem Th64:
for n being Ordinal, i being Nat, 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
let n be Ordinal, i be Nat, b, b1, b2 be bag of n;
A1: 1 in dom divisors b & len divisors b in dom divisors b by FINSEQ_5:6;
A2: (divisors b)/.1 = EmptyBag n & (divisors b)/.len divisors b = b by Th63;
assume
A3: i > 1 & i < len divisors b;
then i in dom divisors b by FINSEQ_3:25;
hence thesis by A2,A1,A3,PARTFUN2:10;
end;
theorem Th65:
for n being Ordinal holds divisors EmptyBag n = <* EmptyBag n *>
proof
let n be Ordinal;
consider S being non empty finite Subset of Bags n such that
A1: divisors EmptyBag n = SgmX(BagOrder n, S) and
A2: for p being bag of n holds p in S iff p divides EmptyBag n by Def15;
A3: S c= { EmptyBag n}
proof
let x be object;
assume
A4: x in S;
then reconsider b = x as bag of n;
b divides EmptyBag n by A2,A4;
then b = EmptyBag n;
hence thesis by TARSKI:def 1;
end;
A5: BagOrder n linearly_orders S by Lm4,ORDERS_1:38;
EmptyBag n in S by A2;
then { EmptyBag n } c= S by ZFMISC_1:31;
then S = { EmptyBag n} by A3;
then
A6: rng divisors EmptyBag n = {EmptyBag n} by A1,A5,Def2;
len divisors EmptyBag n = card rng divisors EmptyBag n by Th18
.= 1 by A6,CARD_1:30;
hence thesis by A6,FINSEQ_1:39;
end;
definition
let n be Ordinal, b be bag of n;
func decomp b -> FinSequence of 2-tuples_on Bags n means
:Def16:
dom it = dom divisors b &
for i being Element of NAT, p being bag of n st i in dom it &
p = (divisors b)/.i holds it/.i = <*p, b-'p*>;
existence
proof
defpred P[Nat,set] means for p being bag of n st p = (divisors b)/.$1
holds $2 = <*p,b-'p*>;
A1: for k being Nat st k in Seg len divisors b ex d being Element of 2
-tuples_on Bags n st P[k,d]
proof
let k be Nat such that
k in Seg len divisors b;
reconsider p = (divisors b)/.k as bag of n;
reconsider b1=p, b2=b-'p as Element of Bags n by Def12;
len<*p,b-'p*> = 2 by FINSEQ_1:44;
then reconsider d = <*b1,b2*> as Element of 2-tuples_on Bags n by
FINSEQ_2:92;
take d;
thus thesis;
end;
consider f being FinSequence of 2-tuples_on Bags n such that
A2: len f = len divisors b and
A3: for n being Nat st n in Seg len divisors b holds P[n,f/.n] from
FINSEQ_4:sch 1(A1);
take f;
thus dom f = dom divisors b by A2,FINSEQ_3:29;
let i be Element of NAT, p be bag of n such that
A4: i in dom f and
A5: p = (divisors b)/.i;
i in Seg len divisors b by A2,A4,FINSEQ_1:def 3;
hence thesis by A3,A5;
end;
uniqueness
proof
let F,G be FinSequence of 2-tuples_on Bags n such that
A6: dom F = dom divisors b and
A7: for i being Element of NAT, p being bag of n st i in dom F & p = (
divisors b)/.i holds F/.i = <*p, b-'p*> and
A8: dom G = dom divisors b and
A9: for i being Element of NAT, p being bag of n st i in dom G & p =
(divisors b)/.i holds G/.i = <*p, b-'p*>;
now
let i be Nat;
reconsider p = (divisors b)/.i as bag of n;
assume
A10: i in dom F;
hence F/.i = <*p,b-'p*> by A7
.= G/.i by A6,A8,A9,A10;
end;
hence thesis by A6,A8,FINSEQ_5:12;
end;
end;
theorem Th66:
for n being Ordinal, i being Element of NAT, b being bag of n st
i in dom decomp b ex b1, b2 being bag of n st (decomp b)/.i = <*b1, b2*> & b =
b1+b2
proof
let n be Ordinal, i be Element of NAT, b be bag of n;
reconsider p = (divisors b)/.i as bag of n;
assume
A1: i in dom decomp b;
take p, b-'p;
thus (decomp b)/.i = <*p,b-'p*> by A1,Def16;
i in dom divisors b by A1,Def16;
hence thesis by Th46,Th62;
end;
theorem Th67:
for n being Ordinal, b, b1, b2 being bag of n st b = b1+b2 ex i
being Element of NAT st i in dom decomp b & (decomp b)/.i = <*b1, b2*>
proof
let n be Ordinal, b, b1, b2 be bag of n;
consider S being non empty finite Subset of Bags n such that
A1: divisors b = SgmX(BagOrder n, S) and
A2: for p being bag of n holds p in S iff p divides b by Def15;
A3: BagOrder n linearly_orders S by Lm4,ORDERS_1:38;
assume
A4: b = b1+b2;
then b1 divides b by Th49;
then b1 in S by A2;
then b1 in rng divisors b by A1,A3,Def2;
then consider i being Element of NAT such that
A5: i in dom divisors b and
A6: (divisors b)/.i= b1 by PARTFUN2:2;
take i;
thus i in dom decomp b by A5,Def16;
then (decomp b)/.i = <*b1, b-'b1*> by A6,Def16;
hence thesis by A4,Th47;
end;
theorem Th68:
for n being Ordinal, i being Element of NAT, b,b1,b2 being bag
of n st i in dom decomp b & (decomp b)/.i = <*b1, b2*> holds b1 = (divisors b)
/.i
proof
let n be Ordinal, i be Element of NAT, b,b1,b2 be bag of n;
reconsider p = (divisors b)/.i as bag of n;
assume i in dom decomp b & (decomp b)/.i = <*b1, b2*>;
then <*b1,b2*> = <*p,b-'p*> by Def16;
hence thesis by FINSEQ_1:77;
end;
registration
let n be Ordinal, b be bag of n;
cluster decomp b -> non empty one-to-one FinSequence-yielding;
coherence
proof
A1: dom divisors b = dom decomp b by Def16;
hence decomp b is non empty;
now
let k,m be Element of NAT;
assume
A2: k in dom decomp b;
assume
A3: m in dom decomp b;
then consider bm1, bm2 being bag of n such that
A4: (decomp b)/.m = <*bm1, bm2*> and
b = bm1+bm2 by Th66;
assume (decomp b)/.k = (decomp b)/.m;
then (divisors b)/.k = bm1 by A2,A4,Th68
.= (divisors b)/.m by A3,A4,Th68;
hence k = m by A1,A2,A3,PARTFUN2:10;
end;
hence decomp b is one-to-one by PARTFUN2:9;
let x be object;
assume x in dom decomp b;
thus thesis;
end;
end;
registration
let n be Ordinal, b be Element of Bags n;
cluster decomp b -> non empty one-to-one FinSequence-yielding;
coherence;
end;
theorem
for n being Ordinal, b being bag of n holds (decomp b)/.1 = <*
EmptyBag n, b*> & (decomp b)/.len decomp b = <*b, EmptyBag n*>
proof
let n be Ordinal, b be bag of n;
reconsider p = (divisors b)/.1 as bag of n;
p = EmptyBag n & 1 in dom decomp b by Th63,FINSEQ_5:6;
hence (decomp b)/.1 = <*EmptyBag n, b-'EmptyBag n*> by Def16
.= <*EmptyBag n, b*> by Th52;
reconsider p = (divisors b)/.len decomp b as bag of n;
dom decomp b = dom divisors b by Def16;
then len decomp b = len divisors b by FINSEQ_3:29;
then
A1: p = b by Th63;
len decomp b in dom decomp b by FINSEQ_5:6;
hence (decomp b)/.len decomp b = <*b,b-'b*> by A1,Def16
.= <*b, EmptyBag n*> by Th54;
end;
theorem
for n being Ordinal, i being Nat, 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
let n be Ordinal, i be Nat, b, b1, b2 be bag of n such that
A1: i > 1 & i < len decomp b and
A2: (decomp b)/.i = <*b1, b2*>;
reconsider p = (divisors b)/.i as bag of n;
A3: i in dom decomp b by A1,FINSEQ_3:25;
then
A4: (decomp b)/.i = <*p,b-'p*> by Def16;
then
A5: b2 = b-'p by A2,FINSEQ_1:77;
A6: dom decomp b = dom divisors b by Def16;
then
A7: len decomp b = len divisors b by FINSEQ_3:29;
b1 = p by A2,A4,FINSEQ_1:77;
hence b1 <> EmptyBag n by A1,A7,Th64;
assume b2 = EmptyBag n;
then p = b by A6,A3,A5,Th55,Th62;
hence contradiction by A1,A7,Th64;
end;
theorem
for n being Ordinal holds decomp EmptyBag n = <* <*EmptyBag n,
EmptyBag n*> *>
proof
let n be Ordinal;
len<*EmptyBag n, EmptyBag n*> = 2 by FINSEQ_1:44;
then reconsider
E = <*EmptyBag n, EmptyBag n*> as Element of 2-tuples_on Bags n
by FINSEQ_2:92;
reconsider e = <* E *> as FinSequence of 2-tuples_on Bags n;
A1: dom e = Seg 1 by FINSEQ_1:38;
A2: <* EmptyBag n *> = divisors EmptyBag n by Th65;
A3: for i being Element of NAT, p being bag of n st i in dom e & p = (
divisors EmptyBag n)/.i holds e/.i = <*p, (EmptyBag n)-'p*>
proof
let i be Element of NAT, p be bag of n such that
A4: i in dom e and
A5: p = (divisors EmptyBag n)/.i;
A6: i = 1 by A1,A4,FINSEQ_1:2,TARSKI:def 1;
then
A7: (divisors EmptyBag n)/.i = EmptyBag n by A2,FINSEQ_4:16;
thus e/.i = E by A6,FINSEQ_4:16
.= <*p, (EmptyBag n)-'p*> by A5,A7,Th52;
end;
dom e = dom divisors EmptyBag n by A2,A1,FINSEQ_1:38;
hence thesis by A3,Def16;
end;
theorem
for n being Ordinal, b being bag of n, 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
qua Element of 2-tuples_on Bags n)/.1) qua Element
of Bags n))) ^^ ((len (decomp
((((decomp b)/.k qua Element of 2-tuples_on Bags n)/.1)
qua Element of Bags n)))
|-> <*(((decomp b)/.k qua Element of 2-tuples_on Bags n)/.2)*>)) &
(for k being Nat st k in dom g holds g.k = ((
len (decomp ((((decomp b)/.k qua Element of 2-tuples_on Bags n)/.2)
qua Element of Bags n)))
|-> <*((decomp b)/.k qua Element of 2-tuples_on Bags n)/.1*>)
^^ (decomp ((((decomp b)/.k qua Element of 2-tuples_on Bags n)/.2)
qua Element of Bags n))) ex p being
Permutation of dom FlattenSeq f st FlattenSeq g = (FlattenSeq f)*p
proof
let n be Ordinal, b be bag of n, f, g be FinSequence of (3-tuples_on Bags n)
* such that
A1: dom f = dom decomp b and
A2: dom g = dom decomp b and
A3: for k being Nat st k in dom f holds f.k
= ((decomp ((((decomp b)/.k qua Element of 2-tuples_on Bags n)
/.1) qua Element of Bags n))) ^^
((len (decomp ((((decomp b)/.k qua Element of 2-tuples_on Bags n)/.1) qua
Element of Bags n))) |->
<*(((decomp b)/.k qua Element of 2-tuples_on Bags n)/.2)*>) and
A4: for k being Nat st k in dom g holds g.k = ((len (decomp ((((decomp b
)/.k qua Element of 2-tuples_on Bags n)/.2) qua Element of Bags n)))
|-> <*(((decomp b)/.k qua Element of 2-tuples_on Bags n)/.1)*>)
^^ (decomp (((
(decomp b)/.k qua Element of 2-tuples_on Bags n)/.2)
qua Element of Bags n));
set Ff = FlattenSeq f, Fg = FlattenSeq g, db = decomp b;
A5: Fg is one-to-one
proof
let k1, k2 be object such that
A6: k1 in dom Fg and
A7: k2 in dom Fg and
A8: Fg.k1 = Fg.k2;
consider i1, j1 being Nat such that
A9: i1 in dom g and
A10: j1 in dom (g.i1) and
A11: k1 = (Sum Card (g|(i1-'1))) + j1 and
A12: (g.i1).j1 = Fg.k1 by A6,Th28;
reconsider dbi1 = db/.i1 as Element of 2-tuples_on Bags n;
set ddbi11 = decomp ((dbi1/.2) qua Element of Bags n);
A13: g.i1 = ((len ddbi11) |-> <*dbi1/.1*>)^^ddbi11 by A4,A9;
then
A14: dom (g.i1) = dom ddbi11 /\ dom ((len ddbi11) |-> <*dbi1/.1*>) by Def4
.= dom ddbi11 /\ Seg len ddbi11
.= dom ddbi11 /\ dom ddbi11 by FINSEQ_1:def 3
.= dom ddbi11;
then
A15: ddbi11/.j1 = ddbi11.j1 by A10,PARTFUN1:def 6;
dom ddbi11 = Seg len ddbi11 by FINSEQ_1:def 3;
then
A16: ((len ddbi11) |-> <*dbi1/.1*>).j1 = <*dbi1/.1*> by A10,A14,FUNCOP_1:7;
consider b11, b12 being bag of n such that
A17: db/.i1 = <*b11,b12*> and
b = b11+b12 by A2,A9,Th66;
reconsider b119 = b11, b129 = b12 as Element of Bags n by Def12;
A18: b119 = b11 & b129 = b12;
then dbi1/.2 = b12 by A17,FINSEQ_4:17;
then consider b111, b112 being bag of n such that
A19: ddbi11/.j1 = <*b111, b112*> and
A20: b12 = b111+b112 by A10,A14,Th66;
dbi1/.1 = b11 by A17,A18,FINSEQ_4:17;
then
A21: (g.i1).j1 = <*b11*>^<*b111,b112*> by A10,A13,A19,A15,A16,Def4
.= <*b11,b111,b112*> by FINSEQ_1:43;
consider i2, j2 being Nat such that
A22: i2 in dom g and
A23: j2 in dom (g.i2) and
A24: k2 = (Sum Card (g|(i2-'1))) + j2 and
A25: (g.i2).j2 = Fg.k2 by A7,Th28;
reconsider dbi2 = db/.i2 as Element of 2-tuples_on Bags n;
set ddbi21 = decomp ((dbi2/.2) qua Element of Bags n);
A26: g.i2 = ((len ddbi21) |-> <*dbi2/.1*>) ^^ ddbi21 by A4,A22;
then
A27: dom (g.i2) = dom ddbi21 /\ dom ((len ddbi21) |-> <*dbi2/.1*>) by Def4
.= dom ddbi21 /\ Seg len ddbi21
.= dom ddbi21 /\ dom ddbi21 by FINSEQ_1:def 3
.= dom ddbi21;
then
A28: ddbi21/.j2 = ddbi21.j2 by A23,PARTFUN1:def 6;
dom ddbi21 = Seg len ddbi21 by FINSEQ_1:def 3;
then
A29: ((len ddbi21) |-> <*dbi2/.1*>).j2 = <*dbi2/.1*> by A23,A27,FUNCOP_1:7;
consider b21, b22 being bag of n such that
A30: db/.i2 = <*b21,b22*> and
b = b21+b22 by A2,A22,Th66;
reconsider b219 = b21, b229 = b22 as Element of Bags n by Def12;
A31: b219 = b21 & b229 = b22;
then dbi2/.2 = b22 by A30,FINSEQ_4:17;
then consider b211, b212 being bag of n such that
A32: ddbi21/.j2 = <*b211, b212*> and
A33: b22 = b211+b212 by A23,A27,Th66;
dbi2/.1 = b21 by A30,A31,FINSEQ_4:17;
then
A34: (g.i2).j2 = <*b21*>^<*b211,b212*> by A23,A26,A32,A28,A29,Def4
.= <*b21,b211, b212*> by FINSEQ_1:43;
then
A35: b111 = b211 & b112 = b212 by A8,A12,A25,A21,FINSEQ_1:78;
A36: db/.i2 = db.i2 by A2,A22,PARTFUN1:def 6;
A37: db/.i1 = db.i1 by A2,A9,PARTFUN1:def 6;
b11 = b21 by A8,A12,A25,A21,A34,FINSEQ_1:78;
then i1 = i2 by A2,A9,A22,A37,A17,A20,A36,A30,A33,A35,FUNCT_1:def 4;
hence thesis by A10,A11,A23,A24,A19,A15,A27,A32,A28,A35,FUNCT_1:def 4;
end;
now
let y be object;
hereby
assume y in rng Ff;
then consider k being object such that
A38: k in dom Ff and
A39: y = Ff.k by FUNCT_1:def 3;
reconsider k as Element of NAT by A38;
consider i, j being Nat such that
A40: i in dom f and
A41: j in dom (f.i) and
k = (Sum Card (f|(i-'1))) + j and
A42: (f.i).j = Ff.k by A38,Th28;
reconsider dbi = db/.i as Element of 2-tuples_on Bags n;
set ddbi1 = decomp ((dbi/.1) qua Element of Bags n);
A43: f.i = ddbi1 ^^ ((len ddbi1) |-> <*dbi/.2*>) by A3,A40;
then
A44: dom (f.i) = dom ddbi1 /\ dom ((len ddbi1) |-> <*dbi/.2*>) by Def4
.= dom ddbi1 /\ Seg len ddbi1
.= dom ddbi1 /\ dom ddbi1 by FINSEQ_1:def 3
.= dom ddbi1;
dom ddbi1 = Seg len ddbi1 by FINSEQ_1:def 3;
then
A45: ((len ddbi1) |-> <*dbi/.2*>).j = <*dbi/.2*> by A41,A44,FUNCOP_1:7;
consider b1, b2 being bag of n such that
A46: db/.i = <*b1,b2*> and
A47: b = b1+b2 by A1,A40,Th66;
reconsider b19 = b1, b29 = b2 as Element of Bags n by Def12;
A48: b19 = b1 & b29 = b2;
then
A49: dbi/.2 = b2 by A46,FINSEQ_4:17;
dbi/.1 = b1 by A46,A48,FINSEQ_4:17;
then consider b11, b12 being bag of n such that
A50: ddbi1/.j = <*b11, b12*> and
A51: b1 = b11+b12 by A41,A44,Th66;
b = b11+(b12+b2) by A47,A51,Th34;
then consider i9 being Element of NAT such that
A52: i9 in dom decomp b and
A53: (decomp b)/.i9 = <*b11, b12+b2*> by Th67;
set b3 = b12+b2;
reconsider b119 = b11, b39 = b3 as Element of Bags n by Def12;
consider j9 being Element of NAT such that
A54: j9 in dom decomp b3 and
A55: (decomp b3)/.j9 = <*b12, b2*> by Th67;
reconsider dbi9 = (decomp b)/.i9 as Element of 2-tuples_on Bags n;
set ddbi92 = decomp ((dbi9/.2) qua Element of Bags n);
A56: (decomp b)/.i9 = <*b119, b39*> by A53;
then
A57: dbi9/.1 = b11 & ddbi92 = decomp b3 by FINSEQ_4:17;
A58: g.i9 = ((len ddbi92) |-> <*dbi9/.1*>) ^^ ddbi92 by A2,A4,A52;
then
A59: dom (g.i9) = dom ((len ddbi92) |-> <*dbi9/.1*>) /\ dom
ddbi92 by Def4
.= Seg len ddbi92 /\ dom ddbi92
.= dom ddbi92 /\ dom ddbi92 by FINSEQ_1:def 3
.= dom ddbi92;
then
A60: j9 in dom (g.i9) by A54,A56,FINSEQ_4:17;
then
A61: j9 in Seg len ddbi92 by A59,FINSEQ_1:def 3;
A62: (decomp b3)/.j9 = (decomp b3).j9 by A54,PARTFUN1:def 6;
set m = (Sum Card (g|(i9-'1))) + j9;
A63: m in dom Fg & Fg.m = (g.i9).j9 by A2,A52,A60,Th29;
A64: (g.i9).j9 = (((len ddbi92) |-> <*dbi9/.1*>)).j9 ^ (
ddbi92).j9 by A58,A60,Def4
.= <*b11*>^<*b12,b2*> by A55,A57,A61,A62,FUNCOP_1:7
.= <*b11,b12,b2*> by FINSEQ_1:43;
ddbi1/.j = ddbi1.j by A41,A44,PARTFUN1:def 6;
then (f.i).j = <*b11,b12*>^<*b2*> by A41,A43,A49,A50,A45,Def4
.= <*b11,b12,b2*> by FINSEQ_1:43;
hence y in rng Fg by A39,A42,A64,A63,FUNCT_1:def 3;
end;
assume y in rng Fg;
then consider k being object such that
A65: k in dom Fg and
A66: y = Fg.k by FUNCT_1:def 3;
reconsider k as Element of NAT by A65;
consider i, j being Nat such that
A67: i in dom g and
A68: j in dom (g.i) and
k = (Sum Card (g|(i-'1))) + j and
A69: (g.i).j = Fg.k by A65,Th28;
reconsider dbi = db/.i as Element of 2-tuples_on Bags n;
set ddbi1 = decomp ((dbi/.2) qua Element of Bags n);
A70: g.i = ((len ddbi1) |-> <*dbi/.1*>) ^^ ddbi1 by A4,A67;
then
A71: dom (g.i) = dom ddbi1 /\ dom ((len ddbi1) |-> <*dbi/.1*>) by Def4
.= dom ddbi1 /\ Seg len ddbi1
.= dom ddbi1 /\ dom ddbi1 by FINSEQ_1:def 3
.= dom ddbi1;
dom ddbi1 = Seg len ddbi1 by FINSEQ_1:def 3;
then
A72: ((len ddbi1) |-> <*dbi/.1*>).j = <*dbi/.1*> by A68,A71,FUNCOP_1:7;
consider b1, b2 being bag of n such that
A73: db/.i = <*b1,b2*> and
A74: b = b1+b2 by A2,A67,Th66;
reconsider b19 = b1, b29 = b2 as Element of Bags n by Def12;
A75: b19 = b1 & b29 = b2;
then
A76: dbi/.1 = b1 by A73,FINSEQ_4:17;
dbi/.2 = b2 by A73,A75,FINSEQ_4:17;
then consider b11, b12 being bag of n such that
A77: ddbi1/.j = <*b11, b12*> and
A78: b2 = b11+b12 by A68,A71,Th66;
ddbi1/.j = ddbi1.j by A68,A71,PARTFUN1:def 6;
then
A79: (g.i).j = <*b1*>^<*b11,b12*> by A68,A70,A76,A77,A72,Def4
.= <*b1,b11,b12*> by FINSEQ_1:43;
set b3 = b1+b11;
reconsider b39 = b3, b129 = b12 as Element of Bags n by Def12;
consider j9 being Element of NAT such that
A80: j9 in dom decomp b3 and
A81: (decomp b3)/.j9 = <*b1, b11*> by Th67;
A82: (decomp b3)/.j9 = (decomp b3).j9 by A80,PARTFUN1:def 6;
b = b1+b11+b12 by A74,A78,Th34;
then consider i9 being Element of NAT such that
A83: i9 in dom decomp b and
A84: (decomp b)/.i9 = <*b1+b11, b12*> by Th67;
reconsider dbi9 = (decomp b)/.i9 as Element of 2-tuples_on Bags n;
set ddbi92 = decomp ((dbi9/.1) qua Element of Bags n);
set m = (Sum Card (f|(i9-'1))) + j9;
A85: (decomp b)/.i9 = <*b39, b129*> by A84;
then
A86: dbi9/.1 = b3 by FINSEQ_4:17;
then
A87: j9 in Seg len ddbi92 by A80,FINSEQ_1:def 3;
A88: f.i9 = ddbi92 ^^ ((len ddbi92) |-> <*dbi9/.2*>) by A1,A3,A83;
then
A89: dom (f.i9) = dom ((len ddbi92) |-> <*dbi9/.2*>) /\ dom
ddbi92 by Def4
.= Seg len ddbi92 /\ dom ddbi92
.= dom ddbi92 /\ dom ddbi92 by FINSEQ_1:def 3
.= dom ddbi92;
then
A90: m in dom Ff & Ff.m = (f.i9).j9 by A1,A83,A80,A86,Th29;
A91: dbi9/.2 = b12 by A85,FINSEQ_4:17;
(f.i9).j9 = (ddbi92).j9 ^ (((len ddbi92) |-> <*dbi9/.2*>)
).j9 by A80,A88,A86,A89,Def4
.= <*b1,b11*>^<*b12*> by A81,A91,A86,A87,A82,FUNCOP_1:7
.= <*b1,b11,b12*> by FINSEQ_1:43;
hence y in rng Ff by A66,A69,A79,A90,FUNCT_1:def 3;
end;
then
A92: rng Ff = rng Fg by TARSKI:2;
Ff is one-to-one
proof
let k1, k2 be object such that
A93: k1 in dom Ff and
A94: k2 in dom Ff and
A95: Ff.k1 = Ff.k2;
consider i1, j1 being Nat such that
A96: i1 in dom f and
A97: j1 in dom (f.i1) and
A98: k1 = (Sum Card (f|(i1-'1))) + j1 and
A99: (f.i1).j1 = Ff.k1 by A93,Th28;
reconsider dbi1 = db/.i1 as Element of 2-tuples_on Bags n;
set ddbi11 = decomp ((dbi1/.1) qua Element of Bags n);
A100: f.i1 = ddbi11 ^^ ((len ddbi11) |-> <*dbi1/.2*>) by A3,A96;
then
A101: dom (f.i1) = dom ddbi11 /\ dom ((len ddbi11) |-> <*dbi1/.2*>) by Def4
.= dom ddbi11 /\ Seg len ddbi11
.= dom ddbi11 /\ dom ddbi11 by FINSEQ_1:def 3
.= dom ddbi11;
then
A102: ddbi11/.j1 = ddbi11.j1 by A97,PARTFUN1:def 6;
dom ddbi11 = Seg len ddbi11 by FINSEQ_1:def 3;
then
A103: ((len ddbi11) |-> <*dbi1/.2*>).j1 = <*dbi1/.2*> by A97,A101,FUNCOP_1:7;
consider b11, b12 being bag of n such that
A104: db/.i1 = <*b11,b12*> and
b = b11+b12 by A1,A96,Th66;
reconsider b119 = b11, b129 = b12 as Element of Bags n by Def12;
A105: b119 = b11 & b129 = b12;
then dbi1/.1 = b11 by A104,FINSEQ_4:17;
then consider b111, b112 being bag of n such that
A106: ddbi11/.j1 = <*b111, b112*> and
A107: b11 = b111+b112 by A97,A101,Th66;
dbi1/.2 = b12 by A104,A105,FINSEQ_4:17;
then
A108: (f.i1).j1 = <*b111,b112*>^<*b12*> by A97,A100,A106,A102,A103,Def4
.= <*b111,b112,b12*> by FINSEQ_1:43;
consider i2, j2 being Nat such that
A109: i2 in dom f and
A110: j2 in dom (f.i2) and
A111: k2 = (Sum Card (f|(i2-'1))) + j2 and
A112: (f.i2).j2 = Ff.k2 by A94,Th28;
reconsider dbi2 = db/.i2 as Element of 2-tuples_on Bags n;
set ddbi21 = decomp ((dbi2/.1) qua Element of Bags n);
A113: f.i2 = ddbi21 ^^ ((len ddbi21) |-> <*dbi2/.2*>) by A3,A109;
then
A114: dom (f.i2) = dom ddbi21 /\ dom ((len ddbi21) |-> <*dbi2/.2*>) by Def4
.= dom ddbi21 /\ Seg len ddbi21
.= dom ddbi21 /\ dom ddbi21 by FINSEQ_1:def 3
.= dom ddbi21;
then
A115: ddbi21/.j2 = ddbi21.j2 by A110,PARTFUN1:def 6;
dom ddbi21 = Seg len ddbi21 by FINSEQ_1:def 3;
then
A116: ((len ddbi21) |-> <*dbi2/.2*>).j2 = <*dbi2/.2*> by A110,A114,FUNCOP_1:7;
consider b21, b22 being bag of n such that
A117: db/.i2 = <*b21,b22*> and
b = b21+b22 by A1,A109,Th66;
reconsider b219 = b21, b229 = b22 as Element of Bags n by Def12;
A118: b219 = b21 & b229 = b22;
then dbi2/.1 = b21 by A117,FINSEQ_4:17;
then consider b211, b212 being bag of n such that
A119: ddbi21/.j2 = <*b211, b212*> and
A120: b21 = b211+b212 by A110,A114,Th66;
dbi2/.2 = b22 by A117,A118,FINSEQ_4:17;
then
A121: (f.i2).j2 = <*b211,b212*>^<*b22*> by A110,A113,A119,A115,A116,Def4
.= <*b211,b212,b22*> by FINSEQ_1:43;
then
A122: b111 = b211 & b112 = b212 by A95,A99,A112,A108,FINSEQ_1:78;
A123: db/.i2 = db.i2 by A1,A109,PARTFUN1:def 6;
A124: db/.i1 = db.i1 by A1,A96,PARTFUN1:def 6;
b12 = b22 by A95,A99,A112,A108,A121,FINSEQ_1:78;
then i1 = i2 by A1,A96,A109,A124,A104,A107,A123,A117,A120,A122,
FUNCT_1:def 4;
hence thesis by A97,A98,A110,A111,A106,A102,A114,A119,A115,A122,
FUNCT_1:def 4;
end;
then Ff, Fg are_fiberwise_equipotent by A92,A5,RFINSEQ:26;
hence thesis by RFINSEQ:4;
end;
theorem
for X being set, b1, b2 being real-valued ManySortedSet of X holds
support (b1+b2) c= support b1 \/ support b2
proof
let X be set, b1, b2 be real-valued ManySortedSet of X;
let x be object;
assume x in support (b1+b2);
then
A1: (b1+b2).x <> 0 by Def7;
assume
A2: not x in support b1 \/ support b2;
then not x in support b1 by XBOOLE_0:def 3;
then
A3: b1.x = 0 by Def7;
not x in support b2 by A2,XBOOLE_0:def 3;
then b1.x+b2.x = 0 by A3,Def7;
hence contradiction by A1,Def5;
end;
registration
let D be non empty set;
let n be Nat;
cluster -> FinSequence-yielding for FinSequence of n-tuples_on D;
coherence;
end;
registration let k be Nat;
let D be non empty set, M be FinSequence of k-tuples_on D;
let x be set;
cluster M/.x -> Function-like Relation-like;
coherence;
end;
registration let k be Element of NAT;
let D be non empty set, M be FinSequence of k-tuples_on D;
let x be set;
cluster M/.x -> D-valued FinSequence-like;
coherence;
end;
begin :: from POLYNOM2, 2012.02.16, A.T.
theorem
for X being set, A being empty Subset of X, R being Order of X st
R linearly_orders A holds SgmX(R,A) = {}
proof
let X be set, A be empty Subset of X, R be Order of X;
assume R linearly_orders A;
then rng SgmX(R,A) = {} by Def2;
hence thesis;
end;
theorem Th75:
for X being set, A being finite Subset of X, R be Order of X st
R linearly_orders A for i,j being Element of NAT st i in dom(SgmX(R,A)) & j in
dom(SgmX(R,A)) holds SgmX(R,A)/.i = SgmX(R,A)/.j implies i = j
proof
let X be set, A be finite Subset of X, R be Order of X;
assume
A1: R linearly_orders A;
let i,j be Element of NAT such that
A2: i in dom(SgmX(R,A)) and
A3: j in dom(SgmX(R,A)) and
A4: SgmX(R,A)/.i = SgmX(R,A)/.j;
assume i <> j;
then i < j or j < i by XXREAL_0:1;
hence thesis by A1,A2,A3,A4,Def2;
end;
Lm5: for D being set, p being FinSequence of D st dom p <> {} holds 1 in dom p
proof
let D be set, p be FinSequence of D;
assume dom p <> {};
then p <> {};
hence thesis by FINSEQ_5:6;
end;
Lm6: for X being set, A being finite Subset of X, a being Element of X, R
being Order of X st R linearly_orders {a} \/ A holds R linearly_orders A
proof
let X be set, A be finite Subset of X, a be Element of X, R be Order of X;
for x being object holds x in A implies x in {a} \/ A by XBOOLE_0:def 3;
then
A1: A c= {a} \/ A;
assume R linearly_orders {a} \/ A;
hence thesis by A1,ORDERS_1:38;
end;
theorem Th76:
for X being set, A being finite Subset of X, a being Element of
X st not a in A for B being finite Subset of X st B = {a} \/ A for R being
Order of X st R linearly_orders B for k being Element of NAT st k in dom(SgmX(R
,B)) & SgmX(R,B)/.k = a for i being Element of NAT st 1 <= i & i <= k - 1 holds
SgmX(R,B)/.i = SgmX(R,A)/.i
proof
let X be set, A be finite Subset of X, a be Element of X;
assume
A1: not a in A;
let B be finite Subset of X;
assume
A2: B = {a} \/ A;
let R be Order of X;
assume
A3: R linearly_orders B;
then
A4: R linearly_orders A by A2,Lm6;
field R = X by ORDERS_1:12;
then
A5: R is_antisymmetric_in X by RELAT_2:def 12;
set sgb = SgmX(R,B), sga = SgmX(R,A);
consider lensga being Nat such that
A6: dom sga = Seg lensga by FINSEQ_1:def 2;
consider lensgb being Nat such that
A7: dom sgb = Seg lensgb by FINSEQ_1:def 2;
reconsider lensga,lensgb as Element of NAT by ORDINAL1:def 12;
lensgb = len sgb by A7,FINSEQ_1:def 3
.= card B by A3,Th10
.= card A + 1 by A1,A2,CARD_2:41
.= len sga + 1 by A2,A3,Lm6,Th10
.= lensga + 1 by A6,FINSEQ_1:def 3;
then
A8: lensga <= lensgb by NAT_1:11;
defpred P[Nat] means sgb/.($1) = sga/.($1);
let k be Element of NAT;
assume that
A9: k in dom(SgmX(R,B)) and
A10: SgmX(R,B)/.k = a;
k in Seg(len(sgb)) by A9,FINSEQ_1:def 3;
then
A11: 1 <= k by FINSEQ_1:1;
then 1 - 1 <= k - 1 by XREAL_1:9;
then reconsider k9 = k - 1 as Element of NAT by INT_1:3;
A12: k - 1 + 1 = k + (0 qua Nat);
A13: for j being Element of NAT st 1 <= j & j < k9 holds (for j9 being
Element of NAT st 1 <= j9 & j9 <= j holds P[j9]) implies P[j+1]
proof
let i9 be Element of NAT;
assume that
A14: 1 <= i9 and
A15: i9 < k9;
A16: 1 <= i9 + 1 by A14,XREAL_1:29;
A17: i9 + 1 < k by A12,A15,XREAL_1:6;
then
A18: i9 + 1 in dom sgb by A9,A16,FINSEQ_3:156;
sgb/.(i9+1) = sgb.(i9+1) by A9,A17,A16,FINSEQ_3:156,PARTFUN1:def 6;
then sgb/.(i9+1) in rng sgb by A18,FUNCT_1:def 3;
then
A19: sgb/.(i9+1) in B by A3,Def2;
sgb/.(i9+1) <> a by A3,A9,A10,A17,A18,Def2;
then not sgb/.(i9+1) in {a} by TARSKI:def 1;
then sgb/.(i9+1) in A by A2,A19,XBOOLE_0:def 3;
then sgb/.(i9+1) in rng sga by A4,Def2;
then consider l being object such that
A20: l in dom sga and
A21: sga.l = sgb/.(i9+1) by FUNCT_1:def 3;
reconsider l as Element of NAT by A20;
A22: 1 <= l by A6,A20,FINSEQ_1:1;
l <= lensga by A6,A20,FINSEQ_1:1;
then l <= lensgb by A8,XXREAL_0:2;
then
A23: l in dom sgb by A7,A22,FINSEQ_1:1;
assume
A24: for j9 being Element of NAT st 1 <= j9 & j9 <= i9 holds P[j9];
assume
A25: sgb/.(i9+1) <> sga/.(i9+1);
then
A26: l <> i9 + 1 by A20,A21,PARTFUN1:def 6;
per cases;
suppose
l < i9 + 1;
then l <= i9 by NAT_1:13;
then sgb/.l = sga/.l by A24,A22
.= sgb/.(i9+1) by A20,A21,PARTFUN1:def 6;
hence thesis by A3,A18,A26,A23,Th75;
end;
suppose
A27: i9 + 1 <= l;
then
A28: i9 + 1 in dom sga by A16,A20,FINSEQ_3:156;
sga/.(i9+1) = sga.(i9+1) by A16,A20,A27,FINSEQ_3:156,PARTFUN1:def 6;
then sga/.(i9+1) in rng sga by A28,FUNCT_1:def 3;
then sga/.(i9+1) in A by A4,Def2;
then sga/.(i9+1) in B by A2,XBOOLE_0:def 3;
then sga/.(i9+1) in rng sgb by A3,Def2;
then consider l9 being object such that
A29: l9 in dom sgb and
A30: sgb.l9 = sga/.(i9+1) by FUNCT_1:def 3;
reconsider l9 as Element of NAT by A29;
i9 + 1 < l by A26,A27,XXREAL_0:1;
then [sga/.(i9+1),sga/.l] in R by A4,A20,A28,Def2;
then [sgb/.l9,sga/.l] in R by A29,A30,PARTFUN1:def 6;
then
A31: [sgb/.l9,sgb/.(i9+1)] in R by A20,A21,PARTFUN1:def 6;
sgb/.l9 = sgb.l9 by A29,PARTFUN1:def 6;
then sgb/.l9 in rng sgb by A29,FUNCT_1:def 3;
then
A32: sgb/.l9 in B by A3,Def2;
A33: 1 <= l9 by A7,A29,FINSEQ_1:1;
A34: i9 + 1 < l9
proof
assume
A35: l9 <= i9 + 1;
now
per cases by A35,XXREAL_0:1;
case
l9 = i9 + 1;
hence thesis by A25,A29,A30,PARTFUN1:def 6;
end;
case
A36: l9 < i9 + 1;
then l9 <= i9 by NAT_1:13;
then
A37: sga/.l9 = sgb/.l9 by A24,A33
.= sga/.(i9+1) by A29,A30,PARTFUN1:def 6;
l9 in dom sga by A28,A33,A36,FINSEQ_3:156;
hence thesis by A2,A3,A28,A36,A37,Lm6,Th75;
end;
end;
hence thesis;
end;
then [sgb/.(i9+1),sgb/.l9] in R by A3,A18,A29,Def2;
then sgb/.l9 = sgb/.(i9+1) by A5,A31,A32;
hence thesis by A3,A18,A29,A34,Th75;
end;
end;
let i be Element of NAT;
assume that
A38: 1 <= i and
A39: i <= k - 1;
A40: 1 in dom sgb by A9,Lm5;
A41: P[1]
proof
sgb/.1 = sgb.1 by A9,Lm5,PARTFUN1:def 6;
then sgb/.1 in rng sgb by A40,FUNCT_1:def 3;
then
A42: sgb/.1 in B by A3,Def2;
k <> 1 by A38,A39,XXREAL_0:2;
then 1 < k by A11,XXREAL_0:1;
then sgb/.1 <> a by A3,A9,A10,A40,Def2;
then not sgb/.1 in {a} by TARSKI:def 1;
then sgb/.1 in A by A2,A42,XBOOLE_0:def 3;
then sgb/.1 in rng sga by A4,Def2;
then consider l being object such that
A43: l in dom sga and
A44: sga.l = sgb/.1 by FUNCT_1:def 3;
A45: sga/.1 = sga.1 by A43,Lm5,PARTFUN1:def 6;
assume
A46: sgb/.1 <> sga/.1;
reconsider l as Element of NAT by A43;
A47: 1 in dom sga by A43,Lm5;
1 <= l by A6,A43,FINSEQ_1:1;
then 1 < l by A46,A44,A45,XXREAL_0:1;
then [sga/.1,sga/.l] in R by A4,A43,A47,Def2;
then
A48: [sga/.1,sgb/.1] in R by A43,A44,PARTFUN1:def 6;
not sga/.1 in B
proof
A49: sgb/.1 = sgb.1 by A9,Lm5,PARTFUN1:def 6;
assume sga/.1 in B;
then sga/.1 in rng sgb by A3,Def2;
then consider l9 being object such that
A50: l9 in dom sgb and
A51: sgb.l9 = sga/.1 by FUNCT_1:def 3;
reconsider l9 as Element of NAT by A50;
1 <= l9 by A7,A50,FINSEQ_1:1;
then 1 < l9 by A46,A51,A49,XXREAL_0:1;
then [sgb/.1,sgb/.l9] in R by A3,A40,A50,Def2;
then [sgb/.1,sga/.1] in R by A50,A51,PARTFUN1:def 6;
hence thesis by A5,A46,A42,A48;
end;
then
A52: not(sga/.1) in A by A2,XBOOLE_0:def 3;
sga/.1 in rng sga by A47,A45,FUNCT_1:def 3;
hence thesis by A4,A52,Def2;
end;
for j being Element of NAT st 1 <= j & j <= k9 holds P[j] from INT_1:sch 8
(A41,A13);
hence thesis by A38,A39;
end;
theorem Th77:
for X being set, A being finite Subset of X, a being Element of
X st not a in A for B being finite Subset of X st B = {a} \/ A for R being
Order of X st R linearly_orders B for k being Element of NAT st k in dom(SgmX(R
,B)) & SgmX(R,B)/.k = a 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
let X be set, A be finite Subset of X, a be Element of X;
assume
A1: not a in A;
let B be finite Subset of X;
assume
A2: B = {a} \/ A;
let R be Order of X;
assume
A3: R linearly_orders B;
then
A4: R linearly_orders A by A2,Lm6;
field R = X by ORDERS_1:12;
then
A5: R is_antisymmetric_in X by RELAT_2:def 12;
set sgb = SgmX(R,B), sga = SgmX(R,A);
consider lensga being Nat such that
A6: dom sga = Seg lensga by FINSEQ_1:def 2;
defpred P[Nat] means sgb/.($1 + 1) = sga/.($1);
consider lensgb being Nat such that
A7: dom sgb = Seg lensgb by FINSEQ_1:def 2;
let k be Element of NAT;
assume that
A8: k in dom(SgmX(R,B)) and
A9: SgmX(R,B)/.k = a;
k in Seg(len(sgb)) by A8,FINSEQ_1:def 3;
then
A10: 1 <= k by FINSEQ_1:1;
then 1 - 1 <= k - 1 by XREAL_1:9;
then reconsider k9 = k - 1 as Element of NAT by INT_1:3;
reconsider lensga,lensgb as Element of NAT by ORDINAL1:def 12;
A11: k9 + 1 = k + (0 qua Nat);
A12: lensgb = len sgb by A7,FINSEQ_1:def 3
.= card B by A3,Th10
.= card A + 1 by A1,A2,CARD_2:41
.= len sga + 1 by A2,A3,Lm6,Th10
.= lensga + 1 by A6,FINSEQ_1:def 3;
A13: for j being Element of NAT st k <= j & j < len sga holds (for j9 being
Element of NAT st k <= j9 & j9 <= j holds P[j9]) implies P[j+1]
proof
let j be Element of NAT;
assume that
A14: k <= j and
A15: j < len sga;
A16: (j + 1) + 1 = j + (1 + 1);
A17: 1 <= j + 2 by NAT_1:12;
len sgb = card B by A3,Th10
.= card A + 1 by A1,A2,CARD_2:41
.= len sga + 1 by A2,A3,Lm6,Th10;
then j + 1 < len sgb by A15,XREAL_1:6;
then j + 2 <= len sgb by A16,NAT_1:13;
then j + 2 <= lensgb by A7,FINSEQ_1:def 3;
then
A18: j+2 in dom sgb by A7,A17,FINSEQ_1:1;
now
assume sgb/.(j+2) = a;
then j + 2 = k by A3,A8,A9,A18,Th75;
hence contradiction by A14,NAT_1:19;
end;
then
A19: not sgb/.(j+2) in {a} by TARSKI:def 1;
sgb/.(j+2) = sgb.(j+2) by A18,PARTFUN1:def 6;
then sgb/.(j+2) in rng sgb by A18,FUNCT_1:def 3;
then sgb/.(j+2) in B by A3,Def2;
then sgb/.(j+2) in A by A2,A19,XBOOLE_0:def 3;
then sgb/.(j+2) in rng sga by A4,Def2;
then consider l being object such that
A20: l in dom sga and
A21: sga.l = sgb/.(j+2) by FUNCT_1:def 3;
reconsider l as Element of NAT by A20;
A22: sga/.l = sga.l by A20,PARTFUN1:def 6;
A23: 1 <= l by A6,A20,FINSEQ_1:1;
j + 1 <= len sga by A15,NAT_1:13;
then
A24: j + 1 <= lensga by A6,FINSEQ_1:def 3;
1 <= j + 1 by NAT_1:12;
then
A25: j + 1 in dom sga by A6,A24,FINSEQ_1:1;
then
A26: sga/.(j+1) = sga.(j+1) by PARTFUN1:def 6;
assume
A27: for j9 being Element of NAT st k <= j9 & j9 <= j holds P[j9];
l <= lensga by A6,A20,FINSEQ_1:1;
then
A28: l + 1 <= lensgb by A12,XREAL_1:6;
1 <= l + 1 by NAT_1:12;
then
A29: l + 1 in dom sgb by A7,A28,FINSEQ_1:1;
l <= l + 1 by XREAL_1:29;
then
A30: l in dom sgb by A23,A29,FINSEQ_3:156;
assume
A31: sgb/.((j+1)+1) <> sga/.(j+1);
then
A32: l <> j + 1 by A20,A21,PARTFUN1:def 6;
per cases;
suppose
A33: l <= j + 1;
then l < j + 1 by A32,XXREAL_0:1;
then
A34: l <= j by NAT_1:13;
now
per cases;
case
k <= l;
then sgb/.(l+1) = sga/.l by A27,A34;
then j + 2 = l + 1 by A3,A18,A20,A21,A29,Th75,PARTFUN1:def 6;
hence thesis by A31,A20,A21,PARTFUN1:def 6;
end;
case
l < k;
then l <= k9 by A11,NAT_1:13;
then
A35: sgb/.l = sga/.l by A1,A2,A3,A8,A9,A23,Th76;
j + 1 < (j + 1) + 1 by XREAL_1:29;
hence thesis by A3,A18,A20,A21,A30,A33,A35,Th75,PARTFUN1:def 6;
end;
end;
hence thesis;
end;
suppose
A36: l > j + 1;
A37: for i9 being Element of NAT st 1 <= i9 & i9 <= j + 2 holds sga/.(j
+1) <> sgb/.i9
proof
let i9 be Element of NAT;
assume that
A38: 1 <= i9 and
A39: i9 <= j + 2;
assume
A40: sga/.(j+1) = sgb/.i9;
per cases;
suppose
i9 = j + 2;
hence contradiction by A31,A40;
end;
suppose
A41: i9 <> j + 2;
then i9 < j + 2 by A39,XXREAL_0:1;
then
A42: i9 <= j + 1 by A16,NAT_1:13;
then i9 <= lensga by A24,XXREAL_0:2;
then
A43: i9 in dom sga by A6,A38,FINSEQ_1:1;
now
per cases;
case
A44: i9 <= k;
now
per cases;
case
i9 = k;
then sga.(j+1) = a by A9,A25,A40,PARTFUN1:def 6;
then a in rng sga by A25,FUNCT_1:def 3;
hence contradiction by A1,A4,Def2;
end;
case
i9 <> k;
then i9 < k by A44,XXREAL_0:1;
then i9 <= k9 by A11,NAT_1:13;
then sgb/.i9 = sga/.i9 by A1,A2,A3,A8,A9,A38,Th76;
then
A45: i9 = j + 1 by A2,A3,A25,A40,A43,Lm6,Th75;
i9 <= j by A14,A44,XXREAL_0:2;
hence contradiction by A45,XREAL_1:29;
end;
end;
hence contradiction;
end;
case
A46: k < i9;
A47: i9 - 1 <= (j + 1) - 1 by A42,XREAL_1:9;
A48: i9 - 1 <= i9 by XREAL_1:146;
1 <= i9 by A10,A46,XXREAL_0:2;
then 1 - 1 <= i9 - 1 by XREAL_1:9;
then
A49: i9 - 1 is Element of NAT by INT_1:3;
A50: (i9 - 1) + 1 = i9 + (0 qua Nat);
then k <= i9 - 1 by A46,A49,NAT_1:13;
then 1 <= i9 - 1 by A10,XXREAL_0:2;
then
A51: i9 - 1 in dom sga by A43,A49,A48,FINSEQ_3:156;
k <= i9 - 1 by A46,A49,A50,NAT_1:13;
then sga/.(i9-1) = sga/.(j+1) by A27,A40,A49,A50,A47;
hence contradiction by A2,A3,A16,A25,A41,A50,A51,Lm6,Th75;
end;
end;
hence thesis;
end;
end;
sga/.(j+1) in rng sga by A25,A26,FUNCT_1:def 3;
then
A52: sga/.(j+1) in A by A4,Def2;
then sga/.(j+1) in B by A2,XBOOLE_0:def 3;
then sga/.(j+1) in rng sgb by A3,Def2;
then consider l9 being object such that
A53: l9 in dom sgb and
A54: sgb.l9 = sga/.(j+1) by FUNCT_1:def 3;
reconsider l9 as Element of NAT by A53;
A55: sgb/.l9 = sgb.l9 by A53,PARTFUN1:def 6;
A56: 1 <= j + 1 by NAT_1:12;
j + 1 <= len sga by A15,NAT_1:13;
then j + 1 in Seg(len sga) by A56,FINSEQ_1:1;
then j + 1 in dom sga by FINSEQ_1:def 3;
then
A57: [sga/.(j+1),sga/.l] in R by A4,A20,A36,Def2;
1 <= l9 by A7,A53,FINSEQ_1:1;
then l9 > j + 2 by A37,A54,A55;
then [sga/.l,sga/.(j+1)] in R by A3,A18,A21,A22,A53,A54,A55,Def2;
then sga/.l = sga/.(j+1) by A5,A57,A52;
hence thesis by A2,A3,A25,A20,A36,Lm6,Th75;
end;
end;
let i be Element of NAT;
assume that
A58: k <= i and
A59: i <= len(SgmX(R,A));
k <= len sga by A58,A59,XXREAL_0:2;
then
A60: k <= lensga by A6,FINSEQ_1:def 3;
then
A61: k in dom sga by A10,A6,FINSEQ_1:1;
A62: lensga <= lensgb by A12,NAT_1:11;
A63: P[k]
proof
A64: sga/.k = sga.k by A61,PARTFUN1:def 6;
then sga/.k in rng sga by A61,FUNCT_1:def 3;
then sga/.k in A by A4,Def2;
then sga/.k in B by A2,XBOOLE_0:def 3;
then sga/.k in rng sgb by A3,Def2;
then consider l being object such that
A65: l in dom sgb and
A66: sgb.l = sga/.k by FUNCT_1:def 3;
reconsider l as Element of NAT by A65;
A67: sgb/.l = sgb.l by A65,PARTFUN1:def 6;
A68: 1 <= l by A7,A65,FINSEQ_1:1;
assume
A69: not(P[k]);
then
A70: l <> k + 1 by A65,A66,PARTFUN1:def 6;
per cases by XXREAL_0:1;
suppose
l = k;
then sga.k = a by A8,A9,A64,A66,PARTFUN1:def 6;
then a in rng sga by A61,FUNCT_1:def 3;
hence thesis by A1,A4,Def2;
end;
suppose
A71: l < k;
then l <= lensga by A60,XXREAL_0:2;
then
A72: l in dom sga by A6,A68,FINSEQ_1:1;
l <= k9 by A11,A71,NAT_1:13;
then sga/.l = sga/.k by A1,A2,A3,A8,A9,A66,A68,A67,Th76;
hence thesis by A2,A3,A61,A71,A72,Lm6,Th75;
end;
suppose
k < l;
then
A73: k + 1 <= l by NAT_1:13;
A74: 1 <= k + 1 by NAT_1:12;
then
A75: k + 1 in dom sgb by A65,A73,FINSEQ_3:156;
now
assume sgb/.(k+1) = a;
then k + 1 = k by A3,A8,A9,A75,Th75;
hence contradiction;
end;
then
A76: not sgb/.(k+1) in {a} by TARSKI:def 1;
k + 1 < l by A70,A73,XXREAL_0:1;
then
A77: [sgb/.(k+1),sgb/.l] in R by A3,A65,A75,Def2;
sgb/.l in rng sgb by A65,A67,FUNCT_1:def 3;
then
A78: sgb/.l in B by A3,Def2;
sgb/.(k+1) = sgb.(k+1) by A65,A73,A74,FINSEQ_3:156,PARTFUN1:def 6;
then sgb/.(k+1) in rng sgb by A75,FUNCT_1:def 3;
then sgb/.(k+1) in B by A3,Def2;
then sgb/.(k+1) in A by A2,A76,XBOOLE_0:def 3;
then sgb/.(k+1) in rng sga by A4,Def2;
then consider l9 being object such that
A79: l9 in dom sga and
A80: sga.l9 = sgb/.(k+1) by FUNCT_1:def 3;
reconsider l9 as Element of NAT by A79;
A81: sga/.l9 = sga.l9 by A79,PARTFUN1:def 6;
A82: 1 <= l9 by A6,A79,FINSEQ_1:1;
l9 <= lensga by A6,A79,FINSEQ_1:1;
then l9 <= lensgb by A62,XXREAL_0:2;
then
A83: l9 in dom sgb by A7,A82,FINSEQ_1:1;
now
assume
A84: l9 < k;
then l9 <= k9 by A11,NAT_1:13;
then sgb/.l9 = sga/.l9 by A1,A2,A3,A8,A9,A82,Th76;
then l9 = k + 1 by A3,A75,A79,A80,A83,Th75,PARTFUN1:def 6;
hence contradiction by A84,XREAL_1:29;
end;
then l9 > k by A69,A80,A81,XXREAL_0:1;
then [sgb/.l,sgb/.(k+1)] in R by A4,A61,A66,A67,A79,A80,A81,Def2;
then sgb/.l = sgb/.(k+1) by A5,A77,A78;
hence thesis by A69,A65,A66,PARTFUN1:def 6;
end;
end;
for j being Element of NAT st k <= j & j <= len sga holds P[j] from
INT_1:sch 8(A63,A13);
hence thesis by A58,A59;
end;
theorem
for X being non empty set, A being finite Subset of X,
a being Element of X st not a in A
for B being finite Subset of X st B = {a} \/ A
for R being Order of X st R linearly_orders B
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
let X be non empty set, A be finite Subset of X, a be Element of X;
assume
A1: not a in A;
let B be finite Subset of X;
assume
A2: B = {a} \/ A;
let R be Order of X;
assume
A3: R linearly_orders B;
let k be Element of NAT;
assume that
A4: k+1 in dom(SgmX(R,B)) and
A5: SgmX(R,B)/.(k+1) = a;
set sgb = SgmX(R,B), sga = Ins(SgmX(R,A),k,a);
A6: dom sgb = Seg(len sgb) by FINSEQ_1:def 3;
then k + 1 <= len sgb by A4,FINSEQ_1:1;
then
A7: k + 1 -1 <= len sgb -1 by XREAL_1:9;
A8: k + 1 - 1 = k + (0 qua Nat);
A9: len sgb = card B by A3,Th10
.= card A + 1 by A1,A2,CARD_2:41
.= len SgmX(R,A) + 1 by A2,A3,Lm6,Th10;
then
A10: dom sgb = Seg(len sga) by A6,FINSEQ_5:69
.= dom sga by FINSEQ_1:def 3;
A11: for i being Nat st 1 <= i & i <= len sgb holds sgb.i = sga.i
proof
let i be Nat;
assume that
A12: 1 <= i and
A13: i <= len sgb;
A14: i in Seg(len sgb) by A12,A13,FINSEQ_1:1;
A15: i in dom sgb by FINSEQ_3:25,A12,A13;
A16: i in dom sga by A10,A14,FINSEQ_1:def 3;
per cases;
suppose
A17: i = k + 1; then
a = sgb.i by A5,PARTFUN1:def 6,A15;
hence sgb.i = sga.(k+1) by A9,A7,FINSEQ_5:73
.= sga.i by A17;
end;
suppose
A18: i <> k + 1;
now
per cases;
case
i < k + 1; then
A19: i <= k by NAT_1:13;
SgmX(R,A)|(Seg k) is FinSequence by FINSEQ_1:15;
then dom(SgmX(R,A)|(Seg k)) = Seg k by A9,A7,FINSEQ_1:17;
then SS: i in dom(SgmX(R,A)|(Seg k)) by A12,A19,FINSEQ_1:1;
then
A20: i in dom(SgmX(R,A)|k) by FINSEQ_1:def 16;
A: i in dom SgmX(R,A) by RELAT_1:57,SS;
thus sgb.i = sgb/.i by A15,PARTFUN1:def 6
.= SgmX(R,A)/.i by A1,A2,A3,A4,A5,A8,A12,A14,A19,Th76
.= SgmX(R,A).i by PARTFUN1:def 6,A
.= sga.i by A20,FINSEQ_5:72;
end;
case
A21: k + 1 <= i; then
a21: k+1 < i by A18,XXREAL_0:1;
1 - 1 <= i - 1 by A12,XREAL_1:9;
then reconsider i9 = i - 1 as Element of NAT by INT_1:3;
A22: i9 + 1 = i + (0 qua Nat);
F: 1 <= k+1 by FINSEQ_3:25,A4;
k + 1 < i9 + 1 by a21; then
1 < i9+1 by F,XXREAL_0:2; then
1 + 1 <= i9 + 1 by NAT_1:13; then
F1: 1 <= i9 by XREAL_1:6;
Z2: i9 + 1 in dom sga by A16; then
i9+1 <= len sga by FINSEQ_3:25; then
i9+1 <= len SgmX(R,A) + 1 by FINSEQ_5:69; then
i9 <= len SgmX(R,A) by XREAL_1:6; then
F2: i9 in dom SgmX(R,A) by FINSEQ_3:25,F1;
k + 1 < i by A18,A21,XXREAL_0:1;
then
A23: k + 1 <= i9 by A22,NAT_1:13;
A24: i9 <= len sgb - 1 by A13,XREAL_1:9;
thus sgb.i = sgb/.(i9+1) by A15,PARTFUN1:def 6
.= SgmX(R,A)/.i9 by A1,A2,A3,A4,A5,A9,A24,A23,Th77
.= SgmX(R,A).i9 by PARTFUN1:def 6,F2
.= sga.(i9+1) by A9,A24,A23,FINSEQ_5:74
.= sga/.(i9+1) by Z2,PARTFUN1:def 6
.= sga.i by A16,PARTFUN1:def 6;
end;
end;
hence thesis;
end;
end;
len sgb = len sga by A9,FINSEQ_5:69;
hence thesis by A11,FINSEQ_1:14;
end;
theorem
for X being set, b being bag of X st support b = {} holds b = EmptyBag X
by Def7;
Lm7: for X being set, b being bag of X holds b is PartFunc of X,NAT
proof
let X be set, b be bag of X;
for u being object holds u in b implies u in [:X,NAT:]
proof
let u be object;
assume
A2: u in b;
then consider u1,u2 being object such that
A3: u = [u1,u2] by RELAT_1:def 1;
u1 in dom b by A2,A3,XTUPLE_0:def 12;
then
A4: u1 in X;
u2 in rng b by A2,A3,XTUPLE_0:def 13;
hence thesis by A3,A4,ZFMISC_1:def 2;
end;
hence thesis by TARSKI:def 3;
end;
definition
let X be set, b be bag of X;
redefine attr b is empty-yielding means :: redefines empty-yielding (FUNCT_1, redefinition) → empty-yielding (RELAT_1, definition)
b = EmptyBag X;
compatibility;
end;
registration
let X be non empty set;
cluster non empty-yielding for bag of X;
existence
proof
set x = the Element of X;
set b = EmptyBag X +* (x,1);
take b;
dom (EmptyBag X) = X;
then
A1: b.x = ((EmptyBag X)+*(x.-->1)).x by FUNCT_7:def 3;
x in dom (x.-->1) by TARSKI:def 1;
then b.x = (x.-->1).x by A1,FUNCT_4:13
.= 1 by FUNCOP_1:72;
then b.x <> (EmptyBag X).x;
hence thesis;
end;
end;
definition
let X be set, b be bag of X;
redefine func support b -> finite Subset of X; :: redefines support (PRE_POLY, definition)
coherence
proof
A1: support b c= dom b by Th36;
for x being object holds x in support b implies x in X
proof
let x be object;
assume x in support b;
then x in dom b by A1;
hence thesis;
end;
hence thesis by TARSKI:def 3;
end;
end;
Lm8: for X being set, A being Subset of X, O being Order of X holds O
is_reflexive_in A & O is_antisymmetric_in A & O is_transitive_in A
proof
let X be set, A be Subset of X, O be Order of X;
A1: field O = X by ORDERS_1:12;
then O is_antisymmetric_in X by RELAT_2:def 12;
then
A2: for x,y being object holds x in A & y in A & [x,y] in O & [y,x] in O
implies x = y;
O is_transitive_in X by A1,RELAT_2:def 16;
then
A3: for x,y,z being object holds x in A & y in A & z in A & [x,y] in O & [y,z]
in O implies [x,z] in O;
O is_reflexive_in X by A1,RELAT_2:def 9;
then for x being object holds x in A implies [x,x] in O;
hence thesis by A2,A3;
end;
theorem
for n being Ordinal, b being bag of n holds RelIncl n
linearly_orders support b
proof
let n be Ordinal, b be bag of n;
set R = RelIncl n, s = support b;
for x,y being object holds x in s & y in s & x <> y implies [x,y] in R or [
y,x] in R
proof
let x,y be object;
assume that
A1: x in s and
A2: y in s and
x <> y;
assume
A3: not [x,y] in R;
reconsider x,y as Ordinal by A1,A2;
y c= x by A1,A2,A3,WELLORD2:def 1;
hence thesis by A1,A2,WELLORD2:def 1;
end;
then
A4: R is_connected_in s;
A5: R is_antisymmetric_in s by Lm8;
A6: R is_transitive_in s by Lm8;
R is_reflexive_in s by Lm8;
hence thesis by A4,A5,A6,ORDERS_1:def 9;
end;
definition
let X be set;
let x be FinSequence of X, b be bag of X;
redefine func b * x -> PartFunc of NAT,NAT; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence
proof
reconsider b as PartFunc of X,NAT by Lm7;
b * x c= [:NAT,NAT:];
hence thesis;
end;
end;
registration let X be set;
cluster support EmptyBag X -> empty;
coherence
proof set S = support EmptyBag X;
assume support EmptyBag X is not empty;
then (EmptyBag X).the Element of S <> 0 by Def7;
hence thesis;
end;
end;