Copyright (c) 1990 Association of Mizar Users
environ
vocabulary FUNCT_1, FINSEQ_1, RELAT_1, FINSET_1, CARD_1, BOOLE, PARTFUN1,
ARYTM_1, INT_1, RLSUB_2, TARSKI, FINSEQ_4;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
FINSEQ_1, RELAT_1, FUNCT_1, PARTFUN1, CARD_1, FUNCT_2, FINSET_1, INT_1,
NAT_1, FINSEQ_3;
constructors DOMAIN_1, WELLORD2, FUNCT_2, INT_1, NAT_1, FINSEQ_3, MEMBERED,
XBOOLE_0;
clusters FINSEQ_1, FUNCT_1, CARD_1, INT_1, FINSET_1, FINSEQ_3, RELSET_1,
MEMBERED, ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions FUNCT_1, TARSKI, XBOOLE_0;
theorems CARD_1, CARD_2, ENUMSET1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCT_1,
FUNCT_2, INT_1, NAT_1, PARTFUN1, REAL_1, RLVECT_1, TARSKI, WELLORD2,
ZFMISC_1, AXIOMS, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_0,
XCMPLX_1;
schemes FINSEQ_1, FINSET_1, NAT_1;
begin
reserve f for Function;
reserve p,q for FinSequence;
reserve A,B,C,x,x1,x2,y,z for set;
reserve i,k,l,m,m1,m2,n for Nat;
definition let f,x;
pred f is_one-to-one_at x means
:Def1: f " (f .: {x}) = {x};
end;
canceled;
theorem Th2:
f is_one-to-one_at x implies x in dom f
proof assume f is_one-to-one_at x;
then f " (f .: {x}) = {x} by Def1;
then x in f " (f .: {x}) by TARSKI:def 1;
hence thesis by FUNCT_1:def 13;
end;
theorem Th3:
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 Th2;
f " (f .: {x}) = {x} by A1,Def1;
hence thesis by A2,FUNCT_1:117;
end;
assume x in dom f & f " {f.x} = {x};
hence f " (f .: {x}) = {x} by FUNCT_1:117;
end;
theorem Th4:
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 Th2;
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 13;
then z in {x} by A1,Th3;
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,Th3;
then consider y 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 13;
now per cases by A8;
suppose y in f " {f.x} & not y in {x};
then y in dom f & f.y in {f.x} & y <> x by FUNCT_1:def 13,TARSKI:def
1;
then y in dom f & x <> y & f.y = f.x by TARSKI:def 1;
hence thesis by A6;
suppose not y in f " {f.x} & y in {x};
hence thesis by A9,TARSKI:def 1;
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;
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,Th4;
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,FUNCT_1:def 8;
hence thesis by A5,Th4;
end;
definition let f,y;
pred f just_once_values y means
:Def2: ex B being finite set st B = f " {y} & card B = 1;
end;
canceled;
theorem Th7:
f just_once_values y implies y in rng f
proof assume f just_once_values y;
then ex B being finite set st B = f " {y} & card B = 1 by Def2;
then rng f meets {y} by CARD_1:78,RELAT_1:173;
then consider x being set such that A1: x in rng f /\ {y} by XBOOLE_0:4;
x in {y} by A1,XBOOLE_0:def 3;
then y = x by TARSKI:def 1;
hence thesis by A1,XBOOLE_0:def 3;
end;
theorem Th8:
f just_once_values y iff ex x st {x} = f " {y}
proof
thus f just_once_values y implies ex x st {x} = f " {y}
proof assume A1: f just_once_values y;
then y in rng f by Th7;
then consider x such that A2: x in dom f and A3: f.x = y by FUNCT_1:def 5
;
take x;
ex B being finite set st B = f " {y} & card B = 1 by A1,Def2;
then consider z such that A4: f " {y} = {z} by CARD_2:60;
f.x in {y} by A3,TARSKI:def 1;
then x in {z} by A2,A4,FUNCT_1:def 13;
hence thesis by A4,TARSKI:def 1;
end;
given x such that A5: {x} = f " {y};
reconsider B = f " {y} as finite set by A5;
take B;
thus B = f " {y} & card B = 1 by A5,CARD_1:79;
end;
theorem Th9:
f just_once_values y iff
ex x st x in dom f & y = f.x &
for z st z in dom f & z <> x holds f.z <> y
proof
thus f just_once_values y implies
ex x st x in dom f & y = f.x & for z st z in
dom f & z <> x holds f.z <> y
proof assume
A1: f just_once_values y;
then consider B being finite set such that
A2: B = f " {y} & card B = 1 by Def2;
y in rng f by A1,Th7;
then consider x1 such that A3: x1 in dom f and A4: f.x1 = y
by FUNCT_1:def 5;
take x1;
thus x1 in dom f & y = f.x1 by A3,A4;
let z;
assume that A5: z in dom f and A6: z <> x1 and A7: f.z = y;
f.x1 in {y} & f.z in {y} by A4,A7,TARSKI:def 1;
then z in f " {y} & x1 in f " {y} by A3,A5,FUNCT_1:def 13;
then {z,x1} c= f " {y} & card B = 1 & f " {y} is finite
by A2,ZFMISC_1:38;
then card{z,x1} <= 1 by A2,CARD_1:80;
then 2 <= 1 by A6,CARD_2:76;
hence thesis;
end;
given x such that A8: x in dom f and A9: y = f.x and
A10: for z st z in dom f & z <> x holds f.z <> y;
A11: {x} = f " {y}
proof
thus {x} c= f " {y}
proof let x1;
assume x1 in {x};
then x1 = x & f.x in {y} by A9,TARSKI:def 1;
hence thesis by A8,FUNCT_1:def 13;
end;
let x1;
assume x1 in f " {y};
then f.x1 in {y} & x1 in dom f by FUNCT_1:def 13;
then x1 in dom f & f.x1 = y by TARSKI:def 1;
then x1 = x by A10;
hence thesis by TARSKI:def 1;
end;
then reconsider B = f " {y} as finite set;
card B = 1 & f " {y} is finite by A11,CARD_1:79;
hence thesis by Def2;
end;
theorem Th10:
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 such that A2: x in dom f & f.x = y by FUNCT_1:def 5;
for z holds z in dom f & z <> x implies f.z <> y
by A1,A2,FUNCT_1:def 8;
hence thesis by A2,Th9;
end;
assume A3: for y st y in rng f holds f just_once_values y;
let x,y;
assume that A4: x in dom f & y in dom f and A5: f.x = f.y;
f.x in rng f & f.y in rng f by A4,FUNCT_1:def 5;
then f just_once_values f.x & f just_once_values f.y by A3;
then consider x1 such that A6: {x1} = f " {f.x} by Th8;
f.x in {f.x} & f.y in {f.y} by TARSKI:def 1;
then x in f " {f.x} & y in f "{f.x} by A4,A5,FUNCT_1:def 13;
then x = x1 & y = x1 by A6,TARSKI:def 1;
hence thesis;
end;
theorem Th11:
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 Th2;
{x} = f " {f.x} by A1,Th3;
hence thesis by Th8;
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,Th8;
f.x in {f.x} by TARSKI:def 1;
then x in {z} by A2,A4,FUNCT_1:def 13;
then x = z by TARSKI:def 1;
hence thesis by A2,A4,Th3;
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,Th7;
then consider x such that A2: x in dom f & f.x = y by FUNCT_1:def 5;
take x;
thus thesis by A2;
end;
uniqueness
proof let x1,x2;
assume A3: x1 in dom f & f.x1 = y & x2 in dom f & f.x2 = y;
consider x such that x in dom f & f.x = y and
A4: for z st z in dom f & z <> x holds f.z <> y by A1,Th9;
x = x1 & x = x2 by A3,A4;
hence thesis;
end;
end;
canceled 4;
theorem
f just_once_values y implies f .: {f <- y} = {y}
proof assume A1: f just_once_values y;
then f <- y in dom f by Def3;
hence f .: {f <- y} = {f.(f <- y)} by FUNCT_1:117
.= {y} by A1,Def3;
end;
theorem Th17:
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 Th8;
x in f " {y} by A2,ZFMISC_1:37;
then x in dom f & f.x in {y} by FUNCT_1:def 13;
then x in dom f & f.x = y by TARSKI:def 1;
hence thesis by A1,A2,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 such that A3: x in dom f & f.x = y by A2,FUNCT_1:def 5;
f just_once_values y by A1,A2,Th10;
then x = f <- y by A3,Def3;
hence thesis by A1,A3,FUNCT_1:54;
end;
canceled;
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 Th11;
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;
then A2: f <- y in dom f by Def3;
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;
hence thesis by A2,Th4;
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;
coherence by FINSEQ_2:15;
end;
definition let D; let d1,d2,d3;
redefine func <* d1,d2,d3 *> -> FinSequence of D;
coherence by FINSEQ_2:16;
end;
definition
let X,D be set, p be PartFunc of X,D, i be set;
assume A1: i in dom p;
func p/.i -> Element of D equals
:Def4: p.i;
coherence by A1,PARTFUN1:27;
end;
theorem
for X,D be non empty set, p be Function of X,D, i be Element of X
holds p/.i = p.i
proof let X,D be non empty set, p be Function of X,D, i be Element of X;
i in X;
then i in dom p by FUNCT_2:def 1;
hence p/.i = p.i by Def4;
end;
canceled;
theorem
for D being set, P being FinSequence of D, i st 1 <= i & i <= len P
holds P/.i = P.i
proof let D be set, P be FinSequence of D, i;
assume 1 <= i & i <= len P;
then i in dom P by FINSEQ_3:27;
hence thesis by Def4;
end;
theorem
<* d *>/.1 = d
proof
dom<* d *> = {1} & <* d *>.1 = d & 1 in {1}
by FINSEQ_1:4,def 8,TARSKI:def 1;
hence thesis by Def4;
end;
theorem
<* d1,d2 *>/.1 = d1 & <* d1,d2 *>/.2 = d2
proof set s = <* d1,d2 *>;
dom s = {1,2} & s.1 = d1 & s.2 = d2 & 1 in {1,2} & 2 in {1,2}
by FINSEQ_1:4,61,FINSEQ_3:29,TARSKI:def 2;
hence thesis by Def4;
end;
theorem
<* d1,d2,d3 *>/.1 = d1 & <* d1,d2,d3 *>/.2 = d2 & <* d1,d2,d3 *>/.3 = d3
proof set s = <* d1,d2,d3 *>;
dom s = {1,2,3} & s.1 = d1 & s.2 = d2 & s.3 = d3 &
1 in {1,2,3} & 2 in {1,2,3} & 3 in {1,2,3}
by ENUMSET1:14,FINSEQ_1:62,FINSEQ_3:1,30;
hence thesis by Def4;
end;
definition let p; let x;
func x..p -> Nat equals
:Def5: Sgm(p " {x}).1;
coherence
proof set q = Sgm(p " {x});
per cases;
suppose
not 1 in dom q;
hence thesis by CARD_1:51,FUNCT_1:def 4;
suppose 1 in dom q;
then q.1 in rng q & rng q c= NAT by FINSEQ_1:def 4,FUNCT_1:def 5;
hence thesis;
end;
end;
canceled;
theorem Th29:
x in rng p implies p.(x..p) = x
proof assume A1: x in rng p;
set q = Sgm(p " {x});
A2: p " {x} <> {} & p " {x} c= dom p & dom p = Seg(len p)
by A1,FINSEQ_1:def 3,FUNCT_1:142,RELAT_1:167;
then rng q <> {} by FINSEQ_1:def 13;
then 1 in dom q by FINSEQ_3:34;
then q.1 in rng q & rng q = p " {x} & x..p = q.1
by A2,Def5,FINSEQ_1:def 13,FUNCT_1:def 5;
then p.(x..p) in {x} by FUNCT_1:def 13;
hence thesis by TARSKI:def 1;
end;
theorem Th30:
x in rng p implies x..p in dom p
proof assume A1: x in rng p;
A2: x..p = Sgm(p " {x}).1 by Def5;
A3: p " {x} <> {} & p " {x} c= dom p & dom p = Seg(len p)
by A1,FINSEQ_1:def 3,FUNCT_1:142,RELAT_1:167;
then rng(Sgm(p " {x})) <> {} by FINSEQ_1:def 13;
then 1 in dom(Sgm(p " {x})) by FINSEQ_3:34;
then x..p in rng(Sgm(p " {x})) by A2,FUNCT_1:def 5;
then x..p in p " {x} by A3,FINSEQ_1:def 13;
hence thesis by FUNCT_1:def 13;
end;
theorem Th31:
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 Th30;
hence thesis by FINSEQ_3:27;
end;
theorem Th32:
x in rng p implies x..p - 1 is Nat & len p - x..p is Nat
proof assume x in rng p;
then len p is Integer & x..p is Integer & 1 is Integer &
1 <= x..p & x..p <= len p by Th31;
hence thesis by INT_1:18;
end;
theorem Th33:
x in rng p implies x..p in p " {x}
proof assume x in rng p;
then p.(x..p) = x & x..p in dom p by Th29,Th30;
then p.(x..p) in {x} & x..p in dom p by TARSKI:def 1;
hence thesis by FUNCT_1:def 13;
end;
theorem Th34:
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: p " {x} c= dom p & dom p = Seg(len p) by FINSEQ_1:def 3,RELAT_1:167;
then rng q = p " {x} & x in {x} by FINSEQ_1:def 13,TARSKI:def 1;
then k in rng q by A1,A3,FUNCT_1:def 13;
then consider y such that A5: y in dom q and A6: q.y = k by FUNCT_1:def 5
;
A7: dom q = Seg(len q) by FINSEQ_1:def 3;
then reconsider y as Nat by A5;
A8: q.1 = x..p by Def5;
now assume not 1 < y;
then 1 = y or y < 1 by REAL_1:def 5;
then 1 = y or y = 0 by RLVECT_1:98;
hence contradiction by A2,A5,A6,Def5,FINSEQ_3:26;
end;
then 1 <= 1 & 1 < y & y <= len q by A5,A7,FINSEQ_1:3;
hence contradiction by A2,A4,A6,A8,FINSEQ_1:def 13;
end;
theorem Th35:
p just_once_values x implies p <- x = x..p
proof assume A1: p just_once_values x;
then p <- x in dom p & x in rng p by Def3,Th7;
then p <- x in dom p & x..p in dom p & p.(x..p) = x & p.(p <- x) = x
by A1,Def3,Th29,Th30;
hence thesis by A1,Def3;
end;
theorem Th36:
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;
x in rng p by A1,Th7;
then p <- x = x..p & p.(x..p) = x by A1,Th29,Th35;
hence thesis by A1,A2,Def3;
end;
theorem Th37:
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: p.(x..p) = x & x..p in dom p by A1,Th29,Th30;
now let z;
assume that A4: z in dom p and A5: z <> x..p;
reconsider n = z as Nat by A4,FINSEQ_3:25;
p.n <> x by A2,A4,A5;
hence p.z <> x;
end;
hence thesis by A3,Th9;
end;
theorem Th38:
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 Th35;
hence thesis by A1,Th7,Th17;
end;
assume that A2: x in rng p and A3: {x..p} = p " {x};
A4: p.(x..p) = x & x..p in dom p by A2,Th29,Th30;
now let z;
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 13;
hence contradiction by A3,A6,TARSKI:def 1;
end;
hence thesis by A4,Th9;
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;
assume y in {x..p};
then y = x..p by TARSKI:def 1;
hence thesis by A2,Th33;
end;
let y;
assume y in p " {x};
then y in dom p & p.y in {x} by FUNCT_1:def 13;
then y in dom p & p.y = x & p.(x..p) = x & x..p in dom p
by A2,Th29,Th30,TARSKI:def 1;
then x..p = y by A1,FUNCT_1:def 8;
hence thesis by TARSKI:def 1;
end;
theorem Th40:
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
proof assume A1: p just_once_values x;
A2: len(p - {x}) = len p - card(p " {x}) by FINSEQ_3:66;
p " {x} = {x..p} by A1,Th38;
hence thesis by A2,CARD_1:79;
end;
assume A3: len(p - {x}) = len p - 1;
len p + (- 1) = len p - 1 by XCMPLX_0:def 8
.= len p - card(p " {x}) by A3,FINSEQ_3:66
.= len p + (- card(p " {x})) by XCMPLX_0:def 8;
then - 1 = - card(p " {x}) by XCMPLX_1:2;
then 1 = - (- card(p " {x}))
.= card(p " {x});
hence thesis by Def2;
end;
theorem Th41:
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;
then A2: x in rng p by Th7;
let k;
assume A3: k in dom(p - {x});
A4: dom(p - {x}) c= dom p by FINSEQ_3:70;
set A = {l : l in dom p & l <= k & p.l in {x}}; set q = p - {x};
set B = {m : m in dom p & m <= k + 1 & p.m in {x}};
thus k < x..p implies (p - {x}).k = p.k
proof assume A5: k < x..p;
A6: A = {}
proof
thus A c= {}
proof let y;
assume y in A;
then consider l such that y = l and A7: l in dom p and
A8: l <= k and A9: p.l in {x};
p.l <> x & p.l = x by A1,A5,A7,A8,A9,Th36,TARSKI:def 1;
hence thesis;
end;
thus {} c= A by XBOOLE_1:2;
end;
p.k <> x by A1,A3,A4,A5,Th36;
then not p.k in {x} by TARSKI:def 1;
then q.(k - 0) = p.k by A3,A4,A6,CARD_1:78,FINSEQ_3:92;
hence thesis;
end;
assume A10: x..p <= k;
A11: B = {x..p}
proof
thus B c= {x..p}
proof let y;
assume y in B;
then consider m such that A12: m = y and A13: m in dom p and
m <= k + 1 and A14: p.m in {x};
p.m = x by A14,TARSKI:def 1;
then m = x..p by A1,A13,Th36;
hence thesis by A12,TARSKI:def 1;
end;
let y;
assume y in {x..p};
then A15: y = x..p by TARSKI:def 1;
A16: x..p in dom p by A2,Th30;
A17: x..p <= k + 1 by A10,NAT_1:37;
p.(x..p) = x by A2,Th29;
then p.(x..p) in {x} by TARSKI:def 1;
hence thesis by A15,A16,A17;
end;
then reconsider B as finite set;
dom q = Seg(len q) & len(p - {x}) = len p - 1 by A1,Th40,FINSEQ_1:def
3
;
then 1 <= k & k <= len p - 1 & k <= k + 1 by A3,FINSEQ_1:3,NAT_1:37;
then 1 <= k + 1 & k + 1 <= len p by AXIOMS:22,REAL_1:84;
then k + 1 in Seg(len p) by FINSEQ_1:3;
then A18: k + 1 in dom p by FINSEQ_1:def 3;
now assume A19: p.(k + 1) in {x};
x..p <> k + 1 by A10,REAL_1:69;
then p.(k + 1) <> x by A1,A18,Th36;
hence contradiction by A19,TARSKI:def 1;
end;
then (p - {x}).((k + 1) - card B) = p.(k + 1) by A18,FINSEQ_3:92;
then q.((k + 1) - 1) = p.(k + 1) by A11,CARD_1:79;
hence thesis by XCMPLX_1:26;
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;
A3: p just_once_values x by A1,A2,Th10;
let k; set q = p - {x};
assume A4: k in dom(p - {x});
A5: dom(p - {x}) c= dom p by FINSEQ_3:70;
dom q = Seg(len q) & len(p - {x}) = len p - 1
by A3,Th40,FINSEQ_1:def 3;
then 1 <= k & k <= len p - 1 & k <= k + 1 by A4,FINSEQ_1:3,NAT_1:37;
then 1 <= k + 1 & k + 1 <= len p by AXIOMS:22,REAL_1:84;
then k + 1 in Seg(len p) by FINSEQ_1:3;
then A6: k + 1 in dom p by FINSEQ_1:def 3;
thus (p - {x}).k = p.k implies k < x..p
proof assume that A7: (p - {x}).k = p.k and A8: not k < x..p;
q.k = p.(k + 1) by A3,A4,A8,Th41;
then k + 0 = k + 1 by A1,A4,A5,A6,A7,FUNCT_1:def 8;
hence thesis by XCMPLX_1:2;
end;
thus k < x..p implies (p - {x}).k = p.k by A3,A4,Th41;
thus (p - {x}).k = p.(k + 1) implies x..p <= k
proof assume A9: (p - {x}).k = p.(k + 1);
assume not x..p <= k;
then p.(k + 1) = p.k by A3,A4,A9,Th41;
then k + 0 = k + 1 by A1,A4,A5,A6,FUNCT_1:def 8;
hence thesis by XCMPLX_1:2;
end;
thus x..p <= k implies (p - {x}).k = p.(k + 1) by A3,A4,Th41;
end;
definition let p; let x;
assume A1: x in rng p;
func p -| x -> FinSequence means
:Def6: ex n st n = x..p - 1 & it = p | Seg n;
existence
proof reconsider n = x..p - 1 as Nat by A1,Th32;
reconsider q = p | Seg n as FinSequence by FINSEQ_1:19;
take q;
thus thesis;
end;
uniqueness;
end;
canceled 2;
theorem Th45:
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 Def6;
hence thesis;
end;
theorem Th46:
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
Def6;
n + 1 <= x..p & x..p <= len p by A1,A2,Th31,REAL_1:84;
then n + 1 <= len p & n <= n + 1 by AXIOMS:22,NAT_1:37;
then n <= len p by AXIOMS:22;
hence thesis by A2,A3,FINSEQ_1:21;
end;
theorem Th47:
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 Th46;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th48:
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,Def6;
hence thesis by A2,FUNCT_1:70;
end;
theorem Th49:
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 Nat by A1,Th32; set r = p | Seg n;
A3: r = p -| x by A1,Th45;
then consider y such that A4: y in dom r and A5: r.y = x by A2,FUNCT_1:def
5;
A6: dom r = Seg n by A1,A3,Th47;
then reconsider y as Nat by A4;
A7: dom r c= dom p by FUNCT_1:76;
y <= n by A4,A6,FINSEQ_1:3;
then y + 1 <= x..p & y < y + 1 by REAL_1:69,84;
then y < x..p by AXIOMS:22;
then p.y <> x by A4,A7,Th34;
hence thesis by A4,A5,FUNCT_1:70;
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 Th49;
then for y 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 Def6;
hence thesis by FUNCT_1:76;
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,Th46
.= 0 by A2;
hence thesis by FINSEQ_1:25;
end;
assume p -| x = {};
then len(p -| x) = 0 & len(p -| x) = x..p - 1 by A1,Th46,FINSEQ_1:25;
then x..p - 1 + 1 = 1;
hence thesis by XCMPLX_1:27;
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 Def6;
hence thesis by FINSEQ_1:23;
end;
definition let p; let x;
assume A1: x in rng p;
func p |-- x -> FinSequence means
:Def7: len it = len p - x..p &
for k st k in dom it holds it.k = p.(k + x..p);
existence
proof reconsider n = len p - x..p as Nat by A1,Th32;
deffunc F(Nat) = p.($1 + x..p);
consider q such that A2: len q = n and
A3: for k st k in Seg n holds q.k = F(k) from SeqLambda;
take q;
dom q = Seg n by A2,FINSEQ_1:def 3;
hence thesis by A2,A3;
end;
uniqueness
proof let q,r be FinSequence;
assume that A4: len q = len p - x..p and
A5: for k st k in dom q holds q.k = p.(k + x..p);
assume that A6: len r = len p - x..p and
A7: for k st k in dom r holds r.k = p.(k + x..p);
now let k;
assume A8: k in Seg(len q);
dom q = Seg(len q) & dom r = Seg(len r) by FINSEQ_1:def 3;
then q.k = p.(k + x..p) & r.k = p.(k + x..p) by A4,A5,A6,A7,A8;
hence q.k = r.k;
end;
hence thesis by A4,A6,FINSEQ_2:10;
end;
end;
canceled 3;
theorem Th57:
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 Def7;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th58:
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);
1 <= n & n <= n + x..p by A2,FINSEQ_3:27,NAT_1:37;
then A3: 1 <= n + x..p by AXIOMS:22;
reconsider m = len p - x..p as Nat by A1,Th32;
n in Seg m by A1,A2,Th57;
then n <= len p - x..p by FINSEQ_1:3;
then n + x..p <= len p by REAL_1:84;
hence n + x..p in dom p by A3,FINSEQ_3:27;
end;
theorem
x in rng p implies rng(p |-- x) c= rng p
proof assume A1: x in rng p;
let y;
assume y in rng(p |-- x);
then consider z such that A2: z in dom(p |-- x) and A3: (p |-- x).z = y
by FUNCT_1:def 5;
reconsider z as Nat by A2,FINSEQ_3:25;
A4: y = p.(z + x..p) by A1,A2,A3,Def7;
z + x..p in dom p by A1,A2,Th58;
hence thesis by A4,FUNCT_1:def 5;
end;
theorem Th60:
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 Th7;
assume x in rng(p |-- x);
then consider z such that A3: z in dom(p |-- x) and A4: (p |-- x).z = x
by FUNCT_1:def
5;
reconsider z as Nat by A3,FINSEQ_3:25;
A5: (p |-- x).z = p.(z + x..p) by A2,A3,Def7;
z + x..p in dom p by A2,A3,Th58;
then z + x..p = 0 + x..p by A1,A4,A5,Th36;
then z = 0 by XCMPLX_1:2;
hence thesis by A3,FINSEQ_3:26;
end;
assume that A6: x in rng p and A7: not x in rng(p |-- x);
now let k;
assume that A8: k in dom p and A9: k <> x..p and A10: p.k = x;
now per cases by A9,AXIOMS:21;
suppose k < x..p;
then k + 1 <= x..p by NAT_1:38;
then k <= x..p - 1 by REAL_1:84;
then 1 <= k & k <= len(p -| x) by A6,A8,Th46,FINSEQ_3:27;
then A11: k in dom(p -| x) by FINSEQ_3:27;
then x = (p -| x).k by A6,A10,Th48;
then x in rng(p -| x) by A11,FUNCT_1:def 5;
hence contradiction by A6,Th49;
suppose A12: x..p < k;
then consider m such that A13: k = x..p + m by NAT_1:28;
x..p + 0 < x..p + m by A12,A13;
then 0 < m by AXIOMS:24;
then A14: 0 + 1 <= m by NAT_1:38;
m + x..p <= len p by A8,A13,FINSEQ_3:27;
then m <= len p - x..p by REAL_1:84;
then m <= len(p |-- x) by A6,Def7;
then A15: m in dom(p |-- x) by A14,FINSEQ_3:27;
then (p |-- x).m = p.k by A6,A13,Def7;
hence contradiction by A7,A10,A15,FUNCT_1:def 5;
end;
hence contradiction;
end;
hence thesis by A6,Th37;
end;
theorem Th61:
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);
consider y such that A4: y in dom(p |-- x) and A5: (p |-- x).y = x
by A3,FUNCT_1:def 5
;
reconsider y as Nat by A4,FINSEQ_3:25;
A6: (p |-- x).y = p.(y + x..p) by A1,A4,Def7;
A7: x..p in dom p & p.(x..p) = x by A1,Th29,Th30;
1 <= x..p & x..p <= y + x..p by A1,Th31,NAT_1:37;
then A8: 1 <= y + x..p by AXIOMS:22;
A9: y in Seg(len(p |-- x)) by A4,FINSEQ_1:def 3;
then y <= len(p |-- x) & len(p |--
x) = len p - x..p by A1,Def7,FINSEQ_1:3;
then y + x..p <= len p by REAL_1:84;
then y + x..p in Seg(len p) by A8,FINSEQ_1:3;
then y + x..p in dom p by FINSEQ_1:def 3;
then 0 + x..p = y + x..p by A2,A5,A6,A7,FUNCT_1:def 8;
then 0 = y by XCMPLX_1:2;
hence thesis by A9,FINSEQ_1:3;
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 Th60;
A2: not x in rng(p |-- x) by A1,Th60;
assume not rng(p |-- x) misses {x};
then ex y st y in rng(p |-- x) & y in {x} by XBOOLE_0:3;
hence thesis by A2,TARSKI:def 1;
end;
assume that A3: x in rng p and A4: rng(p |-- x) misses {x};
now assume A5: x in rng(p |-- x);
x in {x} by TARSKI:def 1;
hence contradiction by A4,A5,XBOOLE_0:3;
end;
hence thesis by A3,Th60;
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 Th61;
then for y 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,Def7
.= 0 by A2,XCMPLX_1:14;
hence thesis by FINSEQ_1:25;
end;
assume p |-- x = {};
then len(p |-- x) = 0 & len(p |--
x) = len p - x..p by A1,Def7,FINSEQ_1:25;
then len p - x..p + x..p = x..p;
hence thesis by XCMPLX_1:27;
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 let y;
assume y in rng(p |-- x);
then consider z such that A3: z in dom(p |-- x) and A4: (p |-- x).z = y
by FUNCT_1:def
5;
A5: dom(p |-- x) = Seg(len(p |-- x)) by FINSEQ_1:def 3;
then reconsider z as Nat by A3;
A6: y = p.(z + x..p) by A1,A3,A4,Def7;
1 <= x..p & x..p <= z + x..p by A1,Th31,NAT_1:37;
then A7: 1 <= z + x..p by AXIOMS:22;
z <= len(p |-- x) & len(p |-- x) = len p - x..p
by A1,A3,A5,Def7,FINSEQ_1:3;
then z + x..p <= len p by REAL_1:84;
then z + x..p in Seg(len p) by A7,FINSEQ_1:3;
then z + x..p in dom p by FINSEQ_1:def 3;
then y in rng p & rng p c= D by A2,A6,FINSEQ_1:def 4,FUNCT_1:def 5;
hence thesis;
end;
hence thesis by FINSEQ_1:def 4;
end;
theorem Th66:
x in rng p implies p = (p -| x) ^ <* x *> ^ (p |-- x)
proof assume A1: x in rng p;
set q1 = p -| x; set q2 = p |-- x; set r = q1 ^ <* x *>;
A2: len p = len p - x..p + x..p by XCMPLX_1:27
.= x..p + len q2 by A1,Def7
.= x..p - 1 + 1 + len q2 by XCMPLX_1:27
.= len q1 + 1 + len q2 by A1,Th46
.= len q1 + len<* x *> + len q2 by FINSEQ_1:57
.= len r + len q2 by FINSEQ_1:35;
A3: now let k;
assume A4: k in dom r;
now per cases by A4,FINSEQ_1:38;
suppose A5: k in dom q1;
hence r.k = q1.k by FINSEQ_1:def 7
.= p.k by A1,A5,Th48;
suppose ex n st n in dom<* x *> & k = len q1 + n;
then consider n such that A6: n in dom <* x *> and
A7: k = len q1 + n;
n in {1} by A6,FINSEQ_1:4,def 8;
then A8: n = 1 by TARSKI:def 1;
hence r.k = <* x *>.1 by A6,A7,FINSEQ_1:def 7
.= x by FINSEQ_1:def 8
.= p.(x..p) by A1,Th29
.= p.(x..p - 1 + 1) by XCMPLX_1:27
.= p.k by A1,A7,A8,Th46;
end;
hence p.k = r.k;
end;
now let k;
assume k in dom q2;
then q2.k = p.(x..p + k) by A1,Def7
.= p.(x..p - 1 + 1 + k) by XCMPLX_1:27
.= p.(len q1 + 1 + k) by A1,Th46
.= p.(len q1 + len<* x *> + k) by FINSEQ_1:57
.= p.(len r + k) by FINSEQ_1:35;
hence p.(len r + k) = q2.k;
end;
hence thesis by A2,A3,FINSEQ_3:43;
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 Th66
.= (p -| x) ^ (<* x *> ^ (p |-- x)) by FINSEQ_1:45;
hence thesis by FINSEQ_3:98;
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 Th66;
hence thesis by FINSEQ_3:98;
end;
theorem Th69:
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 Th7;
then len r + len s = (x..p - 1) + len s by Th46
.= (x..p - 1) + (len p - x..p) by A2,Def7
.= (x.. p + (len p - x..p)) - 1 by XCMPLX_1:29
.= len p - 1 by XCMPLX_1:27
.= len q by A1,Th40;
then A3: dom q = Seg(len r + len s) by FINSEQ_1:def 3;
A4: now let k;
assume A5: k in dom r;
then A6: r.k = p.k by A2,Th48;
x..p <= len p by A2,Th31;
then x..p - 1 <= len p - 1 by REAL_1:49;
then len r <= len p - 1 by A2,Th46;
then len r <= len q by A1,Th40;
then A7: Seg(len r) c= Seg(len q) & Seg(len r) = dom r &
Seg(len q) = dom q by FINSEQ_1:7,def 3;
k in Seg(len r) by A5,FINSEQ_1:def 3;
then k <= len r by FINSEQ_1:3;
then k <= x..p - 1 by A2,Th46;
then k + 1 <= x..p & k < k + 1 by REAL_1:69,84;
then k < x..p by AXIOMS:22;
hence q.k = r.k by A1,A5,A6,A7,Th41;
end;
now let k;
assume A8: k in dom s;
then A9: s.k = p.(k + x..p) by A2,Def7;
A10: k + x..p - 1 = k + x..p + (- 1) by XCMPLX_0:def 8
.= k + (x..p + (- 1)) by XCMPLX_1:1
.= k + (x..p - 1) by XCMPLX_0:def 8;
reconsider m = x..p - 1 as Nat by A2,Th32;
set z = k + m;
A11: dom s = Seg(len s) by FINSEQ_1:def 3;
then A12: 1 <= k & 1 <= x..p by A2,A8,Th31,FINSEQ_1:3;
then 1 + 1 <= k + x..p by REAL_1:55;
then A13: 1 <= k + x..p - 1 by REAL_1:84;
k <= len s by A8,A11,FINSEQ_1:3;
then k <= len p - x..p by A2,Def7;
then k + x..p <= len p by REAL_1:84;
then k + x..p - 1 <= len p - 1 by REAL_1:49;
then k + x..p - 1 <= len q & dom q = Seg(len q)
by A1,Th40,FINSEQ_1:def 3;
then A14: z in dom q by A10,A13,FINSEQ_1:3;
x..p + 1 <= k + x..p by A12,REAL_1:55;
then x..p <= k + x..p - 1 by REAL_1:84;
then q.z = p.(z + 1) by A1,A10,A14,Th41
.= p.(k + x..p) by A10,XCMPLX_1:27;
hence q.(len r + k) = s.k by A2,A9,Th46;
end;
hence thesis by A3,A4,FINSEQ_1:def 7;
end;
assume A15: x in rng p;
assume A16: p - {x} = (p -| x) ^ (p |-- x);
now let k;
assume that A17: k in dom p and A18: k <> x..p and A19: p.k = x;
A20: len q = len p - card(p " {x}) by FINSEQ_3:66
.= len p + (- card(p " {x})) by XCMPLX_0:def 8;
len q = len r + len s by A16,FINSEQ_1:35
.= (x..p - 1) + len s by A15,Th46
.= (x..p - 1) + (len p - x..p) by A15,Def7
.= (x.. p + (len p - x..p)) - 1 by XCMPLX_1:29
.= len p - 1 by XCMPLX_1:27
.= len p + (- 1) by XCMPLX_0:def 8;
then - card(p " {x}) = - 1 by A20,XCMPLX_1:2;
then A21: - (- card(p " {x})) = 1;
{x..p,k} c= p " {x}
proof let y;
assume A22: y in {x..p,k};
x in {x} & x..p in
dom p & p.(x..p) = x by A15,Th29,Th30,TARSKI:def 1;
then x..p in p " {x} & k in p " {x} by A17,A19,FUNCT_1:def 13;
hence thesis by A22,TARSKI:def 2;
end;
then card{x..p,k} <= card(p " {x}) by CARD_1:80;
then 2 <= card(p " {x}) by A18,CARD_2:76;
hence contradiction by A21;
end;
hence thesis by A15,Th37;
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 Th10;
hence thesis by Th69;
end;
theorem Th71:
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);
let x1,x2; set q = p - {x};
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 Nat by A4,A5,FINSEQ_3:25;
A7: p just_once_values x by A1,A3,Th69;
now per cases by AXIOMS:21;
suppose x1 = x..p & x2 = x..p;
hence thesis;
suppose x1 = x..p & x..p < k2;
then p.x1 = x & k2 <> x..p by A1,Th29;
hence thesis by A5,A6,A7,Th36;
suppose x1 = x..p & k2 < x..p;
then p.x1 = x & k2 <> x..p by A1,Th29;
hence thesis by A5,A6,A7,Th36;
suppose k1 < x..p & x..p = x2;
then p.x2 = x & k1 <> x..p by A1,Th29;
hence thesis by A4,A6,A7,Th36;
suppose A8: k1 < x..p & x..p < k2;
then k2 <> 0 by NAT_1:18;
then consider m2 such that A9: k2 = m2 + 1 by NAT_1:22;
k1 in Seg(len p) by A4,FINSEQ_1:def 3;
then A10: 1 <= k1 by FINSEQ_1:3;
x..p <= len p by A1,Th31;
then k1 < len p by A8,AXIOMS:22;
then k1 + 1 <= len p by NAT_1:38;
then k1 <= len p - 1 by REAL_1:84;
then k1 <= len q by A7,Th40;
then k1 in Seg(len q) by A10,FINSEQ_1:3;
then A11: k1 in dom q by FINSEQ_1:def 3;
A12: x..p <= m2 by A8,A9,NAT_1:38;
1 <= x..p by A1,Th31;
then A13: 1 <= m2 by A12,AXIOMS:22;
k2 in Seg(len p) by A5,FINSEQ_1:def 3;
then k2 <= len p by FINSEQ_1:3;
then m2 <= len p - 1 by A9,REAL_1:84;
then m2 <= len q by A7,Th40;
then m2 in Seg(len q) by A13,FINSEQ_1:3;
then A14: m2 in dom(p - {x}) by FINSEQ_1:def 3;
then q.k1 = p.k1 & q.m2 = p.k2 by A7,A8,A9,A11,A12,Th41;
hence thesis by A2,A6,A8,A11,A12,A14,FUNCT_1:def 8;
suppose A15: k1 < x..p & k2 < x..p;
k1 in Seg(len p) & k2 in Seg(len p) by A4,A5,FINSEQ_1:def 3;
then A16: 1 <= k1 & 1 <= k2 by FINSEQ_1:3;
x..p <= len p by A1,Th31;
then k1 < len p & k2 < len p by A15,AXIOMS:22;
then k1 + 1 <= len p & k2 + 1 <= len p by NAT_1:38;
then k1 <= len p - 1 & k2 <= len p - 1 by REAL_1:84;
then k1 <= len q & k2 <= len q by A7,Th40;
then k1 in Seg(len q) & k2 in Seg(len q) by A16,FINSEQ_1:3;
then A17: k1 in dom q & k2 in dom q by FINSEQ_1:def 3;
then p.k1 = (p - {x}).k1 & p.k2 = (p - {x}).k2 by A7,A15,Th41;
hence thesis by A2,A6,A17,FUNCT_1:def 8;
suppose A18: x..p < k1 & x..p < k2;
then A19: k1 <> 0 & k2 <> 0 by NAT_1:18;
then consider m1 such that A20: k1 = m1 + 1 by NAT_1:22;
consider m2 such that A21: k2 = m2 + 1 by A19,NAT_1:22;
A22: x..p <= m1 & x..p <= m2 by A18,A20,A21,NAT_1:38;
1 <= x..p by A1,Th31;
then A23: 1 <= m1 & 1 <= m2 by A22,AXIOMS:22;
k1 in Seg(len p) & k2 in Seg(len p) by A4,A5,FINSEQ_1:def 3;
then k1 <= len p & k2 <= len p by FINSEQ_1:3;
then m1 <= len p - 1 & m2 <= len p - 1 by A20,A21,REAL_1:84;
then m1 <= len q & m2 <= len q by A7,Th40;
then m1 in Seg(len q) & m2 in Seg(len q) by A23,FINSEQ_1:3;
then A24: m1 in dom(p - {x}) & m2 in dom(p - {x}) by FINSEQ_1:def 3;
then p.k1 = (p - {x}).m1 & p.k2 = (p - {x}).m2
by A7,A20,A21,A22,Th41;
hence thesis by A2,A6,A20,A21,A24,FUNCT_1:def 8;
suppose x..p < k1 & x..p = x2;
then p.x2 = x & k1 <> x..p by A1,Th29;
hence thesis by A4,A6,A7,Th36;
suppose A25: x..p < k1 & k2 < x..p;
then k1 <> 0 by NAT_1:18;
then consider m2 such that A26: k1 = m2 + 1 by NAT_1:22;
k2 in Seg(len p) by A5,FINSEQ_1:def 3;
then A27: 1 <= k2 by FINSEQ_1:3;
x..p <= len p by A1,Th31;
then k2 < len p by A25,AXIOMS:22;
then k2 + 1 <= len p by NAT_1:38;
then k2 <= len p - 1 by REAL_1:84;
then k2 <= len q by A7,Th40;
then k2 in Seg(len q) by A27,FINSEQ_1:3;
then A28: k2 in dom q by FINSEQ_1:def 3;
A29: x..p <= m2 by A25,A26,NAT_1:38;
1 <= x..p by A1,Th31;
then A30: 1 <= m2 by A29,AXIOMS:22;
k1 in Seg(len p) by A4,FINSEQ_1:def 3;
then k1 <= len p by FINSEQ_1:3;
then m2 <= len p - 1 by A26,REAL_1:84;
then m2 <= len q by A7,Th40;
then m2 in Seg(len q) by A30,FINSEQ_1:3;
then A31: m2 in dom(p - {x}) by FINSEQ_1:def 3;
then q.k2 = p.k2 & q.m2 = p.k1 by A7,A25,A26,A28,A29,Th41;
hence thesis by A2,A6,A25,A28,A29,A31,FUNCT_1:def 8;
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,Th66;
then rng(p |-- x) misses rng((p -| x) ^ <* x *>) &
rng(p -| x) c= rng((p -| x) ^ <* x *>) by A2,FINSEQ_1:42,FINSEQ_3:98;
hence thesis by XBOOLE_1:63;
end;
theorem Th73:
A is finite implies ex p st rng p = A & p is one-to-one
proof assume A1: A is finite;
defpred P[set] means ex p st rng p = $1 & p is one-to-one;
now reconsider p = {} as FinSequence;
take p;
thus rng p = {} by FINSEQ_1:27;
thus p is one-to-one;
end; then
A2: P[{}];
now let B,C;
assume that B in A and C c= A;
given p such that A3: rng p = C and A4: p is one-to-one;
A5: now assume A6: B in C;
take q = p;
thus rng q = C \/ {B} & q is one-to-one by A3,A4,A6,ZFMISC_1:46;
end;
now assume A7: not B in C;
take q = p ^ <* B *>;
thus rng q = rng p \/ rng<* B *> by FINSEQ_1:44
.= C \/ {B} by A3,FINSEQ_1:55;
thus q is one-to-one
proof let x,y;
assume that A8: x in dom q and A9: y in dom q and A10: q.x = q.y;
x in Seg(len q) & y in Seg(len q) by A8,A9,FINSEQ_1:def 3;
then reconsider k = x, l = y as Nat;
A11: now assume A12: 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 A4,A10,A12,FUNCT_1:def 8;
end;
A13: now assume A14: k in dom p;
given n such that A15: n in dom<* B *> and A16: l = len p + n;
n in {1} by A15,FINSEQ_1:4,55;
then A17: n = 1 by TARSKI:def 1;
<* B *>.n = q.k by A10,A15,A16,FINSEQ_1:def 7
.= p.k by A14,FINSEQ_1:def 7;
then B = p.k by A17,FINSEQ_1:def 8;
hence thesis by A3,A7,A14,FUNCT_1:def 5;
end;
A18: now assume A19: l in dom p;
given n such that A20: n in dom<* B *> and A21: k = len p + n;
n in {1} by A20,FINSEQ_1:4,55;
then A22: n = 1 by TARSKI:def 1;
<* B *>.n = q.l by A10,A20,A21,FINSEQ_1:def 7
.= p.l by A19,FINSEQ_1:def 7;
then B = p.l by A22,FINSEQ_1:def 8;
hence thesis by A3,A7,A19,FUNCT_1:def 5;
end;
now given m1 being Nat such that A23: m1 in dom<* B *> and
A24: k = len p + m1;
given m2 being Nat such that A25: m2 in dom<* B *> and
A26: l = len p + m2;
m1 in {1} & m2 in {1} by A23,A25,FINSEQ_1:4,def 8;
then m1 = 1 & m2 = 1 by TARSKI:def 1;
hence thesis by A24,A26;
end;
hence thesis by A8,A9,A11,A13,A18,FINSEQ_1:38;
end;
end;
hence ex p st rng p = C \/ {B} & p is one-to-one by A5;
end; then
A27: for B,C being set st B in A & C c= A & P[C] holds P[C \/ {B}];
thus P[A] from Finite(A1,A2,A27);
end;
theorem Th74:
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;
now let q;
assume A1: len q = 0;
assume rng q c= dom q & q is one-to-one;
q = {} by A1,FINSEQ_1:25;
then dom q = {} & rng q = {} by FINSEQ_1:26,27;
hence rng q = dom q;
end; then
A2: P[0];
now let k;
assume A3: 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 A4: len q = k + 1 and A5: rng q c= dom q and
A6: q is one-to-one;
A7: dom q = Seg(k + 1) by A4,FINSEQ_1:def 3;
dom q c= rng q
proof let x;
assume A8: x in dom q;
then reconsider n = x as Nat by A7;
per cases;
suppose A9: k + 1 in rng q;
now per cases;
suppose n = k + 1;
hence thesis by A9;
suppose A10: n <> k + 1;
set r = q - {k + 1};
A11: r is one-to-one by A6,FINSEQ_3:94;
A12: len r = (k + 1) - 1 by A4,A6,A9,FINSEQ_3:97
.= k by XCMPLX_1:26;
A13: rng r = rng q \ {k + 1} by FINSEQ_3:72;
then A14: rng r c= Seg(k + 1) \ {k + 1} & dom r = Seg k
by A5,A7,A12,FINSEQ_1:def 3,XBOOLE_1:33;
then rng r c= dom r by RLVECT_1:104;
then A15: rng r = dom r by A3,A11,A12;
not x in {k + 1} by A10,TARSKI:def 1;
then x in Seg(k + 1) \ {k + 1} by A7,A8,XBOOLE_0:def 4;
then x in Seg k by RLVECT_1:104;
hence x in rng q by A13,A14,A15,XBOOLE_0:def 4;
end;
hence thesis;
suppose A16: not k + 1 in rng q;
reconsider r = q | Seg k as FinSequence by FINSEQ_1:19;
A17: len r = k by A4,FINSEQ_3:59;
then A18: dom r = Seg k & rng r c= rng q
by FINSEQ_1:def 3,FUNCT_1:76;
A19: rng q c= Seg k
proof let x;
assume x in rng q;
then x in Seg(k + 1) & not x in {k + 1}
by A5,A7,A16,TARSKI:def 1;
then x in Seg(k + 1) \ {k + 1} by XBOOLE_0:def 4;
hence thesis by RLVECT_1:104;
end;
then A20: rng r c= dom r by A18,XBOOLE_1:1;
r is one-to-one by A6,FUNCT_1:84;
then A21: rng r = dom r by A3,A17,A20;
A22: k + 1 in Seg(k + 1) by FINSEQ_1:6;
then q.(k + 1) in rng q by A7,FUNCT_1:def 5;
then consider x such that A23: x in dom r and
A24: r.x = q.(k + 1) by A18,A19,A21,FUNCT_1:def 5;
reconsider n = x as Nat by A18,A23;
A25: dom r c= dom q by FUNCT_1:76;
A26: r.x = q.x by A18,A23,FUNCT_1:72;
n <= k & k < k + 1 by A18,A23,FINSEQ_1:3,REAL_1:69;
hence thesis by A6,A7,A22,A23,A24,A25,A26,FUNCT_1:def 8;
end;
hence rng q = dom q by A5,XBOOLE_0:def 10;
end; then
A27: for k st P[k] holds P[k+1];
A28: for k holds P[k] from Ind(A2,A27);
len p = len p;
hence thesis by A28;
end;
theorem Th75:
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: P[0] by FINSEQ_1:25;
A2: now let k;
assume A3: P[k];
thus P[k+1]
proof
let p; set q = p - {k + 1}; set x = 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:6;
now let l;
assume that A8: l in dom p and A9: l <> (k + 1)..p and
A10: p.l = k + 1;
p.(x..p) = x by A7,Th29;
then x..p in dom p & p.(x..p) in {k + 1} & p.l in {k + 1}
by A7,A10,Th30,TARSKI:def 1;
then x..p in p " {x} & l in p " {x} by A8,FUNCT_1:def 13;
then A11: {x..p,l} c= p " {k + 1} by ZFMISC_1:38;
card{x..p,l} = 2 & p " {x} is finite
by A9,CARD_2:76;
then 2 <= card(p " {k + 1}) & len q = (k + 1) - card(p " {k + 1})
by A4,A11,CARD_1:80,FINSEQ_3:66;
then 2 + len q <= card(p " {x}) + ((k + 1) - card(p " {k + 1}))
by AXIOMS:24;
then len q + (1 + 1) <= k + 1 by XCMPLX_1:27;
then len q + 1 + 1 <= k + 1 by XCMPLX_1:1;
then len q + 1 <= k by REAL_1:53;
then A12: len q <= k - 1 & dom q = Seg(len q)
by FINSEQ_1:def 3,REAL_1:84;
rng q = Seg(k + 1) \ {k + 1} by A5,A6,FINSEQ_3:72
.= Seg k by RLVECT_1:104;
then A13: card(rng q) = k by FINSEQ_1:78;
A14: Card(rng q) <=` Card(dom q) by CARD_1:28;
reconsider B = dom q as finite set by A12;
rng q is finite & card B = len q by A12,FINSEQ_1:78;
then Card(len q) = Card(dom q) & Card k = Card(rng q)
by A13,CARD_1:def 11;
then k <= len q by A14,CARD_1:72;
then k <= k - 1 by A12,AXIOMS:22;
then k + 1 <= k + 0 by REAL_1:84;
hence contradiction by REAL_1:53;
end;
then A15: p just_once_values k + 1 by A7,Th37;
then A16: len q = (k + 1) - 1 by A4,Th40
.= k by XCMPLX_1:26;
A17: q = (p -| (k + 1)) ^ (p |-- (k + 1)) by A15,Th69;
rng q = Seg(k + 1) \ {k + 1} by A5,A6,FINSEQ_3:72
.= Seg k by RLVECT_1:104;
then dom q = rng q by A16,FINSEQ_1:def 3;
then q is one-to-one by A3,A16;
hence p is one-to-one by A7,A17,Th71;
end;
end;
A18: for k holds P[k] from Ind(A1,A2);
len p = len p;
hence thesis by A18;
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:55;
then A5: dom (q" * p) = dom p by RELAT_1:46
.= 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:47
.= dom q by A3,FUNCT_1:55
.= Seg(len q) by FINSEQ_1:def 3;
then r is one-to-one by A2,A5,Th75;
hence thesis by A4,FUNCT_1:48;
end;
Lm1: for A,B being finite set, f being Function of A,B holds
card A = card B & rng f = B implies
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: rng f = B;
consider p such that A3: rng p = A and A4: p is one-to-one by Th73;
consider q such that A5: rng q = B and A6: q is one-to-one by Th73;
dom p,p .: (dom p) are_equipotent &
dom q,q .: (dom q) are_equipotent by A4,A6,CARD_1:60;
then A7: dom p,A are_equipotent &
dom q,B are_equipotent &
A,B are_equipotent by A1,A3,A5,CARD_1:21,RELAT_1:146;
then dom p,B are_equipotent & B,dom q are_equipotent
by WELLORD2:22;
then A8: dom p,dom q are_equipotent &
dom q = Seg(len q) & Seg(len q) is finite
by FINSEQ_1:def 3,WELLORD2:22;
reconsider X = dom p as finite set by A7,CARD_1:68;
card X = card(Seg(len q)) by A8,CARD_1:81
.= len q by FINSEQ_1:78;
then A9: len q = card(Seg(len p)) by FINSEQ_1:def 3
.= len p by FINSEQ_1:78;
now per cases;
suppose B = {};
hence thesis by A2,RELAT_1:64;
suppose A10: B <> {};
dom(q") = rng q by A6,FUNCT_1:55;
then rng f c= dom(q") by A5,RELSET_1:12;
then dom(q" * f) = dom f by RELAT_1:46;
then rng p = dom(q" * f) by A3,A10,FUNCT_2:def 1;
then A11: dom(q" * f * p) = dom p by RELAT_1:46
.= Seg(len p) by FINSEQ_1:def 3;
then reconsider g = q" * f * p as FinSequence by FINSEQ_1:def 2;
A12: g = q" * (f * p) by RELAT_1:55;
rng p = dom f by A3,A10,FUNCT_2:def 1;
then rng(f * p) = B by A2,RELAT_1:47
.= dom(q") by A5,A6,FUNCT_1:55;
then rng g = rng(q") by A12,RELAT_1:47
.= dom q by A6,FUNCT_1:55
.= Seg(len q) by FINSEQ_1:def 3;
then A13: g is one-to-one by A9,A11,Th75;
q * g = q * (q " * (f * p)) by RELAT_1:55
.= q * q" * (f * p) by RELAT_1:55
.= id(rng q) * (f * p) by A6,FUNCT_1:61
.= id(rng q) * f * p by RELAT_1:55
.= f * p by A2,A5,FUNCT_1:42;
then A14: q * g * p" = f * (p * p") by RELAT_1:55
.= f * id(rng p) by A4,FUNCT_1:61
.= f * id(dom f) by A3,A10,FUNCT_2:def 1
.= f by FUNCT_1:42;
p" is one-to-one & q * g is one-to-one
by A4,A6,A13,FUNCT_1:46,62;
hence thesis by A14,FUNCT_1:46;
end;
hence thesis;
end;
theorem
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:60;
then dom p,rng p are_equipotent by RELAT_1:146;
then Seg(len p),rng p are_equipotent &
Seg(len p) is finite by FINSEQ_1:def 3;
then card(Seg(len p)) = card(rng p) by CARD_1:81;
hence thesis by FINSEQ_1:78;
end;
assume A1: card(rng p) = len p;
reconsider f = p as Function of dom p, rng p by FUNCT_2:3;
A2: card(rng p) = card(Seg(len p)) & Seg(len p) is finite
by A1,FINSEQ_1:78;
then reconsider B = dom p as finite set by FINSEQ_1:def 3;
card(rng p) = card B & dom f is finite by A2,FINSEQ_1:def 3;
hence thesis by Lm1;
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;
theorem
for A,B being finite set, f being Function of A,B
holds card A = card B & f is one-to-one implies rng f = B
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;
consider p such that A3: rng p = A and A4: p is one-to-one by Th73;
consider q such that A5: rng q = B and A6: q is one-to-one by Th73;
dom p,p .: (dom p) are_equipotent &
dom q,q .: (dom q) are_equipotent by A4,A6,CARD_1:60;
then A7: dom p,A are_equipotent &
dom q,B are_equipotent & A,B are_equipotent
by A1,A3,A5,CARD_1:21,RELAT_1:146;
then dom p,B are_equipotent & B,dom q are_equipotent by WELLORD2:22;
then A8: dom p,dom q are_equipotent & dom q = Seg(len q) & Seg(len q)
is finite
by FINSEQ_1:def 3,WELLORD2:22;
reconsider X = dom p as finite set by A7,CARD_1:68;
card X = card(Seg(len q)) by A8,CARD_1:81
.= len q by FINSEQ_1:78;
then A9: len q = card(Seg(len p)) by FINSEQ_1:def 3
.= len p by FINSEQ_1:78;
now per cases;
suppose A10: B = {};
now assume A11: A <> {};
consider x being Element of A;
{x} c= A by A11,ZFMISC_1:37;
then card{x} <= card A by CARD_1:80;
then 1 <= 0 by A1,A10,CARD_1:78,79;
hence contradiction;
end;
hence thesis by A10,PARTFUN1:10,57;
suppose A12: B <> {};
dom(q") = rng q by A6,FUNCT_1:55;
then rng f c= dom(q") by A5,RELSET_1:12;
then dom(q" * f) = dom f by RELAT_1:46;
then rng p = dom(q" * f) by A3,A12,FUNCT_2:def 1;
then A13: dom(q" * f * p) = dom p by RELAT_1:46
.= 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:55;
then rng g c= rng(q") by RELAT_1:45;
then rng g c= dom q by A6,FUNCT_1:55;
then A14: rng g c= dom g by A9,A13,FINSEQ_1:def 3;
q " is one-to-one by A6,FUNCT_1:62;
then q " * f is one-to-one by A2,FUNCT_1:46;
then g is one-to-one by A4,FUNCT_1:46;
then A15: rng g = dom g by A14,Th74;
A16: rng f c= rng q by A5,RELSET_1:12;
A17: q * g = q * (q " * (f * p)) by RELAT_1:55
.= q * q" * (f * p) by RELAT_1:55
.= id(rng q) * (f * p) by A6,FUNCT_1:61
.= id(rng q) * f * p by RELAT_1:55
.= f * p by A16,RELAT_1:79;
rng g = dom q by A9,A13,A15,FINSEQ_1:def 3;
then A18: rng(q * g) = B by A5,RELAT_1:47;
rng p = dom f by A3,A12,FUNCT_2:def 1;
hence thesis by A17,A18,RELAT_1:47;
end;
hence thesis;
end;
theorem
for A,B being finite set, f being Function of A,B
st card A = card B & rng f = B
holds f is one-to-one by Lm1;
theorem
Card B <` 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 <` 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 holds x in dom f & y in
dom f & f.x = f.y implies x = y by A3;
then dom f c= dom f & f is one-to-one by FUNCT_1:def 8;
then dom f,f .: (dom f) are_equipotent by CARD_1:60;
then dom f,rng f are_equipotent by RELAT_1:146;
then Card A = Card(rng f) & rng f c= B by A4,CARD_1:21,RELSET_1:12;
then Card A <=` Card B by CARD_1:27;
hence contradiction by A1,CARD_1:14;
end;
theorem
Card A <` 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 <` 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:47,FUNCT_2:def 1;
rng f = B
proof
thus rng f c= B by RELSET_1:12;
let x;
assume x in B;
then ex y st y in A & f.y = x by A2;
hence thesis by A3,FUNCT_1:def 5;
end;
then Card B <=` Card A by A3,CARD_1:28;
hence thesis by A1,CARD_1:14;
end;