:: Pigeon Hole Principle
:: by Wojciech A. Trybulec
::
:: Received April 8, 1990
:: Copyright (c) 1990-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, FUNCT_1, FINSEQ_1, NAT_1, RELAT_1, FINSET_1, CARD_1,
XBOOLE_0, TARSKI, XXREAL_0, SUBSET_1, PARTFUN1, ARYTM_1, ARYTM_3,
ORDINAL4, FINSEQ_4, FUNCT_2, EQREL_1, CARD_3, SETFAM_1, ZFMISC_1,
NUMBER09;
notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, SUBSET_1, ORDINAL1, RELAT_1,
CARD_1, SETFAM_1, EQREL_1, NUMBERS, XCMPLX_0, FUNCT_1, PARTFUN1, FUNCT_2,
FINSET_1, NAT_1, FINSEQ_1, FINSEQ_3, XXREAL_0;
constructors ZFMISC_1, ENUMSET1, WELLORD2, FUNCT_2, XXREAL_0, REAL_1,
PARTFUN1, NAT_1, INT_1, FINSEQ_3, RELSET_1, EQREL_1, SETFAM_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, XREAL_0, INT_1, FINSEQ_1,
ORDINAL1, CARD_1, RELSET_1, SUBSET_1, EQREL_1, NAT_1, PARTFUN1, FUNCT_2,
XXREAL_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions FUNCT_1, TARSKI, XBOOLE_0;
equalities RELAT_1, FINSEQ_1, ORDINAL1;
expansions RELAT_1, FUNCT_1, XBOOLE_0, FINSEQ_1;
theorems CARD_1, CARD_2, ENUMSET1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCT_1,
FUNCT_2, INT_1, NAT_1, PARTFUN1, TARSKI, WELLORD2, ZFMISC_1, RELAT_1,
XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, GRFUNC_1, EQREL_1,
RELSET_1, SETFAM_1;
schemes FINSEQ_1, FINSET_1, NAT_1, FUNCT_1, FINSEQ_2, FUNCT_2;
begin
reserve f for Function;
reserve p,q for FinSequence;
reserve A,B,C for set,x,x1,x2,y,z for object;
reserve k,l,m,n for Nat;
reserve a for Nat;
definition
let f; let x be object;
pred f is_one-to-one_at x means
f"Im(f,x) = {x};
end;
theorem Th1:
f is_one-to-one_at x implies x in dom f
proof
assume f is_one-to-one_at x;
then f"Im(f,x) = {x};
then x in f"Im(f,x) by TARSKI:def 1;
hence thesis by FUNCT_1:def 7;
end;
theorem Th2:
f is_one-to-one_at x iff x in dom f & f " {f.x} = {x}
proof
thus f is_one-to-one_at x implies x in dom f & f " {f.x} = {x}
proof
assume
A1: f is_one-to-one_at x;
hence
A2: x in dom f by Th1;
f"Im(f,x) = {x} by A1;
hence thesis by A2,FUNCT_1:59;
end;
assume x in dom f & f " {f.x} = {x};
hence f"Im(f,x) = {x} by FUNCT_1:59;
end;
theorem Th3:
f is_one-to-one_at x iff x in dom f & for z st z in dom f & x <>
z holds f.x <> f.z
proof
thus f is_one-to-one_at x implies x in dom f & for z st z in dom f & x <> z
holds f.x <> f.z
proof
assume
A1: f is_one-to-one_at x;
hence x in dom f by Th1;
let z;
assume that
A2: z in dom f and
A3: x <> z and
A4: f.x = f.z;
f.x in {f.x} by TARSKI:def 1;
then z in f " {f.x} by A2,A4,FUNCT_1:def 7;
then z in {x} by A1,Th2;
hence thesis by A3,TARSKI:def 1;
end;
assume that
A5: x in dom f and
A6: for z st z in dom f & x <> z holds f.x <> f.z and
A7: not f is_one-to-one_at x;
f " {f.x} <> {x} by A5,A7,Th2;
then consider y being object such that
A8: y in f " {f.x} & not y in {x} or y in {x} & not y in f " {f.x} by TARSKI:2;
f.x in {f.x} by TARSKI:def 1;
then
A9: x in f " {f.x} by A5,FUNCT_1:def 7;
now
per cases by A8;
suppose
A10: y in f " {f.x} & not y in {x};
then f.y in {f.x} by FUNCT_1:def 7;
then
A11: f.y = f.x by TARSKI:def 1;
y in dom f & x <> y by A10,FUNCT_1:def 7,TARSKI:def 1;
hence thesis by A6,A11;
end;
suppose
not y in f " {f.x} & y in {x};
hence thesis by A9,TARSKI:def 1;
end;
end;
hence thesis;
end;
theorem
(for x st x in dom f holds f is_one-to-one_at x) iff f is one-to-one
proof
thus (for x st x in dom f holds f is_one-to-one_at x) implies f is one-to-one
proof
assume
A1: for x st x in dom f holds f is_one-to-one_at x;
let x1,x2 be object;
assume that
A2: x1 in dom f and
A3: x2 in dom f & f.x1 = f.x2;
f is_one-to-one_at x1 by A1,A2;
hence thesis by A3,Th3;
end;
assume
A4: f is one-to-one;
let x;
assume
A5: x in dom f;
then for z holds z in dom f & x <> z implies f.x <> f.z by A4;
hence thesis by A5,Th3;
end;
definition
let R be Relation, y be object;
pred R just_once_values y means
:Def2:
card Coim(R,y) = 1;
end;
theorem Th5:
f just_once_values y implies y in rng f
proof
assume f just_once_values y;
then card Coim(f,y) = 1;
then rng f meets {y} by CARD_1:27,RELAT_1:138;
then consider x being object such that
A1: x in rng f /\ {y} by XBOOLE_0:4;
x in {y} by A1,XBOOLE_0:def 4;
then y = x by TARSKI:def 1;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem Th6:
f just_once_values y iff ex x st {x} = f " {y}
by CARD_2:42;
theorem Th7:
f just_once_values y iff
ex x being object st x in dom f & y = f.x &
for z being object st z in dom f & z <> x holds f.z <> y
proof
thus f just_once_values y implies
ex x being object st x in dom f & y = f.x & for z being object st z
in dom f & z <> x holds f.z <> y
proof
assume
A1: f just_once_values y;
then
A2: card Coim(f,y) = 1;
y in rng f by A1,Th5;
then consider x1 being object such that
A3: x1 in dom f and
A4: f.x1 = y by FUNCT_1:def 3;
f.x1 in {y} by A4,TARSKI:def 1;
then
A5: x1 in f " {y} by A3,FUNCT_1:def 7;
take x1;
thus x1 in dom f & y = f.x1 by A3,A4;
let z be object;
assume that
A6: z in dom f and
A7: z <> x1 and
A8: f.z = y;
A9: f"{y} is finite by A2;
f.z in {y} by A8,TARSKI:def 1;
then z in f " {y} by A6,FUNCT_1:def 7;
then {z,x1} c= f " {y} by A5,ZFMISC_1:32;
then card{z,x1} <= 1 by A9,A2,NAT_1:43;
then 2 <= 1 by A7,CARD_2:57;
hence thesis;
end;
given x being object such that
A10: x in dom f and
A11: y = f.x and
A12: for z being object st z in dom f & z <> x holds f.z <> y;
A13: {x} = f " {y}
proof
thus {x} c= f " {y}
proof
let x1 be object;
assume x1 in {x};
then
A14: x1 = x by TARSKI:def 1;
f.x in {y} by A11,TARSKI:def 1;
hence thesis by A10,A14,FUNCT_1:def 7;
end;
let x1 be object;
assume
A15: x1 in f " {y};
then f.x1 in {y} by FUNCT_1:def 7;
then
A16: f.x1 = y by TARSKI:def 1;
x1 in dom f by A15,FUNCT_1:def 7;
then x1 = x by A12,A16;
hence thesis by TARSKI:def 1;
end;
card Coim(f,y) = 1 by A13,CARD_1:30;
hence thesis;
end;
theorem Th8:
f is one-to-one iff for y st y in rng f holds f just_once_values y
proof
thus f is one-to-one implies for y st y in rng f holds f just_once_values y
proof
assume
A1: f is one-to-one;
let y;
assume y in rng f;
then consider x being object such that
A2: x in dom f & f.x = y by FUNCT_1:def 3;
for z being object holds z in dom f & z <> x implies f.z <> y
by A1,A2;
hence thesis by A2,Th7;
end;
assume
A3: for y st y in rng f holds f just_once_values y;
let x,y be object;
assume that
A4: x in dom f and
A5: y in dom f & f.x = f.y;
f.x in rng f by A4,FUNCT_1:def 3;
then f just_once_values f.x by A3;
then consider x1 such that
A6: {x1} = f " {f.x} by Th6;
A7: f.x in {f.x} by TARSKI:def 1;
then
A8: y in f "{f.x} by A5,FUNCT_1:def 7;
x in f " {f.x} by A4,A7,FUNCT_1:def 7;
then x = x1 by A6,TARSKI:def 1;
hence thesis by A6,A8,TARSKI:def 1;
end;
theorem Th9:
f is_one-to-one_at x iff x in dom f & f just_once_values f.x
proof
thus f is_one-to-one_at x implies x in dom f & f just_once_values f.x
proof
assume
A1: f is_one-to-one_at x;
hence x in dom f by Th1;
{x} = f " {f.x} by A1,Th2;
hence thesis by Th6;
end;
assume that
A2: x in dom f and
A3: f just_once_values f.x;
consider z such that
A4: f " {f.x} = {z} by A3,Th6;
f.x in {f.x} by TARSKI:def 1;
then x in {z} by A2,A4,FUNCT_1:def 7;
then x = z by TARSKI:def 1;
hence thesis by A2,A4,Th2;
end;
definition
let f,y;
assume
A1: f just_once_values y;
func f <- y -> set means
:Def3:
it in dom f & f.it = y;
existence
proof
y in rng f by A1,Th5;
then consider x being object such that
A2: x in dom f & f.x = y by FUNCT_1:def 3;
take x;
thus thesis by A2;
end;
uniqueness
proof
let x1,x2 be set;
assume that
A3: x1 in dom f & f.x1 = y and
A4: x2 in dom f & f.x2 = y;
consider x being object such that
x in dom f and
f.x = y and
A5: for z being object st z in dom f & z <> x holds f.z <> y by A1,Th7;
x = x1 by A3,A5;
hence thesis by A4,A5;
end;
end;
theorem
f just_once_values y implies Im(f, f<-y) = {y}
proof
assume
A1: f just_once_values y;
then f <- y in dom f by Def3;
hence Im(f,f <- y) = {f.(f <- y)} by FUNCT_1:59
.= {y} by A1,Def3;
end;
theorem Th11:
f just_once_values y implies f " {y} = {f <- y}
proof
assume
A1: f just_once_values y;
then consider x such that
A2: {x} = f " {y} by Th6;
A3: x in f " {y} by A2,ZFMISC_1:31;
then f.x in {y} by FUNCT_1:def 7;
then
A4: f.x = y by TARSKI:def 1;
x in dom f by A3,FUNCT_1:def 7;
hence thesis by A1,A2,A4,Def3;
end;
theorem
f is one-to-one & y in rng f implies (f").y = f <- y
proof
assume that
A1: f is one-to-one and
A2: y in rng f;
consider x being object such that
A3: x in dom f & f.x = y by A2,FUNCT_1:def 3;
f just_once_values y by A1,A2,Th8;
then x = f <- y by A3,Def3;
hence thesis by A1,A3,FUNCT_1:32;
end;
theorem
f is_one-to-one_at x implies f <- (f.x) = x
proof
assume f is_one-to-one_at x;
then x in dom f & f just_once_values f.x by Th9;
hence thesis by Def3;
end;
theorem
f just_once_values y implies f is_one-to-one_at f <- y
proof
assume
A1: f just_once_values y;
A2: now
let x;
assume x in dom f & x <> f <- y;
then f.x <> y by A1,Def3;
hence f.x <> f.(f <- y) by A1,Def3;
end;
f <- y in dom f by A1,Def3;
hence thesis by A2,Th3;
end;
reserve D for non empty set;
reserve d,d1,d2,d3 for Element of D;
definition
let D;
let d1,d2;
redefine func <* d1,d2 *> -> FinSequence of D; :: redefines <* (FINSEQ_1, definition)
coherence by FINSEQ_2:13;
end;
definition
let D;
let d1,d2,d3;
redefine func <* d1,d2,d3 *> -> FinSequence of D; :: redefines <* (FINSEQ_1, definition)
coherence by FINSEQ_2:14;
end;
theorem
for i being Nat for D being set, P being FinSequence of D st 1 <= i &
i <= len P holds P/.i = P.i
proof
let i be Nat;
let D be set, P be FinSequence of D;
assume 1 <= i & i <= len P;
then i in dom P by FINSEQ_3:25;
hence thesis by PARTFUN1:def 6;
end;
theorem
<* d *>/.1 = d
proof
A1: 1 in {1} by FINSEQ_1:2;
dom<* d *> = {1} & <* d *>.1 = d by FINSEQ_1:2,def 8;
hence thesis by A1,PARTFUN1:def 6;
end;
theorem
<* d1,d2 *>/.1 = d1 & <* d1,d2 *>/.2 = d2
proof
set s = <* d1,d2 *>;
A1: s.2 = d2 & 1 in {1,2} by FINSEQ_1:2;
A2: 2 in {1,2} by FINSEQ_1:2;
dom s = {1,2} & s.1 = d1 by FINSEQ_1:2,89;
hence thesis by A1,A2,PARTFUN1:def 6;
end;
theorem
<* d1,d2,d3 *>/.1 = d1 & <* d1,d2,d3 *>/.2 = d2 & <* d1,d2,d3 *>/.3 = d3
proof
set s = <* d1,d2,d3 *>;
A1: s.2 = d2 & s.3 = d3;
A2: 1 in {1,2,3} & 2 in {1,2,3} by FINSEQ_3:1;
A3: 3 in {1,2,3} by FINSEQ_3:1;
dom s = {1,2,3} & s.1 = d1 by FINSEQ_1:89,FINSEQ_3:1;
hence thesis by A1,A2,A3,PARTFUN1:def 6;
end;
definition
let p; let x be object;
func x..p -> Element of NAT equals
Sgm(p " {x}).1;
coherence
proof
set q = Sgm(p " {x});
per cases;
suppose not 1 in dom q;
then q.1 = 0 by FUNCT_1:def 2;
hence thesis;
end;
suppose
A1: 1 in dom q;
A2: rng q c= NAT by FINSEQ_1:def 4;
q.1 in rng q by A1,FUNCT_1:def 3;
hence thesis by A2;
end;
end;
end;
theorem Th19:
x in rng p implies p.(x..p) = x
proof
set q = Sgm(p " {x});
p " {x} c= dom p & dom p = Seg(len p) by FINSEQ_1:def 3,RELAT_1:132;
then
a1: p"{x} is included_in_Seg;
assume x in rng p;
then p " {x} <> {} by FUNCT_1:72;
then rng q <> {} by a1,FINSEQ_1:def 14;
then 1 in dom q by FINSEQ_3:32;
then
A2: q.1 in rng q by FUNCT_1:def 3;
rng q = p " {x} by a1,FINSEQ_1:def 14;
then p.(x..p) in {x} by A2,FUNCT_1:def 7;
hence thesis by TARSKI:def 1;
end;
theorem Th20:
x in rng p implies x..p in dom p
proof
p " {x} c= dom p & dom p = Seg(len p) by FINSEQ_1:def 3,RELAT_1:132;
then
a1: p"{x} is included_in_Seg;
assume x in rng p;
then p " {x} <> {} by FUNCT_1:72;
then rng(Sgm(p " {x})) <> {} by a1,FINSEQ_1:def 14;
then 1 in dom(Sgm(p " {x})) by FINSEQ_3:32;
then x..p in rng(Sgm(p " {x})) by FUNCT_1:def 3;
then x..p in p " {x} by a1,FINSEQ_1:def 14;
hence thesis by FUNCT_1:def 7;
end;
theorem Th21:
x in rng p implies 1 <= x..p & x..p <= len p
proof
assume x in rng p;
then x..p in dom p by Th20;
hence thesis by FINSEQ_3:25;
end;
theorem Th22:
x in rng p implies x..p - 1 is Element of NAT & len p - x..p is
Element of NAT
proof
assume x in rng p;
then 1 <= x..p & x..p <= len p by Th21;
hence thesis by INT_1:5;
end;
theorem Th23:
x in rng p implies x..p in p " {x}
proof
assume
A1: x in rng p;
then p.(x..p) = x by Th19;
then
A2: p.(x..p) in {x} by TARSKI:def 1;
x..p in dom p by A1,Th20;
hence thesis by A2,FUNCT_1:def 7;
end;
theorem Th24:
for k st k in dom p & k < x..p holds p.k <> x
proof
let k;
set q = Sgm(p " {x});
assume that
A1: k in dom p and
A2: k < x..p and
A3: p.k = x;
A4: x in {x} by TARSKI:def 1;
p " {x} c= dom p & dom p = Seg(len p) by FINSEQ_1:def 3,RELAT_1:132;
then
a1: p"{x} is included_in_Seg;
then rng q = p " {x} by FINSEQ_1:def 14;
then k in rng q by A1,A3,A4,FUNCT_1:def 7;
then consider y being object such that
A6: y in dom q and
A7: q.y = k by FUNCT_1:def 3;
reconsider y as Element of NAT by A6;
A8: now
assume not 1 < y;
then 1 = y or y < 1 by XXREAL_0:1;
hence contradiction by A2,A6,A7,FINSEQ_3:24,NAT_1:14;
end;
dom q = Seg(len q) by FINSEQ_1:def 3;
then y <= len q by A6,FINSEQ_1:1;
hence contradiction by a1,A2,A7,A8,FINSEQ_1:def 14;
end;
theorem Th25:
p just_once_values x implies p <- x = x..p
proof
assume
A1: p just_once_values x;
then x in rng p by Th5;
then x..p in dom p & p.(x..p) = x by Th19,Th20;
hence thesis by A1,Def3;
end;
theorem Th26:
p just_once_values x implies for k st k in dom p & k <> x..p holds p.k <> x
proof
assume
A1: p just_once_values x;
let k;
assume
A2: k in dom p & k <> x..p & p.k = x;
p <- x = x..p by A1,Th25;
hence thesis by A1,A2,Def3;
end;
theorem Th27:
x in rng p & (for k st k in dom p & k <> x..p holds p.k <> x)
implies p just_once_values x
proof
assume that
A1: x in rng p and
A2: for k st k in dom p & k <> x..p holds p.k <> x;
A3: for z being object st z in dom p & z <> x..p holds p.z <> x by A2;
p.(x..p) = x & x..p in dom p by A1,Th19,Th20;
hence thesis by A3,Th7;
end;
theorem
p just_once_values x iff x in rng p & {x..p} = p " {x}
proof
thus p just_once_values x implies x in rng p & {x..p} = p " {x}
proof
assume
A1: p just_once_values x;
then x..p = p <- x by Th25;
hence thesis by A1,Th5,Th11;
end;
assume that
A2: x in rng p and
A3: {x..p} = p " {x};
A4: now
let z be object;
assume that
A5: z in dom p and
A6: z <> x..p and
A7: p.z = x;
p.z in {x} by A7,TARSKI:def 1;
then z in p " {x} by A5,FUNCT_1:def 7;
hence contradiction by A3,A6,TARSKI:def 1;
end;
p.(x..p) = x & x..p in dom p by A2,Th19,Th20;
hence thesis by A4,Th7;
end;
theorem
p is one-to-one & x in rng p implies {x..p} = p " {x}
proof
assume that
A1: p is one-to-one and
A2: x in rng p;
thus {x..p} c= p " {x}
proof
let y be object;
assume y in {x..p};
then y = x..p by TARSKI:def 1;
hence thesis by A2,Th23;
end;
let y be object;
assume
A3: y in p " {x};
then
A4: y in dom p by FUNCT_1:def 7;
p.y in {x} by A3,FUNCT_1:def 7;
then
A5: p.y = x by TARSKI:def 1;
p.(x..p) = x & x..p in dom p by A2,Th19,Th20;
then x..p = y by A1,A4,A5;
hence thesis by TARSKI:def 1;
end;
theorem Th30:
p just_once_values x iff len(p - {x}) = len p - 1
proof
thus p just_once_values x implies len(p - {x}) = len p - 1
by FINSEQ_3:59;
assume len(p - {x}) = len p - 1;
then len p + -1 = len p - card(p " {x}) by FINSEQ_3:59
.= len p + - (card (p"{x}));
hence thesis;
end;
reserve L,M for Element of NAT;
theorem Th31:
p just_once_values x implies for k st k in dom(p - {x}) holds (k
< x..p implies (p - {x}).k = p.k) & (x..p <= k implies (p - {x}).k = p.(k + 1))
proof
assume
A1: p just_once_values x;
set q = p - {x};
let k;
assume
A2: k in dom(p - {x});
set A = {L : L in dom p & L <= k & p.L in {x}};
A3: dom(p - {x}) c= dom p by FINSEQ_3:63;
thus k < x..p implies (p - {x}).k = p.k
proof
assume
A4: k < x..p;
A c= {}
proof
let y be object;
assume y in A;
then consider L such that
y = L and
A5: L in dom p & L <= k and
A6: p.L in {x};
p.L <> x by A1,A4,A5,Th26;
hence thesis by A6,TARSKI:def 1;
end;
then
A7: A = {};
p.k <> x by A1,A2,A3,A4,Th26;
then not p.k in {x} by TARSKI:def 1;
then q.(k - 0) = p.k by A2,A3,A7,CARD_1:27,FINSEQ_3:85;
hence thesis;
end;
set B = {M : M in dom p & M <= k + 1 & p.M in {x}};
assume
A8: x..p <= k;
A9: x in rng p by A1,Th5;
A10: B = {x..p}
proof
thus B c= {x..p}
proof
let y be object;
assume y in B;
then consider M such that
A11: M = y and
A12: M in dom p and
M <= k + 1 and
A13: p.M in {x};
p.M = x by A13,TARSKI:def 1;
then M = x..p by A1,A12,Th26;
hence thesis by A11,TARSKI:def 1;
end;
let y be object;
assume y in {x..p};
then
A14: y = x..p by TARSKI:def 1;
p.(x..p) = x by A9,Th19;
then
A15: p.(x..p) in {x} by TARSKI:def 1;
x..p in dom p & x..p <= k + 1 by A9,A8,Th20,NAT_1:12;
hence thesis by A14,A15;
end;
then reconsider B as finite set;
dom q = Seg(len q) & len(p - {x}) = len p - 1 by A1,Th30,FINSEQ_1:def 3;
then k <= len p - 1 by A2,FINSEQ_1:1;
then 1 <= k + 1 & k + 1 <= len p by NAT_1:12,XREAL_1:19;
then k + 1 in Seg(len p);
then
A16: k + 1 in dom p by FINSEQ_1:def 3;
now
x..p <> k + 1 by A8,XREAL_1:29;
then
A17: p.(k + 1) <> x by A1,A16,Th26;
assume p.(k + 1) in {x};
hence contradiction by A17,TARSKI:def 1;
end;
then (p - {x}).((k + 1) - card B) = p.(k + 1) by A16,FINSEQ_3:85;
then q.((k + 1) - 1) = p.(k + 1) by A10,CARD_1:30;
hence thesis;
end;
theorem
p is one-to-one & x in rng p implies for k st k in dom(p - {x}) holds
((p - {x}).k = p.k iff k < x..p) & ((p - {x}).k = p.(k + 1) iff x..p <= k)
proof
assume that
A1: p is one-to-one and
A2: x in rng p;
set q = p - {x};
let k;
assume
A3: k in dom(p - {x});
A4: p just_once_values x by A1,A2,Th8;
then dom q = Seg(len q) & len(p - {x}) = len p - 1 by Th30,FINSEQ_1:def 3;
then k <= len p - 1 by A3,FINSEQ_1:1;
then 1 <= k + 1 & k + 1 <= len p by NAT_1:12,XREAL_1:19;
then k + 1 in Seg(len p);
then
A5: dom(p - {x}) c= dom p & k + 1 in dom p by FINSEQ_1:def 3,FINSEQ_3:63;
thus (p - {x}).k = p.k implies k < x..p
proof
assume that
A6: (p - {x}).k = p.k and
A7: not k < x..p;
q.k = p.(k + 1) by A4,A3,A7,Th31;
then k + 0 = k + 1 by A1,A3,A5,A6;
hence thesis;
end;
thus k < x..p implies (p - {x}).k = p.k by A4,A3,Th31;
thus (p - {x}).k = p.(k + 1) implies x..p <= k
proof
assume
A8: (p - {x}).k = p.(k + 1);
assume not x..p <= k;
then p.(k + 1) = p.k by A4,A3,A8,Th31;
then k + 0 = k + 1 by A1,A3,A5;
hence thesis;
end;
thus thesis by A4,A3,Th31;
end;
definition
let p;
let x;
assume
A1: x in rng p;
func p -| x -> FinSequence means
:Def5:
ex n st n = x..p - 1 & it = p | Seg n;
existence
proof
reconsider n = x..p - 1 as Element of NAT by A1,Th22;
reconsider q = p | Seg n as FinSequence by FINSEQ_1:15;
take q;
thus thesis;
end;
uniqueness;
end;
theorem Th33:
x in rng p & n = x..p - 1 implies p | Seg n = p -| x
proof
assume x in rng p;
then ex m st m = x..p - 1 & p | Seg m = p -| x by Def5;
hence thesis;
end;
theorem Th34:
x in rng p implies len(p -| x) = x..p - 1
proof
assume
A1: x in rng p;
then consider n such that
A2: n = x..p - 1 and
A3: p | Seg n = p -| x by Def5;
A4: n <= n + 1 by NAT_1:12;
n + 1 <= len p by A1,A2,Th21;
then n <= len p by A4,XXREAL_0:2;
hence thesis by A2,A3,FINSEQ_1:17;
end;
theorem Th35:
x in rng p & n = x..p - 1 implies dom(p -| x) = Seg n
proof
assume x in rng p;
then len(p -| x) = x..p - 1 by Th34;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th36:
x in rng p & k in dom(p -| x) implies p.k = (p -| x).k
proof
assume that
A1: x in rng p and
A2: k in dom(p -| x);
ex n st n = x..p - 1 & p | Seg n = p -| x by A1,Def5;
hence thesis by A2,FUNCT_1:47;
end;
theorem Th37:
x in rng p implies not x in rng(p -| x)
proof
assume that
A1: x in rng p and
A2: x in rng(p -| x);
reconsider n = x..p - 1 as Element of NAT by A1,Th22;
set r = p | Seg n;
A3: r = p -| x by A1,Th33;
then consider y being object such that
A4: y in dom r and
A5: r.y = x by A2,FUNCT_1:def 3;
A6: dom r = Seg n by A1,A3,Th35;
then reconsider y as Element of NAT by A4;
y <= n by A4,A6,FINSEQ_1:1;
then
A7: y + 1 <= x..p by XREAL_1:19;
y < y + 1 by XREAL_1:29;
then dom r c= dom p & y < x..p by A7,RELAT_1:60,XXREAL_0:2;
then p.y <> x by A4,Th24;
hence thesis by A4,A5,FUNCT_1:47;
end;
theorem
x in rng p implies rng(p -| x) misses {x}
proof
assume x in rng p;
then not x in rng(p -| x) by Th37;
then for y being object st y in rng(p -| x) holds not y in {x}
by TARSKI:def 1;
hence thesis by XBOOLE_0:3;
end;
theorem
x in rng p implies rng(p -| x) c= rng p
proof
assume x in rng p;
then ex n st n = x..p - 1 & p | Seg n = p -| x by Def5;
hence thesis by RELAT_1:70;
end;
theorem
x in rng p implies (x..p = 1 iff p -| x = {})
proof
assume
A1: x in rng p;
thus x..p = 1 implies p -| x = {}
proof
assume
A2: x..p = 1;
len(p -| x) = x..p - 1 by A1,Th34
.= 0 by A2;
hence thesis;
end;
assume p -| x = {};
then
A3: len(p -| x) = 0;
len(p -| x) = x..p - 1 by A1,Th34;
hence thesis by A3;
end;
theorem
x in rng p & p is FinSequence of D implies p -| x is FinSequence of D
proof
assume x in rng p;
then ex n st n = x..p - 1 & p | Seg n = p -| x by Def5;
hence thesis by FINSEQ_1:18;
end;
definition
let p;
let x;
assume
A1: x in rng p;
func p |-- x -> FinSequence means
:Def6:
len it = len p - x..p & for k st k in dom it holds it.k = p.(k + x..p);
existence
proof
deffunc F(Nat) = p.($1 + x..p);
reconsider n = len p - x..p as Element of NAT by A1,Th22;
consider q such that
A2: len q = n & for k be Nat st k in dom q holds q.k = F(k) from
FINSEQ_1:sch 2;
take q;
thus thesis by A2;
end;
uniqueness
proof
let q,r be FinSequence;
assume that
A3: len q = len p - x..p and
A4: for k st k in dom q holds q.k = p.(k + x..p);
assume that
A5: len r = len p - x..p and
A6: for k st k in dom r holds r.k = p.(k + x..p);
now
let k be Nat;
A7: dom q = Seg(len q) & dom r = Seg(len r) by FINSEQ_1:def 3;
assume
A8: k in dom q;
then q.k = p.(k + x..p) by A4;
hence q.k = r.k by A3,A5,A6,A8,A7;
end;
hence thesis by A3,A5,FINSEQ_2:9;
end;
end;
theorem Th42:
x in rng p & n = len p - x..p implies dom(p |-- x) = Seg n
proof
assume x in rng p;
then len(p |-- x) = len p - x..p by Def6;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th43:
x in rng p & n in dom(p |-- x) implies n + x..p in dom p
proof
assume that
A1: x in rng p and
A2: n in dom(p |-- x);
reconsider m = len p - x..p as Element of NAT by A1,Th22;
n in Seg m by A1,A2,Th42;
then n <= len p - x..p by FINSEQ_1:1;
then
A3: n + x..p <= len p by XREAL_1:19;
1 <= n by A2,FINSEQ_3:25;
then 1 <= n + x..p by NAT_1:12;
hence thesis by A3,FINSEQ_3:25;
end;
theorem
x in rng p implies rng(p |-- x) c= rng p
proof
assume
A1: x in rng p;
let y be object;
assume y in rng(p |-- x);
then consider z being object such that
A2: z in dom(p |-- x) and
A3: (p |-- x).z = y by FUNCT_1:def 3;
reconsider z as Element of NAT by A2;
y = p.(z + x..p) & z + x..p in dom p by A1,A2,A3,Def6,Th43;
hence thesis by FUNCT_1:def 3;
end;
theorem Th45:
p just_once_values x iff x in rng p & not x in rng(p |-- x)
proof
thus p just_once_values x implies x in rng p & not x in rng(p |-- x)
proof
assume
A1: p just_once_values x;
hence
A2: x in rng p by Th5;
assume x in rng(p |-- x);
then consider z being object such that
A3: z in dom(p |-- x) and
A4: (p |-- x).z = x by FUNCT_1:def 3;
reconsider z as Element of NAT by A3;
(p |-- x).z = p.(z + x..p) & z + x..p in dom p by A2,A3,Def6,Th43;
then z + x..p = 0 + x..p by A1,A4,Th26;
hence thesis by A3,FINSEQ_3:24;
end;
assume that
A5: x in rng p and
A6: not x in rng(p |-- x);
now
let k;
assume that
A7: k in dom p and
A8: k <> x..p and
A9: p.k = x;
now
per cases by A8,XXREAL_0:1;
suppose
k < x..p;
then k + 1 <= x..p by NAT_1:13;
then k <= x..p - 1 by XREAL_1:19;
then
A10: k <= len(p -| x) by A5,Th34;
1 <= k by A7,FINSEQ_3:25;
then
A11: k in dom(p -| x) by A10,FINSEQ_3:25;
then x = (p -| x).k by A5,A9,Th36;
then x in rng(p -| x) by A11,FUNCT_1:def 3;
hence contradiction by A5,Th37;
end;
suppose
A12: x..p < k;
then consider m be Nat such that
A13: k = x..p + m by NAT_1:10;
x..p + 0 < x..p + m by A12,A13;
then 0 < m;
then
A14: 0 + 1 <= m by NAT_1:13;
m + x..p <= len p by A7,A13,FINSEQ_3:25;
then m <= len p - x..p by XREAL_1:19;
then m <= len(p |-- x) by A5,Def6;
then
A15: m in dom(p |-- x) by A14,FINSEQ_3:25;
then (p |-- x).m = p.k by A5,A13,Def6;
hence contradiction by A6,A9,A15,FUNCT_1:def 3;
end;
end;
hence contradiction;
end;
hence thesis by A5,Th27;
end;
theorem Th46:
x in rng p & p is one-to-one implies not x in rng(p |-- x)
proof
assume that
A1: x in rng p and
A2: p is one-to-one and
A3: x in rng(p |-- x);
A4: len(p |-- x) = len p - x..p by A1,Def6;
consider y being object such that
A5: y in dom(p |-- x) and
A6: (p |-- x).y = x by A3,FUNCT_1:def 3;
reconsider y as Element of NAT by A5;
A7: 1 <= y + x..p by A1,Th21,NAT_1:12;
A8: y in Seg(len(p |-- x)) by A5,FINSEQ_1:def 3;
then y <= len(p |-- x) by FINSEQ_1:1;
then y + x..p <= len p by A4,XREAL_1:19;
then y + x..p in Seg(len p) by A7;
then
A9: y + x..p in dom p by FINSEQ_1:def 3;
A10: x..p in dom p & p.(x..p) = x by A1,Th19,Th20;
(p |-- x).y = p.(y + x..p) by A1,A5,Def6;
then 0 + x..p = y + x..p by A2,A6,A10,A9;
hence thesis by A8,FINSEQ_1:1;
end;
theorem
p just_once_values x iff x in rng p & rng(p |-- x) misses {x}
proof
thus p just_once_values x implies x in rng p & rng(p |-- x) misses {x}
proof
assume
A1: p just_once_values x;
hence x in rng p by Th45;
assume not rng(p |-- x) misses {x};
then
A2: ex y being object st y in rng(p |-- x) & y in {x} by XBOOLE_0:3;
not x in rng(p |-- x) by A1,Th45;
hence thesis by A2,TARSKI:def 1;
end;
assume that
A3: x in rng p and
A4: rng(p |-- x) misses {x};
now
A5: x in {x} by TARSKI:def 1;
assume x in rng(p |-- x);
hence contradiction by A4,A5,XBOOLE_0:3;
end;
hence thesis by A3,Th45;
end;
theorem
x in rng p & p is one-to-one implies rng(p |-- x) misses {x}
proof
assume x in rng p & p is one-to-one;
then not x in rng(p |-- x) by Th46;
then for y being object st y in rng(p |-- x) holds not y in {x}
by TARSKI:def 1;
hence thesis by XBOOLE_0:3;
end;
theorem
x in rng p implies (x..p = len p iff p |-- x = {})
proof
assume
A1: x in rng p;
thus x..p = len p implies p |-- x = {}
proof
assume
A2: x..p = len p;
len(p |-- x) = len p - x..p by A1,Def6
.= 0 by A2;
hence thesis;
end;
assume p |-- x = {};
then
A3: len(p |-- x) = 0;
len(p |-- x) = len p - x..p by A1,Def6;
hence thesis by A3;
end;
theorem
x in rng p & p is FinSequence of D implies p |-- x is FinSequence of D
proof
assume that
A1: x in rng p and
A2: p is FinSequence of D;
rng(p |-- x) c= D
proof
A3: len(p |-- x) = len p - x..p by A1,Def6;
let y be object;
assume y in rng(p |-- x);
then consider z being object such that
A4: z in dom(p |-- x) and
A5: (p |-- x).z = y by FUNCT_1:def 3;
reconsider z as Element of NAT by A4;
dom(p |-- x) = Seg(len(p |-- x)) by FINSEQ_1:def 3;
then z <= len(p |-- x) by A4,FINSEQ_1:1;
then
A6: z + x..p <= len p by A3,XREAL_1:19;
1 <= z + x..p by A1,Th21,NAT_1:12;
then z + x..p in Seg(len p) by A6;
then
A7: z + x..p in dom p by FINSEQ_1:def 3;
y = p.(z + x..p) by A1,A4,A5,Def6;
then
A8: y in rng p by A7,FUNCT_1:def 3;
rng p c= D by A2,FINSEQ_1:def 4;
hence thesis by A8;
end;
hence thesis by FINSEQ_1:def 4;
end;
theorem Th51:
x in rng p implies p = (p -| x) ^ <* x *> ^ (p |-- x)
proof
set q1 = p -| x;
set q2 = p |-- x;
set r = q1 ^ <* x *>;
assume
A1: x in rng p;
A2: now
let k be Nat;
assume k in dom q2;
then q2.k = p.(x..p - 1 + 1 + k) by A1,Def6
.= p.(len q1 + 1 + k) by A1,Th34
.= p.(len q1 + len<* x *> + k) by FINSEQ_1:40
.= p.(len r + k) by FINSEQ_1:22;
hence p.(len r + k) = q2.k;
end;
A3: now
let k be Nat;
assume
A4: k in dom r;
now
per cases by A4,FINSEQ_1:25;
suppose
A5: k in dom q1;
hence r.k = q1.k by FINSEQ_1:def 7
.= p.k by A1,A5,Th36;
end;
suppose
ex n be Nat st n in dom<* x *> & k = len q1 + n;
then consider n be Nat such that
A6: n in dom <* x *> and
A7: k = len q1 + n;
n in {1} by A6,FINSEQ_1:2,def 8;
then
A8: n = 1 by TARSKI:def 1;
hence r.k = <* x *>.1 by A6,A7,FINSEQ_1:def 7
.= x
.= p.(x..p - 1 + 1) by A1,Th19
.= p.k by A1,A7,A8,Th34;
end;
end;
hence p.k = r.k;
end;
len p = len p - x..p + x..p .= x..p - 1 + 1 + len q2 by A1,Def6
.= len q1 + 1 + len q2 by A1,Th34
.= len q1 + len<* x *> + len q2 by FINSEQ_1:40
.= len r + len q2 by FINSEQ_1:22;
hence thesis by A3,A2,FINSEQ_3:38;
end;
theorem
x in rng p & p is one-to-one implies p -| x is one-to-one
proof
assume x in rng p;
then p = (p -| x) ^ <* x *> ^ (p |-- x) by Th51
.= (p -| x) ^ (<* x *> ^ (p |-- x)) by FINSEQ_1:32;
hence thesis by FINSEQ_3:91;
end;
theorem
x in rng p & p is one-to-one implies p |-- x is one-to-one
proof
assume x in rng p;
then p = (p -| x) ^ <* x *> ^ (p |-- x) by Th51;
hence thesis by FINSEQ_3:91;
end;
theorem Th54:
p just_once_values x iff x in rng p & p - {x} = (p -| x) ^ (p |-- x)
proof
set q = p - {x};
set r = p -| x;
set s = p |-- x;
thus p just_once_values x implies x in rng p & p - {x} = (p -| x) ^ (p |-- x
)
proof
assume
A1: p just_once_values x;
hence
A2: x in rng p by Th5;
A3: now
x..p <= len p by A2,Th21;
then x..p - 1 <= len p - 1 by XREAL_1:9;
then len r <= len p - 1 by A2,Th34;
then len r <= len q by A1,Th30;
then
A4: Seg(len r) c= Seg(len q) by FINSEQ_1:5;
let k be Nat;
A5: Seg(len r) = dom r & Seg(len q) = dom q by FINSEQ_1:def 3;
assume
A6: k in dom r;
then k in Seg(len r) by FINSEQ_1:def 3;
then k <= len r by FINSEQ_1:1;
then k <= x..p - 1 by A2,Th34;
then
A7: k + 1 <= x..p by XREAL_1:19;
k < k + 1 by XREAL_1:29;
then
A8: k < x..p by A7,XXREAL_0:2;
r.k = p.k by A2,A6,Th36;
hence q.k = r.k by A1,A6,A4,A5,A8,Th31;
end;
A9: now
reconsider m = x..p - 1 as Element of NAT by A2,Th22;
let k be Nat;
set z = k + m;
assume
A10: k in dom s;
then
A11: s.k = p.(k + x..p) by A2,Def6;
A12: dom s = Seg(len s) by FINSEQ_1:def 3;
then
A13: 1 <= k by A10,FINSEQ_1:1;
then x..p + 1 <= k + x..p by XREAL_1:7;
then
A14: x..p <= k + x..p - 1 by XREAL_1:19;
k <= len s by A10,A12,FINSEQ_1:1;
then k <= len p - x..p by A2,Def6;
then k + x..p <= len p by XREAL_1:19;
then k + x..p - 1 <= len p - 1 by XREAL_1:9;
then
A15: k + x..p - 1 <= len q by A1,Th30;
1 <= x..p by A2,Th21;
then 1 + 1 <= k + x..p by A13,XREAL_1:7;
then
A16: 1 <= k + x..p - 1 by XREAL_1:19;
dom q = Seg(len q) by FINSEQ_1:def 3;
then z in dom q by A16,A15;
then q.z = p.(z + 1) by A1,A14,Th31
.= p.(k + x..p);
hence q.(len r + k) = s.k by A2,A11,Th34;
end;
len r + len s = (x..p - 1) + len s by A2,Th34
.= (x..p - 1) + (len p - x..p) by A2,Def6
.= len p - 1
.= len q by A1,Th30;
then dom q = Seg(len r + len s) by FINSEQ_1:def 3;
hence thesis by A3,A9,FINSEQ_1:def 7;
end;
assume
A17: x in rng p;
assume
A18: p - {x} = (p -| x) ^ (p |-- x);
now
let k;
assume that
A19: k in dom p and
A20: k <> x..p and
A21: p.k = x;
{x..p,k} c= p " {x}
proof
let y be object;
assume
A22: y in {x..p,k};
A23: x in {x} by TARSKI:def 1;
x..p in dom p & p.(x..p) = x by A17,Th19,Th20;
then
A24: x..p in p " {x} by A23,FUNCT_1:def 7;
k in p " {x} by A19,A21,A23,FUNCT_1:def 7;
hence thesis by A22,A24,TARSKI:def 2;
end;
then card{x..p,k} <= card(p " {x}) by NAT_1:43;
then
A25: 2 <= card(p " {x}) by A20,CARD_2:57;
A26: len q = len p - card(p " {x}) by FINSEQ_3:59
.= len p + (- card(p " {x}));
len q = len r + len s by A18,FINSEQ_1:22
.= (x..p - 1) + len s by A17,Th34
.= (x..p - 1) + (len p - x..p) by A17,Def6
.= len p + (- 1);
hence contradiction by A26,A25;
end;
hence thesis by A17,Th27;
end;
theorem
x in rng p & p is one-to-one implies p - {x} = (p -| x) ^ (p |-- x)
proof
assume x in rng p & p is one-to-one;
then p just_once_values x by Th8;
hence thesis by Th54;
end;
theorem Th56:
x in rng p & p - {x} is one-to-one & p - {x} = (p -| x) ^ (p |--
x) implies p is one-to-one
proof
assume that
A1: x in rng p and
A2: p - {x} is one-to-one and
A3: p - {x} = (p -| x) ^ (p |-- x);
set q = p - {x};
let x1,x2 be object;
assume that
A4: x1 in dom p and
A5: x2 in dom p and
A6: p.x1 = p.x2;
reconsider k1 = x1, k2 = x2 as Element of NAT by A4,A5;
A7: p just_once_values x by A1,A3,Th54;
now
per cases by XXREAL_0:1;
suppose
x1 = x..p & x2 = x..p;
hence thesis;
end;
suppose
x1 = x..p & x..p < k2;
hence thesis by A1,A5,A6,A7,Th19,Th26;
end;
suppose
x1 = x..p & k2 < x..p;
hence thesis by A1,A5,A6,A7,Th19,Th26;
end;
suppose
k1 < x..p & x..p = x2;
hence thesis by A1,A4,A6,A7,Th19,Th26;
end;
suppose
A8: k1 < x..p & x..p < k2;
x..p <= len p by A1,Th21;
then k1 < len p by A8,XXREAL_0:2;
then k1 + 1 <= len p by NAT_1:13;
then k1 <= len p - 1 by XREAL_1:19;
then
A9: k1 <= len q by A7,Th30;
k1 in Seg(len p) by A4,FINSEQ_1:def 3;
then 1 <= k1 by FINSEQ_1:1;
then k1 in Seg(len q) by A9;
then
A10: k1 in dom q by FINSEQ_1:def 3;
then
A11: q.k1 = p.k1 by A7,A8,Th31;
consider m2 be Nat such that
A12: k2 = m2 + 1 by A8,NAT_1:6;
reconsider m2 as Element of NAT by ORDINAL1:def 12;
A13: x..p <= m2 by A8,A12,NAT_1:13;
k2 in Seg(len p) by A5,FINSEQ_1:def 3;
then k2 <= len p by FINSEQ_1:1;
then m2 <= len p - 1 by A12,XREAL_1:19;
then
A14: m2 <= len q by A7,Th30;
1 <= x..p by A1,Th21;
then 1 <= m2 by A13,XXREAL_0:2;
then m2 in Seg(len q) by A14;
then
A15: m2 in dom(p - {x}) by FINSEQ_1:def 3;
then q.m2 = p.k2 by A7,A12,A13,Th31;
hence thesis by A2,A6,A8,A10,A13,A15,A11;
end;
suppose
A16: k1 < x..p & k2 < x..p;
A17: x..p <= len p by A1,Th21;
then k2 < len p by A16,XXREAL_0:2;
then k2 + 1 <= len p by NAT_1:13;
then k2 <= len p - 1 by XREAL_1:19;
then
A18: k2 <= len q by A7,Th30;
k2 in Seg(len p) by A5,FINSEQ_1:def 3;
then 1 <= k2 by FINSEQ_1:1;
then k2 in Seg(len q) by A18;
then
A19: k2 in dom q by FINSEQ_1:def 3;
then
A20: p.k2 = (p - {x}).k2 by A7,A16,Th31;
k1 < len p by A16,A17,XXREAL_0:2;
then k1 + 1 <= len p by NAT_1:13;
then k1 <= len p - 1 by XREAL_1:19;
then
A21: k1 <= len q by A7,Th30;
k1 in Seg(len p) by A4,FINSEQ_1:def 3;
then 1 <= k1 by FINSEQ_1:1;
then k1 in Seg(len q) by A21;
then
A22: k1 in dom q by FINSEQ_1:def 3;
then p.k1 = (p - {x}).k1 by A7,A16,Th31;
hence thesis by A2,A6,A22,A19,A20;
end;
suppose
A23: x..p < k1 & x..p < k2;
then consider m2 be Nat such that
A24: k2 = m2 + 1 by NAT_1:6;
consider m1 be Nat such that
A25: k1 = m1 + 1 by A23,NAT_1:6;
reconsider m1, m2 as Element of NAT by ORDINAL1:def 12;
k2 in Seg(len p) by A5,FINSEQ_1:def 3;
then k2 <= len p by FINSEQ_1:1;
then m2 <= len p - 1 by A24,XREAL_1:19;
then
A26: m2 <= len q by A7,Th30;
A27: 1 <= x..p by A1,Th21;
A28: x..p <= m2 by A23,A24,NAT_1:13;
then 1 <= m2 by A27,XXREAL_0:2;
then m2 in Seg(len q) by A26;
then
A29: m2 in dom(p - {x}) by FINSEQ_1:def 3;
then
A30: p.k2 = (p - {x}).m2 by A7,A24,A28,Th31;
k1 in Seg(len p) by A4,FINSEQ_1:def 3;
then k1 <= len p by FINSEQ_1:1;
then m1 <= len p - 1 by A25,XREAL_1:19;
then
A31: m1 <= len q by A7,Th30;
A32: x..p <= m1 by A23,A25,NAT_1:13;
then 1 <= m1 by A27,XXREAL_0:2;
then m1 in Seg(len q) by A31;
then
A33: m1 in dom(p - {x}) by FINSEQ_1:def 3;
then p.k1 = (p - {x}).m1 by A7,A25,A32,Th31;
hence thesis by A2,A6,A25,A24,A33,A29,A30;
end;
suppose
x..p < k1 & x..p = x2;
hence thesis by A1,A4,A6,A7,Th19,Th26;
end;
suppose
A34: x..p < k1 & k2 < x..p;
x..p <= len p by A1,Th21;
then k2 < len p by A34,XXREAL_0:2;
then k2 + 1 <= len p by NAT_1:13;
then k2 <= len p - 1 by XREAL_1:19;
then
A35: k2 <= len q by A7,Th30;
k2 in Seg(len p) by A5,FINSEQ_1:def 3;
then 1 <= k2 by FINSEQ_1:1;
then k2 in Seg(len q) by A35;
then
A36: k2 in dom q by FINSEQ_1:def 3;
then
A37: q.k2 = p.k2 by A7,A34,Th31;
consider m2 be Nat such that
A38: k1 = m2 + 1 by A34,NAT_1:6;
reconsider m2 as Element of NAT by ORDINAL1:def 12;
A39: x..p <= m2 by A34,A38,NAT_1:13;
k1 in Seg len p by A4,FINSEQ_1:def 3;
then k1 <= len p by FINSEQ_1:1;
then m2 <= len p - 1 by A38,XREAL_1:19;
then
A40: m2 <= len q by A7,Th30;
1 <= x..p by A1,Th21;
then 1 <= m2 by A39,XXREAL_0:2;
then m2 in Seg len q by A40;
then
A41: m2 in dom(p - {x}) by FINSEQ_1:def 3;
then q.m2 = p.k1 by A7,A38,A39,Th31;
hence thesis by A2,A6,A34,A36,A39,A41,A37;
end;
end;
hence thesis;
end;
theorem
x in rng p & p is one-to-one implies rng(p -| x) misses rng(p |-- x)
proof
assume that
A1: x in rng p and
A2: p is one-to-one;
p = (p -| x) ^ <* x *> ^ (p |-- x) by A1,Th51;
then rng(p |-- x) misses rng((p -| x) ^ <* x *>) by A2,FINSEQ_3:91;
hence thesis by FINSEQ_1:29,XBOOLE_1:63;
end;
theorem Th58:
A is finite implies ex p st rng p = A & p is one-to-one
proof
defpred P[set] means ex p st rng p = $1 & p is one-to-one;
rng {} = {};
then
A1: P[{}];
now
let B,C;
assume that
B in A and
C c= A;
given p such that
A2: rng p = C and
A3: p is one-to-one;
A4: now
assume
A5: not B in C;
take q = p ^ <* B *>;
thus rng q = rng p \/ rng<* B *> by FINSEQ_1:31
.= C \/ {B} by A2,FINSEQ_1:38;
thus q is one-to-one
proof
let x,y be object;
assume that
A6: x in dom q & y in dom q and
A7: q.x = q.y;
reconsider k = x, l = y as Element of NAT by A6;
A8: now
assume
A9: k in dom p;
given n be Nat such that
A10: n in dom<* B *> and
A11: l = len p + n;
n in {1} by A10,FINSEQ_1:2,38;
then
A12: n = 1 by TARSKI:def 1;
<* B *>.n = q.k by A7,A10,A11,FINSEQ_1:def 7
.= p.k by A9,FINSEQ_1:def 7;
then B = p.k by A12;
hence thesis by A2,A5,A9,FUNCT_1:def 3;
end;
A13: now
assume
A14: l in dom p;
given n be Nat such that
A15: n in dom<* B *> and
A16: k = len p + n;
n in {1} by A15,FINSEQ_1:2,38;
then
A17: n = 1 by TARSKI:def 1;
<* B *>.n = q.l by A7,A15,A16,FINSEQ_1:def 7
.= p.l by A14,FINSEQ_1:def 7;
then B = p.l by A17;
hence thesis by A2,A5,A14,FUNCT_1:def 3;
end;
A18: now
given m1 being Nat such that
A19: m1 in dom<* B *> and
A20: k = len p + m1;
m1 in {1} by A19,FINSEQ_1:2,def 8;
then
A21: m1 = 1 by TARSKI:def 1;
given m2 being Nat such that
A22: m2 in dom<* B *> and
A23: l = len p + m2;
m2 in {1} by A22,FINSEQ_1:2,def 8;
hence thesis by A20,A23,A21,TARSKI:def 1;
end;
now
assume
A24: k in dom p & l in dom p;
then q.k = p.k & q.l = p.l by FINSEQ_1:def 7;
hence thesis by A3,A7,A24;
end;
hence thesis by A6,A8,A13,A18,FINSEQ_1:25;
end;
end;
now
assume
A25: B in C;
take q = p;
thus rng q = C \/ {B} & q is one-to-one by A2,A3,A25,ZFMISC_1:40;
end;
hence ex p st rng p = C \/ {B} & p is one-to-one by A4;
end;
then
A26: for B,C being set st B in A & C c= A & P[C] holds P[C \/ {B}];
assume
A27: A is finite;
thus P[A] from FINSET_1:sch 2(A27,A1,A26);
end;
theorem Th59:
rng p c= dom p & p is one-to-one implies rng p = dom p
proof
defpred P[Nat] means for q st len q = $1 & rng q c= dom q & q is one-to-one
holds rng q = dom q;
A1: len p = len p;
now
let k;
assume
A2: for q st len q = k & rng q c= dom q & q is one-to-one holds rng q = dom q;
let q;
assume that
A3: len q = k + 1 and
A4: rng q c= dom q and
A5: q is one-to-one;
A6: dom q = Seg(k + 1) by A3,FINSEQ_1:def 3;
dom q c= rng q
proof
let x be object;
assume
A7: x in dom q;
then reconsider n = x as Element of NAT;
per cases;
suppose
A8: k + 1 in rng q;
now
per cases;
suppose
n = k + 1;
hence thesis by A8;
end;
suppose
n <> k + 1;
then not x in {k + 1} by TARSKI:def 1;
then x in Seg(k + 1) \ {k + 1} by A6,A7,XBOOLE_0:def 5;
then
A9: x in Seg k by FINSEQ_1:10;
set r = q - {k + 1};
A10: len r = (k + 1) - 1 by A3,A5,A8,FINSEQ_3:90;
then
A11: dom r = Seg k by FINSEQ_1:def 3;
A12: rng r = rng q \ {k + 1} by FINSEQ_3:65;
then rng r c= Seg(k + 1) \ {k + 1} by A4,A6,XBOOLE_1:33;
then rng r c= dom r by A11,FINSEQ_1:10;
then rng r = dom r by A2,A5,A10,FINSEQ_3:87;
hence thesis by A12,A11,A9;
end;
end;
hence thesis;
end;
suppose
A13: not k + 1 in rng q;
A14: rng q c= Seg k
proof
let x be object;
assume
A15: x in rng q;
then not x in {k + 1} by A13,TARSKI:def 1;
then x in Seg(k + 1) \ {k + 1} by A4,A6,A15,XBOOLE_0:def 5;
hence thesis by FINSEQ_1:10;
end;
A16: k + 1 in Seg(k + 1) by FINSEQ_1:4;
then
A17: q.(k + 1) in rng q by A6,FUNCT_1:def 3;
reconsider r = q | Seg k as FinSequence by FINSEQ_1:15;
A18: dom r c= dom q & k < k + 1 by RELAT_1:60,XREAL_1:29;
A19: len r = k by A3,FINSEQ_3:53;
then
A20: dom r = Seg k by FINSEQ_1:def 3;
rng r c= rng q & r is one-to-one by A5,FUNCT_1:52,RELAT_1:70;
then rng r = dom r by A2,A19,A20,A14,XBOOLE_1:1;
then consider x being object such that
A21: x in dom r and
A22: r.x = q.(k + 1) by A20,A14,A17,FUNCT_1:def 3;
reconsider n = x as Element of NAT by A21;
r.x = q.x & n <= k by A20,A21,FINSEQ_1:1,FUNCT_1:49;
hence thesis by A5,A6,A16,A21,A22,A18;
end;
end;
hence rng q = dom q by A4;
end;
then
A23: for k st P[k] holds P[k+1];
now
let q;
assume
A24: len q = 0;
assume that
rng q c= dom q and
q is one-to-one;
q = {} by A24;
hence rng q = dom q;
end;
then
A25: P[0];
for k holds P[k] from NAT_1:sch 2(A25,A23);
hence thesis by A1;
end;
theorem Th60:
rng p = dom p implies p is one-to-one
proof
defpred P[Nat] means for p st len p = $1 & rng p = dom p holds p is
one-to-one;
A1: len p = len p;
A2: now
let k;
assume
A3: P[k];
thus P[k+1]
proof
set x = k + 1;
let p;
set q = p - {k + 1};
assume that
A4: len p = k + 1 and
A5: rng p = dom p;
A6: dom p = Seg(k + 1) by A4,FINSEQ_1:def 3;
then
A7: k + 1 in rng p by A5,FINSEQ_1:4;
now
rng q = Seg(k + 1) \ {k + 1} by A5,A6,FINSEQ_3:65
.= Seg k by FINSEQ_1:10;
then card(rng q) = k by FINSEQ_1:57;
then
A8: card k = card(rng q);
p.(x..p) = x by A5,A6,Th19,FINSEQ_1:4;
then
A9: p.(x..p) in {k + 1} by TARSKI:def 1;
let l;
assume that
A10: l in dom p and
A11: l <> (k + 1)..p and
A12: p.l = k + 1;
A13: card{x..p,l} = 2 by A11,CARD_2:57;
p.l in {k + 1} by A12,TARSKI:def 1;
then
A14: l in p " {x} by A10,FUNCT_1:def 7;
x..p in dom p by A5,A6,Th20,FINSEQ_1:4;
then x..p in p " {x} by A9,FUNCT_1:def 7;
then {x..p,l} c= p " {k + 1} by A14,ZFMISC_1:32;
then
A15: 2 <= card(p " {k + 1}) by A13,NAT_1:43;
len q = (k + 1) - card(p " {k + 1}) by A4,FINSEQ_3:59;
then
2 + len q <= card(p " {x}) + ((k + 1) - card(p " {k + 1})) by A15,
XREAL_1:6;
then len q + 1 + 1 <= k + 1;
then len q + 1 <= k by XREAL_1:6;
then
A16: len q <= k - 1 by XREAL_1:19;
dom q = Seg(len q) by FINSEQ_1:def 3;
then card Segm k c= card(dom q) &
card Segm len q = card(dom q) by CARD_1:12,FINSEQ_1:57,A8;
then k <= len q by NAT_1:40;
then k <= k - 1 by A16,XXREAL_0:2;
then k + 1 <= k + 0 by XREAL_1:19;
hence contradiction by XREAL_1:6;
end;
then
A17: p just_once_values k + 1 by A7,Th27;
then
A18: len q = (k + 1) - 1 by A4,Th30
.= k;
A19: q = (p -| (k + 1)) ^ (p |-- (k + 1)) by A17,Th54;
rng q = Seg(k + 1) \ {k + 1} by A5,A6,FINSEQ_3:65
.= Seg k by FINSEQ_1:10;
then dom q = rng q by A18,FINSEQ_1:def 3;
hence thesis by A3,A7,A18,A19,Th56;
end;
end;
A20: P[0]
proof
let p;
assume len p = 0;
then p = {};
hence thesis;
end;
for k holds P[k] from NAT_1:sch 2(A20,A2);
hence thesis by A1;
end;
theorem
rng p = rng q & len p = len q & q is one-to-one implies p is one-to-one
proof
assume that
A1: rng p = rng q and
A2: len p = len q and
A3: q is one-to-one;
A4: rng p = dom(q") by A1,A3,FUNCT_1:33;
then
A5: dom (q" * p) = dom p by RELAT_1:27
.= Seg(len p) by FINSEQ_1:def 3;
then reconsider r = q" * p as FinSequence by FINSEQ_1:def 2;
rng r = rng(q") by A4,RELAT_1:28
.= dom q by A3,FUNCT_1:33
.= Seg(len q) by FINSEQ_1:def 3;
then r is one-to-one by A2,A5,Th60;
hence thesis by A4,FUNCT_1:26;
end;
Lm1: for A,B being finite set, f being Function of A,B st card A = card B &
f is onto holds f is one-to-one
proof
let A,B be finite set, f be Function of A,B;
assume that
A1: card A = card B and
A2: f is onto;
a2: rng f = B by A2,FUNCT_2:def 3;
A3: A,B are_equipotent by A1,CARD_1:5;
consider p such that
A4: rng p = A and
A5: p is one-to-one by Th58;
dom p,p .: (dom p) are_equipotent by A5,CARD_1:33;
then dom p,A are_equipotent by A4,RELAT_1:113;
then
A6: dom p,B are_equipotent by A3,WELLORD2:15;
reconsider X = dom p as finite set;
consider q such that
A7: rng q = B and
A8: q is one-to-one by Th58;
A9: dom q = Seg(len q) by FINSEQ_1:def 3;
dom q,q .: (dom q) are_equipotent by A8,CARD_1:33;
then dom q,B are_equipotent by A7,RELAT_1:113;
then dom p,dom q are_equipotent by A6,WELLORD2:15;
then card X = card(Seg(len q)) by A9,CARD_1:5
.= len q by FINSEQ_1:57;
then
A10: len q = card Seg len p by FINSEQ_1:def 3
.= len p by FINSEQ_1:57;
now
per cases;
suppose
B = {};
hence thesis;
end;
suppose
A11: B <> {};
then rng p = dom f by A4,FUNCT_2:def 1;
then
A12: rng(f * p) = B by a2,RELAT_1:28
.= dom(q") by A7,A8,FUNCT_1:33;
dom(q") = rng q by A8,FUNCT_1:33;
then rng f c= dom(q") by A7,RELAT_1:def 19;
then dom(q" * f) = dom f by RELAT_1:27;
then rng p = dom(q" * f) by A4,A11,FUNCT_2:def 1;
then
A13: dom(q" * f * p) = dom p by RELAT_1:27
.= Seg(len p) by FINSEQ_1:def 3;
then reconsider g = q" * f * p as FinSequence by FINSEQ_1:def 2;
g = q" * (f * p) by RELAT_1:36;
then rng g = rng(q") by A12,RELAT_1:28
.= dom q by A8,FUNCT_1:33
.= Seg(len q) by FINSEQ_1:def 3;
then
A14: g is one-to-one by A10,A13,Th60;
q * g = q * (q " * (f * p)) by RELAT_1:36
.= q * q" * (f * p) by RELAT_1:36
.= id(rng q) * (f * p) by A8,FUNCT_1:39
.= id(rng q) * f * p by RELAT_1:36
.= f * p by a2,A7,RELAT_1:54;
then q * g * p" = f * (p * p") by RELAT_1:36
.= f * id(rng p) by A5,FUNCT_1:39
.= f * id(dom f) by A4,A11,FUNCT_2:def 1
.= f by RELAT_1:52;
hence thesis by A5,A8,A14;
end;
end;
hence thesis;
end;
theorem Th62:
p is one-to-one iff card rng p = len p
proof
thus p is one-to-one implies card rng p = len p
proof
assume p is one-to-one;
then dom p,p .: (dom p) are_equipotent by CARD_1:33;
then dom p,rng p are_equipotent by RELAT_1:113;
then Seg len p, rng p are_equipotent by FINSEQ_1:def 3;
then card Seg len p = card rng p by CARD_1:5;
hence thesis by FINSEQ_1:57;
end;
reconsider f = p as Function of dom p, rng p by FUNCT_2:1;
reconsider B = dom p as finite set;
assume card rng p = len p;
then card rng p = card Seg len p by FINSEQ_1:57;
then
A1: card rng p = card B by FINSEQ_1:def 3;
f is onto by FUNCT_2:def 3;
hence thesis by Lm1,A1;
end;
:: If you are looking for theorem
:: rng p = rng q & p is one-to-one & q is one-to-one implies len p = len q,
:: it is placed in RLVECT_1 under number 106.
reserve f for Function of A,B;
Lemacik:
for A,B being finite set, f being Function of A,B st
card A = card B & f is one-to-one holds f is onto
proof
let A,B be finite set;
let f be Function of A,B;
assume that
A1: card A = card B and
A2: f is one-to-one;
A3: A,B are_equipotent by A1,CARD_1:5;
consider p such that
A4: rng p = A and
A5: p is one-to-one by Th58;
dom p,p .: (dom p) are_equipotent by A5,CARD_1:33;
then dom p,A are_equipotent by A4,RELAT_1:113;
then
A6: dom p,B are_equipotent by A3,WELLORD2:15;
consider q such that
A7: rng q = B and
A8: q is one-to-one by Th58;
A9: dom q = Seg(len q) by FINSEQ_1:def 3;
dom q,q .: (dom q) are_equipotent by A8,CARD_1:33;
then dom q,B are_equipotent by A7,RELAT_1:113;
then dom p,dom q are_equipotent by A6,WELLORD2:15;
then card dom p = card Seg len q by A9,CARD_1:5
.= len q by FINSEQ_1:57; then
A10: len q = card Seg len p by FINSEQ_1:def 3
.= len p by FINSEQ_1:57;
per cases;
suppose
B = {}; then
rng f = B;
hence thesis by FUNCT_2:def 3;
end;
suppose
A11: B <> {};
dom(q") = rng q by A8,FUNCT_1:33;
then rng f c= dom(q") by A7,RELAT_1:def 19;
then dom(q" * f) = dom f by RELAT_1:27;
then rng p = dom(q" * f) by A4,A11,FUNCT_2:def 1;
then
A12: dom(q" * f * p) = dom p by RELAT_1:27
.= Seg(len p) by FINSEQ_1:def 3;
then reconsider g = q" * f * p as FinSequence by FINSEQ_1:def 2;
g = q" * (f * p) by RELAT_1:36;
then rng g c= rng(q") by RELAT_1:26;
then rng g c= dom q by A8,FUNCT_1:33;
then rng g c= dom g by A10,A12,FINSEQ_1:def 3;
then rng g = dom g by A2,A5,A8,Th59;
then rng g = dom q by A10,A12,FINSEQ_1:def 3;
then
A13: rng(q * g) = B by A7,RELAT_1:28;
A14: rng f c= rng q by A7,RELAT_1:def 19;
A15: rng p = dom f by A4,A11,FUNCT_2:def 1;
q * g = q * (q " * (f * p)) by RELAT_1:36
.= q * q" * (f * p) by RELAT_1:36
.= id(rng q) * (f * p) by A8,FUNCT_1:39
.= id(rng q) * f * p by RELAT_1:36
.= f * p by A14,RELAT_1:53;
then rng f = B by A13,A15,RELAT_1:28;
hence thesis by FUNCT_2:def 3;
end;
end;
theorem
for A,B being finite set, f being Function of A,B st
card A = card B holds f is one-to-one iff f is onto by Lemacik,Lm1;
::$CT
::$N Dirichlet Principle
::$N Pigeon Hole Principle
theorem
card B in card A & B <> {} implies ex x,y st x in A & y in A & x <> y
& f.x = f.y
proof
assume that
A1: card B in card A and
A2: B <> {} and
A3: for x,y st x in A & y in A & x <> y holds f.x <> f.y;
A4: dom f = A by A2,FUNCT_2:def 1;
then for x,y being object holds x in dom f & y in dom f & f.x = f.y
implies x = y by A3;
then f is one-to-one;
then dom f,f .: (dom f) are_equipotent by CARD_1:33;
then dom f,rng f are_equipotent by RELAT_1:113;
then
A5: card A = card(rng f) by A4,CARD_1:5;
rng f c= B by RELAT_1:def 19;
then card A c= card B by A5,CARD_1:11;
hence contradiction by A1,CARD_1:4;
end;
theorem Th66:
card A in card B implies ex x st x in B & for y st y in A holds f.y <> x
proof
assume that
A1: card A in card B and
A2: for x st x in B ex y st y in A & f.y = x;
A3: dom f = A by A1,CARD_1:27,FUNCT_2:def 1;
rng f = B
proof
thus rng f c= B by RELAT_1:def 19;
let x be object;
assume x in B;
then ex y st y in A & f.y = x by A2;
hence thesis by A3,FUNCT_1:def 3;
end;
then card B c= card A by A3,CARD_1:12;
hence thesis by A1,CARD_1:4;
end;
begin :: Addenda
:: from TOPREAL4
theorem
for D being non empty set, f being FinSequence of D,
p being Element of D holds (f^<*p*>)/.(len f + 1) = p
proof
let D be non empty set, f be FinSequence of D, p be Element of D;
len(f^<*p*>) = len f + len<*p*> by FINSEQ_1:22;
then 1 <= len f + 1 & len f + 1 <= len(f^<*p*>) by FINSEQ_1:39,NAT_1:11;
then len f + 1 in dom(f^<*p*>) by FINSEQ_3:25;
hence (f^<*p*>)/.(len f + 1) = (f^<*p*>).(len f + 1) by PARTFUN1:def 6
.= p by FINSEQ_1:42;
end;
:: from GROUP_5
theorem
for E being non empty set, p,q being FinSequence of E st k in dom p
holds (p ^ q)/.k = p/.k
proof
let E be non empty set, p,q be FinSequence of E;
assume
A1: k in dom p;
then k in dom(p ^ q) by FINSEQ_3:22;
hence (p ^ q)/.k = (p ^ q).k by PARTFUN1:def 6
.= p.k by A1,FINSEQ_1:def 7
.= p/.k by A1,PARTFUN1:def 6;
end;
theorem
for E being non empty set, p,q being FinSequence of E st k in dom q
holds (p ^ q)/.(len p + k) = q/.k
proof
let E be non empty set, p,q be FinSequence of E;
assume
A1: k in dom q;
then len p + k in dom(p ^ q) by FINSEQ_1:28;
hence (p ^ q)/.(len p + k) = (p ^ q).(len p + k) by PARTFUN1:def 6
.= q.k by A1,FINSEQ_1:def 7
.= q/.k by A1,PARTFUN1:def 6;
end;
:: from TOPREAL1
theorem
for m being Nat for D being set, p being FinSequence of D st
a in dom(p|m) holds (p|m qua FinSequence of D)/.a = p/.a
proof
let m be Nat;
let D be set, p be FinSequence of D;
assume
A1: a in dom(p|m);
then a in dom p /\ (Seg m) by RELAT_1:61;
then
A2: a in dom p by XBOOLE_0:def 4;
thus (p|m)/.a = (p|Seg m).a by A1,PARTFUN1:def 6
.= p.a by A1,FUNCT_1:47
.= p/.a by A2,PARTFUN1:def 6;
end;
:: from GOBOARD1
theorem Th71:
for D being set, f being FinSequence of D, n,m st n in dom f & m in
Seg n holds m in dom f & (f|n)/.m = f/.m
proof
let D be set, f be FinSequence of D, n,m;
assume that
A1: n in dom f and
A2: m in Seg n;
dom f = Seg len f & n<=len f by A1,FINSEQ_1:def 3,FINSEQ_3:25;
then
A3: Seg n c= dom f by FINSEQ_1:5;
hence m in dom f by A2;
A4: Seg n = dom f /\ Seg n by A3,XBOOLE_1:28
.= dom(f|n) by RELAT_1:61;
hence (f|n)/.m = (f|n).m by A2,PARTFUN1:def 6
.= f.m by A2,A4,FUNCT_1:47
.= f/.m by A2,A3,PARTFUN1:def 6;
end;
:: from VECTSP_9, 2006.01.06, A.T.
theorem
for X being finite set st n <= card X holds ex A being finite Subset
of X st card A = n
proof
let X be finite set such that
A1: n <= card X;
consider p being FinSequence such that
A2: rng p = X and
A3: p is one-to-one by Th58;
reconsider q = p|Seg n as FinSequence by FINSEQ_1:15;
n <= len p by A1,A2,A3,Th62;
then
A4: len q = n by FINSEQ_1:17;
reconsider A = rng q as Subset of X by A2,RELAT_1:70;
q is one-to-one by A3,FUNCT_1:52;
then card A = n by A4,Th62;
hence thesis;
end;
reserve f for Function;
theorem
f is one-to-one & x in rng f implies card Coim (f,x) = 1 by Th8,Def2;
:: form SCMPDS_1, 2006.03.24, A.T.
definition
let x1,x2,x3,x4 be object;
func <*x1,x2,x3,x4*> -> set equals
<*x1,x2,x3*>^<*x4*>;
correctness;
let x5 be object;
func <*x1,x2,x3,x4,x5*> -> set equals
<*x1,x2,x3*>^<*x4,x5*>;
correctness;
end;
registration
let x1,x2,x3,x4 be object;
cluster <*x1,x2,x3,x4*> -> non empty Function-like Relation-like;
coherence;
let x5 be object;
cluster <*x1,x2,x3,x4,x5*> -> non empty Function-like Relation-like;
coherence;
end;
registration
let x1,x2,x3,x4 be object;
cluster <*x1,x2,x3,x4*> -> FinSequence-like;
coherence;
let x5 be object;
cluster <*x1,x2,x3,x4,x5*> -> FinSequence-like;
coherence;
end;
definition
let D be non empty set,x1,x2,x3,x4 be Element of D;
redefine func <* x1,x2,x3,x4*> -> FinSequence of D; :: redefines <* (FINSEQ_4, definition)
coherence
proof
<*x1,x2,x3,x4*>=<* x1,x2,x3*>^<*x4*>;
hence thesis;
end;
end;
definition
let D be non empty set,x1,x2,x3,x4,x5 be Element of D;
redefine func <*x1,x2,x3,x4,x5*> -> FinSequence of D; :: redefines <* (FINSEQ_4, definition)
coherence
proof
<*x1,x2,x3,x4,x5*>=<* x1,x2,x3*>^<*x4,x5*>;
hence thesis;
end;
end;
reserve x1,x2,x3,x4,x5 for object;
theorem Th74:
<*x1,x2,x3,x4*>=<*x1,x2,x3*>^<*x4*> & <*x1,x2,x3,x4*>=<*x1,x2*>^
<*x3,x4*> & <*x1,x2,x3,x4*>=<*x1*>^<*x2,x3,x4*> & <*x1,x2,x3,x4*>=<*x1*>^<*x2*>
^<*x3*>^<*x4*>
proof
thus <*x1,x2,x3,x4*>=<*x1,x2,x3*>^<*x4*>;
thus <*x1,x2,x3,x4*>=<*x1,x2*>^<*x3,x4*> by FINSEQ_1:32;
hence <*x1,x2,x3,x4*>=<*x1*>^(<*x2*>^<*x3,x4*>) by FINSEQ_1:32
.=<*x1*>^<*x2,x3,x4*> by FINSEQ_1:43;
thus thesis;
end;
theorem Th75:
<*x1,x2,x3,x4,x5*>=<*x1,x2,x3*>^<*x4,x5*> & <*x1,x2,x3,x4,x5*>=
<*x1,x2,x3,x4*>^<*x5*> & <*x1,x2,x3,x4,x5*>=<*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>
& <*x1,x2,x3,x4,x5*>=<*x1,x2*>^<*x3,x4,x5*> & <*x1,x2,x3,x4,x5*>=<*x1*>^<*x2,x3
,x4,x5*>
proof
thus <*x1,x2,x3,x4,x5*>=<*x1,x2,x3*>^<*x4,x5*>;
thus
A1: <*x1,x2,x3,x4,x5*>=<*x1,x2,x3,x4*>^<*x5*> by FINSEQ_1:32;
thus <*x1,x2,x3,x4,x5*>=<*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*> by FINSEQ_1:32;
thus <*x1,x2,x3,x4,x5*>=<*x1,x2*>^(<*x3*>^<*x4*>)^<*x5*> by A1,FINSEQ_1:32
.=<*x1,x2*>^<*x3,x4,x5*> by FINSEQ_1:32;
hence <*x1,x2,x3,x4,x5*>=<*x1*>^(<*x2*>^<*x3,x4,x5*>) by FINSEQ_1:32
.=<*x1*>^<*x2,x3,x4,x5*> by Th74;
end;
reserve p for FinSequence;
theorem Th76:
p = <*x1,x2,x3,x4*> iff len p = 4 & p.1 = x1 & p.2 = x2 & p.3=x3 & p.4= x4
proof
thus p = <*x1,x2,x3,x4*> implies len p = 4 & p.1 = x1 & p.2 = x2 & p.3 = x3
& p.4 = x4
proof
set p3=<*x1,x2,x3*>;
assume
A1: p =<*x1,x2,x3,x4*>;
hence len p =len <*x1,x2,x3*> + len <*x4*> by FINSEQ_1:22
.=3 + len <*x4*> by FINSEQ_1:45
.=3+1 by FINSEQ_1:40
.=4;
A2: dom p3 ={1,2,3} by FINSEQ_1:89,FINSEQ_3:1;
then 1 in dom p3 by ENUMSET1:def 1;
hence p.1 = p3.1 by A1,FINSEQ_1:def 7
.=x1;
2 in dom p3 by A2,ENUMSET1:def 1;
hence p.2 = p3.2 by A1,FINSEQ_1:def 7
.=x2;
3 in dom p3 by A2,ENUMSET1:def 1;
hence p.3 = p3.3 by A1,FINSEQ_1:def 7
.=x3;
1 in {1} by TARSKI:def 1;
then
A3: 1 in dom <*x4*> by FINSEQ_1:2,def 8;
thus p.4 = (p3^<*x4*>).(3+1) by A1
.=(p3^<*x4*>).(len p3 + 1) by FINSEQ_1:45
.= <*x4*>.1 by A3,FINSEQ_1:def 7
.= x4;
end;
assume that
A4: len p = 4 and
A5: p.1 = x1 and
A6: p.2 = x2 and
A7: p.3 = x3 and
A8: p.4=x4;
A9: for k be Nat st k in dom <*x1,x2,x3*> holds p.k=<*x1,x2,x3*>.k
proof
A10: len <*x1,x2,x3*> = 3 by FINSEQ_1:45;
let k be Nat;
assume k in dom <*x1,x2,x3*>;
then
A11: k in {1,2,3} by A10,FINSEQ_1:def 3,FINSEQ_3:1;
per cases by A11,ENUMSET1:def 1;
suppose
k=1;
hence thesis by A5;
end;
suppose
k=2;
hence thesis by A6;
end;
suppose
k=3;
hence thesis by A7;
end;
end;
A12: for k be Nat st k in dom <*x4*> holds p.( (len <*x1,x2,x3*>) + k) = <*
x4*>.k
proof
let k be Nat;
assume k in dom <*x4*>;
then k in {1} by FINSEQ_1:2,def 8;
then
A13: k = 1 by TARSKI:def 1;
hence p.( (len <*x1,x2,x3*>) + k) = p.(3+1) by FINSEQ_1:45
.=<*x4*>.k by A8,A13;
end;
dom p = Seg(3+1) by A4,FINSEQ_1:def 3
.= Seg((len <*x1,x2,x3*>) + 1) by FINSEQ_1:45
.= Seg((len <*x1,x2,x3*>) + len <*x4*>) by FINSEQ_1:39;
hence thesis by A9,A12,FINSEQ_1:def 7;
end;
registration
let a,b,c,d be object;
reduce <*a,b,c,d*>.1 to a;
reducibility by Th76;
reduce <*a,b,c,d*>.2 to b;
reducibility by Th76;
reduce <*a,b,c,d*>.3 to c;
reducibility by Th76;
reduce <*a,b,c,d*>.4 to d;
reducibility by Th76;
end;
::$CT
theorem Th77:
p = <*x1,x2,x3,x4,x5*> iff
len p = 5 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5
proof
set p4=<*x1,x2,x3,x4*>;
thus p = <*x1,x2,x3,x4,x5*> implies len p = 5 & p.1 = x1 & p.2 = x2 & p.3 =
x3 & p.4 = x4 & p.5 = x5
proof
set p4=<*x1,x2,x3,x4*>;
1 in {1} by TARSKI:def 1;
then
A1: 1 in dom <*x5*> by FINSEQ_1:2,def 8;
assume
A2: p =<*x1,x2,x3,x4,x5*>;
then
A3: p = (p4^<*x5*>) by Th75;
thus len p = len (<*x1,x2,x3,x4*>^<*x5*>) by A2,Th75
.=len <*x1,x2,x3,x4*> + len <*x5*> by FINSEQ_1:22
.=4 + len <*x5*> by Th76
.=4+1 by FINSEQ_1:40
.=5;
A4: dom p4 ={1,2,3,4} by FINSEQ_1:89,FINSEQ_3:2;
then 1 in dom p4 by ENUMSET1:def 2;
hence p.1 = p4.1 by A3,FINSEQ_1:def 7
.=x1;
2 in dom p4 by A4,ENUMSET1:def 2;
hence p.2 = p4.2 by A3,FINSEQ_1:def 7
.=x2;
3 in dom p4 by A4,ENUMSET1:def 2;
hence p.3 = p4.3 by A3,FINSEQ_1:def 7
.=x3;
4 in dom p4 by A4,ENUMSET1:def 2;
hence p.4 = p4.4 by A3,FINSEQ_1:def 7
.=x4;
thus p.5 = (p4^<*x5*>).(4+1) by A2,Th75
.=(p4^<*x5*>).(len p4+ 1) by Th76
.= <*x5*>.1 by A1,FINSEQ_1:def 7
.= x5;
end;
assume that
A5: len p = 5 and
A6: p.1 = x1 and
A7: p.2 = x2 and
A8: p.3 = x3 and
A9: p.4=x4 and
A10: p.5=x5;
A11: for k be Nat st k in dom p4 holds p.k=p4.k
proof
A12: len p4 = 4 by Th76;
let k be Nat;
assume k in dom p4;
then
A13: k in {1,2,3,4} by A12,FINSEQ_1:def 3,FINSEQ_3:2;
per cases by A13,ENUMSET1:def 2;
suppose
k=1;
hence thesis by A6;
end;
suppose
k=2;
hence thesis by A7;
end;
suppose
k=3;
hence thesis by A8;
end;
suppose
k=4;
hence thesis by A9;
end;
end;
A14: for k be Nat st k in dom <*x5*> holds p.( len p4 + k) = <*x5*>.k
proof
let k be Nat;
assume k in dom <*x5*>;
then k in {1} by FINSEQ_1:2,def 8;
then
A15: k = 1 by TARSKI:def 1;
hence p.( len p4 + k) = p.(4+1) by Th76
.=<*x5*>.k by A10,A15;
end;
dom p = Seg(4+1) by A5,FINSEQ_1:def 3
.= Seg(len p4 + 1) by Th76
.= Seg(len p4 + len <*x5*>) by FINSEQ_1:39;
hence p=p4^<*x5*> by A11,A14,FINSEQ_1:def 7
.=<*x1,x2,x3,x4,x5*> by Th75;
end;
registration
let a,b,c,d,e be object;
reduce <*a,b,c,d,e*>.1 to a;
reducibility by Th77;
reduce <*a,b,c,d,e*>.2 to b;
reducibility by Th77;
reduce <*a,b,c,d,e*>.3 to c;
reducibility by Th77;
reduce <*a,b,c,d,e*>.4 to d;
reducibility by Th77;
reduce <*a,b,c,d,e*>.5 to e;
reducibility by Th77;
end;
reserve ND for non empty set;
reserve y1,y2,y3,y4,y5 for Element of ND;
::$CT
theorem
<*y1,y2,y3,y4*>/.1 = y1 & <*y1,y2,y3,y4*>/.2 = y2 & <*y1,y2,y3,y4*>/.3
= y3 & <*y1,y2,y3,y4*>/.4=y4
proof
set s = <* y1,y2,y3,y4 *>;
A1: 2 in {1,2,3,4} & 3 in {1,2,3,4} by FINSEQ_3:2;
A2: s.2 = y2 & s.3 = y3;
A3: 4 in {1,2,3,4} by FINSEQ_3:2;
A4: s.4 = y4 & 1 in {1,2,3,4} by FINSEQ_3:2;
dom s = {1,2,3,4} & s.1 = y1 by FINSEQ_1:89,FINSEQ_3:2;
hence thesis by A2,A4,A1,A3,PARTFUN1:def 6;
end;
theorem
<*y1,y2,y3,y4,y5*>/.1 = y1 & <*y1,y2,y3,y4,y5*>/.2 = y2 & <*y1,y2,y3,
y4,y5*>/.3 = y3 & <*y1,y2,y3,y4,y5*>/.4=y4 & <*y1,y2,y3,y4,y5*>/.5=y5
proof
set s = <* y1,y2,y3,y4,y5 *>, i5={1,2,3,4,5};
A1: 1 in i5 & 2 in i5 by FINSEQ_3:3;
A2: 3 in i5 & 4 in i5 by FINSEQ_3:3;
A3: s.4 = y4 & s.5=y5;
A4: s.2 = y2 & s.3 = y3;
A5: 5 in i5 by FINSEQ_3:3;
dom s =i5 & s.1 = y1 by FINSEQ_1:89,FINSEQ_3:3;
hence thesis by A4,A3,A1,A2,A5,PARTFUN1:def 6;
end;
:: form GOBOARD1, 2007.07.22, A.T.
scheme
Sch1{D()->non empty set, N()->Nat, P[object,object]}:
ex f being FinSequence of D(
) st len f = N() & for n st n in Seg N() holds P[n,f/.n]
provided
A1: for n st n in Seg N() ex d being Element of D() st P[n,d];
defpred P1[object,object] means P[$1,$2] & $2 in D();
reconsider X=D() as set;
A2: now
let x be object;
assume
A3: x in Seg N();
then reconsider x9=x as Element of NAT;
consider d be Element of D() such that
A4: P[x9,d] by A1,A3;
reconsider y=d as object;
take y;
thus y in X & P1[x,y] by A4;
end;
consider f be Function such that
A5: dom f = Seg N() & rng f c= X & for x be object st x in Seg N() holds P1
[x,f.x] from FUNCT_1:sch 6(A2);
reconsider f as FinSequence by A5,FINSEQ_1:def 2;
reconsider f as FinSequence of D() by A5,FINSEQ_1:def 4;
take f;
N() in NAT by ORDINAL1:def 12;
hence len f = N() by A5,FINSEQ_1:def 3;
let n;
assume
A6: n in Seg N();
then P[n,f.n] by A5;
hence thesis by A5,A6,PARTFUN1:def 6;
end;
:: form SCMFSA_7, 2007.07.22, A.T.
theorem Th80:
for D being non empty set, p,q being FinSequence of D st p c= q
holds ex p9 being FinSequence of D st p ^ p9 = q
proof
let D be non empty set, p,q be FinSequence of D;
assume
A1: p c= q;
dom p = Seg len p & dom q = Seg len q by FINSEQ_1:def 3;
then Seg len p c= Seg len q by A1,GRFUNC_1:2;
then len p <= len q by FINSEQ_1:5;
then reconsider N = len q - len p as Element of NAT by INT_1:3,XREAL_1:48;
defpred P[Nat,set] means q/.(len p + $1) = $2;
A2: for n being Nat st n in Seg N ex d being Element of D st P[n,d];
consider f being FinSequence of D such that
A3: len f = N and
A4: for n being Nat st n in Seg N holds P[n,f/.n] from Sch1(A2);
take f;
A5: len (p ^ f) = len p + N by A3,FINSEQ_1:22
.= len q;
now
let k be Nat;
assume that
A6: 1 <= k and
A7: k <= len (p ^ f);
k in Seg len q by A5,A6,A7;
then
A8: k in dom q by FINSEQ_1:def 3;
per cases;
suppose
k <= len p;
then k in Seg len p by A6;
then
A9: k in dom p by FINSEQ_1:def 3;
hence (p ^ f).k = p.k by FINSEQ_1:def 7
.= q.k by A1,A9,GRFUNC_1:2;
end;
suppose
A10: len p < k;
then k - len p > 0 by XREAL_1:50;
then reconsider kk = k - len p as Element of NAT by INT_1:3;
k <= len p + len f by A7,FINSEQ_1:22;
then
A11: kk <= len p + len f - len p by XREAL_1:9;
k - len p >= 0 + 1 by A10,INT_1:7,XREAL_1:50;
then
A12: kk in Seg len f by A11;
then
A13: kk in dom f by FINSEQ_1:def 3;
thus (p ^ f).k = f.kk by A7,A10,FINSEQ_1:24
.= f/.kk by A13,PARTFUN1:def 6
.= q/.(len p + kk) by A3,A4,A12
.= q.k by A8,PARTFUN1:def 6;
end;
end;
hence thesis by A5;
end;
theorem
for D being non empty set, p,q being FinSequence of D, i being Element
of NAT st p c= q & 1 <= i & i <= len p holds q.i = p.i
proof
let D be non empty set, p,q be FinSequence of D, i be Element of NAT;
assume p c= q;
then
A1: ex p9 being FinSequence of D st p ^ p9 = q by Th80;
assume 1 <= i & i <= len p;
hence thesis by A1,FINSEQ_1:64;
end;
:: form GOBOARD2, 2008.03.08, A.T.
scheme
PiLambdaD{D()-> non empty set, l()->Nat, F(set)-> Element of D()}: ex g
being FinSequence of D() st len g=l() & for n being Nat st n in dom g holds g/.
n=F(n) proof
consider g being FinSequence of D() such that
A1: len g=l() & for n be Nat st n in dom g holds g.n=F(n) from FINSEQ_2:
sch 1;
take g;
thus len g=l() by A1;
let n be Nat;
assume
A2: n in dom g;
then g.n = F(n) by A1;
hence thesis by A2,PARTFUN1:def 6;
end;
:: from CIRCCMB3, 2009.02.16, A.T.
registration
let x1,x2,x3,x4 be object;
cluster <*x1,x2,x3,x4*> -> 4-element;
coherence;
let x5 be object;
cluster <*x1,x2,x3,x4,x5*> -> 5-element;
coherence;
end;
begin :: Moved from FSM_1, 2010.03.16, A.T.
theorem
for m, n being Nat holds m < n implies ex p being Element of NAT
st n = m+p & 1 <= p
proof
let m, n be Nat;
assume
A1: m < n;
then consider p being Nat such that
A2: n=m+p by NAT_1:10;
reconsider p as Element of NAT by ORDINAL1:def 12;
take p;
thus n = m+p by A2;
assume p < 1;
then p < 0+1;
then p = 0 by NAT_1:13;
hence contradiction by A1,A2;
end;
theorem
for S being set, D1, D2 being non empty set, f1 being Function of
S, D1, f2 being Function of D1, D2 holds f1 is bijective & f2 is bijective
implies f2*f1 is bijective
proof
let S be set, D1, D2 be non empty set, f1 be Function of S, D1, f2 be
Function of D1, D2;
set f3 = f2*f1;
A1: dom f2 = D1 by FUNCT_2:def 1;
assume
A2: f1 is bijective & f2 is bijective;
then rng f2 = D2 & rng f1 = D1 by FUNCT_2:def 3;
then rng f3 = D2 by A1,RELAT_1:28;
then f3 is one-to-one onto by A2,FUNCT_2:def 3;
hence thesis;
end;
:: Partitions & Equivalence Relations
theorem
for Y being set, E1, E2 being Equivalence_Relation of Y st
Class E1 = Class E2 holds E1 = E2
proof
let Y be set, E1, E2 be Equivalence_Relation of Y such that
A1: Class E1 = Class E2;
now
let x be object;
hereby
assume
A2: x in E1;
then consider a, b being object such that
A3: x = [a, b] and
A4: a in Y and
A5: b in Y by RELSET_1:2;
reconsider a,b as Element of Y by A4,A5;
Class (E1, b) in Class E2 by A1,A4,EQREL_1:def 3;
then consider c being object such that
c in Y and
A6: Class (E1, b) = Class (E2, c) by EQREL_1:def 3;
b in Class (E1, b) by A4,EQREL_1:20;
then [b, c] in E2 by A6,EQREL_1:19;
then
A7: [c, b] in E2 by EQREL_1:6;
a in Class (E1, b) by A2,A3,EQREL_1:19;
then [a, c] in E2 by A6,EQREL_1:19;
hence x in E2 by A3,A7,EQREL_1:7;
end;
assume
A8: x in E2;
then consider a, b being object such that
A9: x = [a, b] and
A10: a in Y and
A11: b in Y by RELSET_1:2;
reconsider a, b as Element of Y by A10,A11;
Class (E2, b) in Class E1 by A1,A10,EQREL_1:def 3;
then consider c being object such that
c in Y and
A12: Class (E2, b) = Class (E1, c) by EQREL_1:def 3;
b in Class (E2, b) by A10,EQREL_1:20;
then [b, c] in E1 by A12,EQREL_1:19;
then
A13: [c, b] in E1 by EQREL_1:6;
a in Class (E2, b) by A8,A9,EQREL_1:19;
then [a, c] in E1 by A12,EQREL_1:19;
hence x in E1 by A9,A13,EQREL_1:7;
end;
hence thesis;
end;
registration
let Z be finite set;
cluster -> finite for a_partition of Z;
coherence;
end;
registration
let X be non empty finite set;
cluster non empty finite for a_partition of X;
existence
proof
set p = the a_partition of X;
take p;
thus thesis;
end;
end;
theorem Th85:
for X being non empty set, PX being a_partition of X
for Pi being set st Pi in PX ex x being Element of X st x in Pi
proof
let X be non empty set, PX be a_partition of X;
let Pi be set;
assume Pi in PX;
then reconsider Pi as Element of PX;
set q = the Element of Pi;
reconsider q as Element of X;
take q;
thus thesis;
end;
reserve X, A for non empty finite set,
PX for a_partition of X,
PA1, PA2 for a_partition of A;
theorem
card PX <= card X
proof
assume card PX > card X;
then card Segm card X in card Segm card PX by NAT_1:41;
then consider Pi being object such that
A1: Pi in PX and
A2: for x being object st x in X holds (proj PX).x <> Pi by Th66;
reconsider Pi as Element of PX by A1;
consider q being Element of X such that
A3: q in Pi by Th85;
reconsider Pq = (proj PX).q as Element of PX;
A4: Pq = Pi or Pq misses Pi by EQREL_1:def 4;
q in Pq by EQREL_1:def 9;
hence contradiction by A2,A3,A4,XBOOLE_0:3;
end;
theorem
PA1 is_finer_than PA2 implies card PA2 <= card PA1
proof
defpred P[object,object] means
ex A,B being set st A = $1 & B = $2 & A c= B;
assume
A1: PA1 is_finer_than PA2;
A2: for e being object st e in PA1 ex u being object st u in PA2 & P[e,u]
proof let e be object;
reconsider ee=e as set by TARSKI:1;
assume e in PA1;
then ee in PA1;
then ex u being set st u in PA2 & ee c= u by SETFAM_1:def 2,A1;
hence thesis;
end;
consider f being Function of PA1, PA2 such that
A3: for e being object st e in PA1 holds P[e,f.e] from FUNCT_2:sch 1 (A2);
assume card PA1 < card PA2;
then card Segm card PA1 in card Segm card PA2 by NAT_1:41;
then consider p2i being object such that
A4: p2i in PA2 and
A5: for x being object st x in PA1 holds f.x <> p2i by Th66;
reconsider p2i as Element of PA2 by A4;
consider q being Element of A such that
A6: q in p2i by Th85;
reconsider p2q = f.((proj PA1).q) as Element of PA2;
A7: p2q=p2i or p2q misses p2i by EQREL_1:def 4;
P[((proj PA1).q),f.((proj PA1).q)] by A3;
then q in (proj PA1).q & (proj PA1).q c= p2q by EQREL_1:def 9;
hence contradiction by A5,A6,A7,XBOOLE_0:3;
end;
theorem Th88:
PA1 is_finer_than PA2 implies for p2 being Element of PA2
ex p1 being Element of PA1 st p1 c= p2
proof
assume
A1: PA1 is_finer_than PA2;
let p2 be Element of PA2;
consider E1 being Equivalence_Relation of A such that
A2: PA1 = Class E1 by EQREL_1:34;
reconsider p29 = p2 as Subset of A;
consider E2 being Equivalence_Relation of A such that
A3: PA2 = Class E2 by EQREL_1:34;
consider a being object such that
A4: a in A and
A5: p29 = Class (E2, a) by A3,EQREL_1:def 3;
A6: a in Class (E1, a) by A4,EQREL_1:20;
reconsider E1a = Class (E1, a) as Element of PA1 by A2,A4,EQREL_1:def 3;
consider p22 being set such that
A7: p22 in PA2 and
A8: E1a c= p22 by A1,SETFAM_1:def 2;
reconsider p229 = p22 as Subset of A by A7;
take E1a;
ex b being object st b in A & p229 = Class (E2, b) by A3,A7,EQREL_1:def 3;
hence thesis by A5,A8,A6,EQREL_1:23;
end;
theorem
PA1 is_finer_than PA2 & card PA1 = card PA2 implies PA1 = PA2
proof
defpred P[object,object] means
ex A,B being set st A = $1 & B = $2 & A c= B;
assume that
A1: PA1 is_finer_than PA2 and
A2: card PA1 = card PA2;
A3: for e being object st e in PA1 ex u being object st u in PA2 & P[e,u]
proof let e be object;
reconsider ee=e as set by TARSKI:1;
assume e in PA1;
then ee in PA1;
then ex u being set st u in PA2 & ee c= u by SETFAM_1:def 2,A1;
hence thesis;
end;
consider f being Function of PA1, PA2 such that
A4: for e being object st e in PA1 holds P[e,f.e] from FUNCT_2:sch 1 (A3);
A5: dom f = PA1 by FUNCT_2:def 1;
A6: PA2 c= rng f
proof
let p2 be object;
assume p2 in PA2;
then reconsider p29 = p2 as Element of PA2;
consider p1 being Element of PA1 such that
A7: p1 c= p29 by A1,Th88;
reconsider fp1 = f.p1 as Subset of A by TARSKI:def 3;
P[p1,f.p1] by A4;
then
A8: p1 c= f.p1;
p29 meets f.p1
proof
ex x being Element of A st x in p1 by Th85;
hence thesis by A7,A8,XBOOLE_0:3;
end;
then p29 = fp1 by EQREL_1:def 4;
hence thesis by A5,FUNCT_1:def 3;
end;
rng f c= PA2 by RELAT_1:def 19;
then rng f = PA2 by A6; then
f is onto by FUNCT_2:def 3; then
A9: f is one-to-one by A2,Lm1;
A10: for x being Element of PA1 holds x = f.x
proof
let x be Element of PA1;
reconsider fx = f.x as Subset of A by TARSKI:def 3;
consider E1 being Equivalence_Relation of A such that
A11: PA1 = Class E1 by EQREL_1:34;
assume x <> f.x;
then consider a being object such that
A12: a in x & not a in f.x or a in f.x & not a in x by TARSKI:2;
A13: fx c= A;
then
A14: a in Class (E1, a) by A12,EQREL_1:20;
reconsider CE1a = Class (E1, a) as Element of PA1 by A13,A12,A11,
EQREL_1:def 3;
reconsider fCE1a = f.CE1a as Subset of A by TARSKI:def 3;
P[x,f.x] by A4; then
A15: x c= f.x;
P[CE1a,f.CE1a] by A4;
then CE1a c= f.CE1a;
then fx meets fCE1a by A15,A12,A14,XBOOLE_0:3;
then fx = fCE1a by EQREL_1:def 4;
hence contradiction by A5,A9,A15,A12,A14;
end;
now
let x be object;
hereby
assume x in PA1;
then reconsider x9 = x as Element of PA1;
set fx = f.x9;
fx in PA2;
hence x in PA2 by A10;
end;
assume x in PA2;
then consider y being object such that
A16: y in dom f and
A17: x = f.y by A6,FUNCT_1:def 3;
reconsider y9 = y as Element of PA1 by A16,FUNCT_2:def 1;
y9 = f.y9 by A10;
hence x in PA1 by A17;
end;
hence thesis by TARSKI:2;
end;
registration
let D be set, M be FinSequence of D*;
let k;
cluster M/.k -> Function-like Relation-like; ::: !!!
coherence;
:: pewnie wystarczy 'D*-valued'
end;
registration
let D be set, M be FinSequence of D*;
let k;
cluster M/.k -> FinSequence-like D-valued for Function;
coherence by FINSEQ_1:def 11;
end;
reserve f for FinSequence of D;
theorem
m in dom f implies f/.1 = (f|m)/.1
proof
assume that
A1: m in dom f;
1<=m by A1,FINSEQ_3:25;
then 1 in Seg m;
hence thesis by A1,Th71;
end;
theorem
m in dom f implies f/.m = (f|m)/.len(f|m)
proof
assume that
A1: m in dom f;
m<=len f by A1,FINSEQ_3:25;
then
A2: len (f|m) = m by FINSEQ_1:59;
1<=m by A1,FINSEQ_3:25;
then m in Seg m;
hence thesis by A1,A2,Th71;
end;