:: Stirling Numbers of the Second Kind
:: by Karol P\c{a}k
::
:: Received March 15, 2005
:: Copyright (c) 2005-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, XBOOLE_0, XXREAL_0, NAT_1, ORDINAL1, CARD_1,
TARSKI, ARYTM_3, ARYTM_1, FUNCT_1, RELAT_1, FUNCT_2, INT_1, FINSET_1,
AFINSQ_1, FINSEQ_1, FINSOP_1, CARD_3, BINOP_2, ZFMISC_1, NEWTON,
REALSET1, STIRL2_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
RELAT_1, FUNCT_1, RELSET_1, SEQ_4, PARTFUN1, FINSET_1, AFINSQ_1,
AFINSQ_2, XXREAL_0, XCMPLX_0, FUNCT_2, INT_1, NAT_1, BINOP_1, BINOP_2,
NEWTON, DOMAIN_1;
constructors WELLORD2, DOMAIN_1, SETWISEO, REAL_1, BINOP_2, SEQ_4, NEWTON,
AFINSQ_2, RELSET_1, PARTFUN3, BINOP_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, BINOP_2, MEMBERED, AFINSQ_1,
CARD_1, VALUED_0, XXREAL_2, RELSET_1, AFINSQ_2, NEWTON;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, FUNCT_1;
equalities ORDINAL1, CARD_1;
expansions TARSKI, XBOOLE_0, FUNCT_1;
theorems AFINSQ_1, TARSKI, FUNCT_1, XBOOLE_0, ZFMISC_1, RELAT_1, XBOOLE_1,
NAT_1, FUNCT_2, AXIOMS, XCMPLX_1, CARD_2, INT_1, ORDINAL1, WELLORD2,
FRAENKEL, SUBSET_1, ENUMSET1, CARD_1, BINOP_2, NEWTON, WSIERP_1, XREAL_1,
XXREAL_0, XXREAL_2, AFINSQ_2;
schemes FUNCT_2, NAT_1, INT_1;
begin
reserve k, l, m, n, i, j for Nat,
K, N for non empty Subset of NAT,
Ke, Ne, Me for Subset of NAT,
X,Y for set;
theorem Th1:
min N = min* N
proof
A1: for n being ExtReal st n in N holds min* N <= n by NAT_1:def 1;
min* N in N by NAT_1:def 1;
hence thesis by A1,XXREAL_2:def 7;
end;
theorem Th2:
min(min K,min N) = min(K\/N)
proof
set m=min(min N,min K);
A1: for k be ExtReal st k in N\/K holds m<=k
proof
let k be ExtReal;
assume k in N\/K;
then k in N or k in K by XBOOLE_0:def 3;
then
A2: min N<=k or min K <=k by XXREAL_2:def 7;
A3: m<=min K by XXREAL_0:17;
m<=min N by XXREAL_0:17;
hence thesis by A2,A3,XXREAL_0:2;
end;
m=min N or m=min K by XXREAL_0:15;
then m in N or m in K by XXREAL_2:def 7;
then m in N\/K by XBOOLE_0:def 3;
hence thesis by A1,XXREAL_2:def 7;
end;
theorem
min(min* Ke,min* Ne) <= min* (Ke\/Ne)
proof
now
per cases;
suppose
Ke is empty or Ne is empty;
then min* Ke=0 & min* Ne >=0 or min* Ne=0 & min*Ke>=0 by NAT_1:def 1;
hence thesis by XXREAL_0:def 9;
end;
suppose
Ke is non empty & Ne is non empty;
then reconsider K=Ke,N=Ne as non empty Subset of NAT;
A1: min N=min* Ne by Th1;
A2: min(K\/N)=min*(Ke\/Ne) by Th1;
min K=min* Ke by Th1;
hence thesis by A1,A2,Th2;
end;
end;
hence thesis;
end;
theorem
not min* Ne in Ne/\Ke implies min* Ne = min* (Ne\Ke)
proof
assume
A1: not min* Ne in Ne/\Ke;
now
per cases;
suppose
Ne is empty;
hence thesis;
end;
suppose
Ne is non empty;
then
A2: min* Ne in Ne by NAT_1:def 1;
then not min* Ne in Ke by A1,XBOOLE_0:def 4;
then
A3: min* Ne in Ne\Ke by A2,XBOOLE_0:def 5;
then
A4: min* (Ne\Ke)<=min* Ne by NAT_1:def 1;
A5: Ne\Ke c=Ne by XBOOLE_1:36;
min* (Ne\Ke) in Ne\Ke by A3,NAT_1:def 1;
then min* Ne<=min* (Ne\Ke) by A5,NAT_1:def 1;
hence thesis by A4,XXREAL_0:1;
end;
end;
hence thesis;
end;
theorem Th5:
for n be Element of NAT holds min* {n} = n & min {n} = n
proof
let n be Element of NAT;
A1: min* {n} in {n} by NAT_1:def 1;
min*{n}=min {n} by Th1;
hence thesis by A1,TARSKI:def 1;
end;
theorem Th6:
for n,k be Element of NAT holds min* {n,k} = min(n,k) & min {n,k} = min(n,k)
proof
let n,k be Element of NAT;
A1: min {n} = n by Th5;
{n,k}={n}\/{k} by ENUMSET1:1;
then
A2: min {n,k} = min(min {n},min {k}) by Th2;
min {n,k} = min* {n,k} by Th1;
hence thesis by A2,A1,Th5;
end;
theorem
for n,k,l be Element of NAT holds min* {n,k,l} = min(n,min(k,l))
proof
let n,k,l be Element of NAT;
A1: min {n,k,l}=min* {n,k,l} by Th1;
{n,k,l}={n}\/{k,l} by ENUMSET1:2;
then
A2: min{n,k,l} = min(min {n},min {k,l}) by Th2;
min {k,l}=min(k,l) by Th6;
hence thesis by A2,A1,Th5;
end;
theorem Th8:
n is Subset of NAT
proof
now
let x be object;
assume x in {l where l is Nat: l natural for Element of Segm n;
coherence;
end;
theorem
N c= n implies n-1 is Element of NAT
proof
A1: min* N in N by NAT_1:def 1;
assume N c= n;
then min*N in n by A1;
then min* N in {l where l is Nat:l {n-1} implies min* N < n-1
proof
assume that
A1: N c= Segm n and
A2: N<>{n-1} and
A3: min* N >=n-1;
now
let k be object such that
A4: k in N;
reconsider k9=k as Element of NAT by A4;
min* N <=k9 by A4,NAT_1:def 1;
then
A5: n-1 <=k9 by A3,XXREAL_0:2;
k9 <= n-1 by A1,A4,Th10;
then n-1 = k by A5,XXREAL_0:1;
hence k in {n-1} by TARSKI:def 1;
end;
then N c= {n-1};
hence thesis by A2,ZFMISC_1:33;
end;
theorem Th14:
Ne c= Segm n & n>0 implies min* Ne <= n-1
proof
assume that
A1: Ne c= Segm n and
A2: n>0;
now
per cases;
suppose
Ne is non empty;
hence thesis by A1,Th12;
end;
suppose
Ne is empty;
then min* Ne =0 by NAT_1:def 1;
hence thesis by A2,NAT_1:20;
end;
end;
hence thesis;
end;
reserve f for Function of Segm n,Segm k;
definition
let n,X;
let f be Function of Segm n,X;
let x be set;
redefine func f"x -> Subset of NAT;
coherence
proof
for y being object st y in f"x holds y in NAT by TARSKI:def 3;
hence thesis by TARSKI:def 3;
end;
end;
definition
let X,k;
let f be Function of X, Segm k;
let x be object;
redefine func f.x -> Element of Segm k;
coherence
proof
per cases;
suppose
x in dom f;
then f.x in rng f by FUNCT_1:3;
hence f.x is Element of Segm k;
end;
suppose
A1: not x in dom f;
A2: k=0 or k>0;
f.x=0 by A1,FUNCT_1:def 2;
hence thesis by A2,NAT_1:44,SUBSET_1:def 1;
end;
end;
end;
definition
let n,k be Nat;
let f be Function of Segm n,Segm k;
attr f is "increasing means
(n = 0 iff k = 0) & for l,m st l in rng f
& m in rng f & l < m holds min* f"{l} < min* f"{m};
end;
theorem Th15:
n=0 & k=0 implies f is onto "increasing
proof
assume that
A1: n=0 and
A2: k=0;
rng f = {} by A1;
hence thesis by A1,A2,FUNCT_2:def 3;
end;
theorem Th16:
n>0 implies min* f"{m} <= n-1
proof
A1: f"{m} c= n
proof
let x be object;
assume x in f"{m};
then x in dom f by FUNCT_1:def 7;
hence thesis;
end;
assume n>0;
hence thesis by A1,Th14;
end;
theorem Th17:
f is onto implies n>=k
proof
assume
A1: f is onto;
now
per cases;
suppose
k=0;
hence thesis;
end;
suppose
A2: k<>0;
A3: rng f = k by A1,FUNCT_2:def 3;
dom f =n by A2,FUNCT_2:def 1;
then Segm card k c= Segm card n by A3,CARD_1:12;
then
A4: card k <= card n by NAT_1:39;
thus thesis by A4;
end;
end;
hence thesis;
end;
theorem Th18:
f is onto "increasing implies for m st m < k holds m <= min* f"{ m}
proof
defpred M[Nat] means $10;
then reconsider k1=k-1 as Element of NAT by NAT_1:20;
defpred I[Integer] means 0<=$1 implies min* f"{$1} <= n-k+$1;
A2: k10;
A5: now
let m9 be object such that
A6: m9 in Segm n;
reconsider m=m9 as Element of NAT by A6;
m in rng f by A1,A2,A6,FUNCT_2:def 3;
then
A7: ex x be object st x in dom f & f.x =m by FUNCT_1:def 3;
m in {m} by TARSKI:def 1;
then reconsider F=f"{m} as non empty Subset of NAT by A7,FUNCT_1:def 7;
A8: m < k by A2,A6,NAT_1:44;
then
A9: m <= min* f"{m} by A1,Th18;
n-k+m =m by A2;
then min* f"{m}<= m by A1,A8,Th19;
then
A10: min* F=m by A9,XXREAL_0:1;
min* F in F by NAT_1:def 1;
then f.m in {m} by A10,FUNCT_1:def 7;
hence f.m9=m9 by TARSKI:def 1;
end;
dom f = n by A2,A4,FUNCT_2:def 1;
hence thesis by A5,FUNCT_1:17;
end;
end;
hence thesis;
end;
theorem
f = id n & n > 0 implies f is "increasing
proof
assume that
A1: f = id n and
A2: n>0;
A3: ex x be object st x in n by A2,XBOOLE_0:def 1;
A4: now
let l,m such that
A5: l in rng f and
A6: m in rng f and
A7: l0;
then consider f be Function such that
A4: dom f=n and
A5: rng f={0} by FUNCT_1:5;
reconsider f as Function of n,{0} by A4,A5,FUNCT_2:1;
rng f c= Segm k
proof
let x be object such that
A6: x in rng f;
x=0 by A6,TARSKI:def 1;
hence thesis by A1,A6,NAT_1:44;
end;
then reconsider f as Function of Segm n,Segm k by FUNCT_2:6;
for l,m st l in rng f & m in rng f & l < m holds min* f"{l} < min*
f"{m} by A5,TARSKI:def 1;
then f is "increasing by A1;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th23:
(n=0 iff k=0) & n>=k implies
ex f be Function of Segm n,Segm k st f is onto "increasing
proof
assume that
A1: n=0 iff k=0 and
A2: n>=k;
now
per cases;
suppose
A3: n=0;
set f={};
A4: dom f = n by A3;
rng f= k by A1,A3;
then reconsider f as Function of Segm n,Segm k by A4,FUNCT_2:1;
f is onto "increasing by A1,Th15;
hence thesis;
end;
suppose
A5: n>0;
then reconsider k1=k-1 as Element of NAT by A1,NAT_1:20;
reconsider k,n as non zero Element of NAT by A1,A5,ORDINAL1:def 12;
defpred F[Element of Segm n,Element of Segm k] means $2=min($1,k1);
A6: for x be Element of Segm n ex y be Element of Segm k st F[x,y]
proof
let x be Element of Segm n;
A7: k1 Nat,P[set]}:
{f where f is Function of Segm n(),Segm k():P[f]} is finite
proof
set F= {f where f is Function of Segm n(),Segm k():P[f]};
now
per cases;
suppose
A1: k()=0;
F c= {{}}
proof
let x be object;
assume x in F;
then consider f be Function of n(),k() such that
A2: x=f and
P[f];
f ={} by A1;
hence thesis by A2,TARSKI:def 1;
end;
hence thesis;
end;
suppose
A3: k()>0;
A4: F c= Funcs(n(),k())
proof
let x be object;
assume x in F;
then ex f be Function of n(),k() st x=f & P[f];
hence thesis by A3,FUNCT_2:8;
end;
Funcs(n(),k()) is finite by FRAENKEL:6;
hence thesis by A4;
end;
end;
hence thesis;
end;
theorem Th24:
for n,k holds
{f where f is Function of Segm n,Segm k:f is onto "increasing} is finite
proof
let n,k;
defpred P[Function of Segm n,Segm k] means $1 is onto "increasing;
{f where f is Function of Segm n,Segm k:P[f]} is finite from Sch1;
hence thesis;
end;
theorem Th25:
for n,k holds
card {f where f is Function of Segm n,Segm k:f is onto "increasing}
is Element of NAT
proof
let n,k;
set F= {f where f is Function of Segm n,Segm k:f is onto "increasing};
F is finite by Th24;
then reconsider m = card F as Nat;
card F=card m;
hence thesis;
end;
:: Stirling Numbers of the second kind
definition
let n,k be Nat;
func n block k -> set equals
card {f where f is Function of Segm n,Segm k:f is onto "increasing};
coherence;
end;
registration
let n,k be Nat;
cluster n block k -> natural;
coherence by Th25;
end;
theorem Th26:
n block n = 1
proof
set F={f where f is Function of Segm n,Segm n:f is onto "increasing};
A1: F c= {id n}
proof
let x be object;
assume x in F;
then consider f be Function of Segm n,Segm n such that
A2: x=f and
A3: f is onto "increasing;
f=id n by A3,Th20;
hence thesis by A2,TARSKI:def 1;
end;
n=0 iff n=0;
then consider f be Function of Segm n,Segm n such that
A4: f is onto "increasing by Th23;
f in F by A4;
then F={id n} by A1,ZFMISC_1:33;
hence thesis by CARD_1:30;
end;
theorem Th27:
k<>0 implies 0 block k = 0
proof
set F={f where f is Function of Segm 0,Segm k:f is onto "increasing};
assume
A1: k<>0;
F ={}
proof
assume F<>{};
then consider x be object such that
A2: x in F by XBOOLE_0:def 1;
ex f be Function of Segm 0,Segm k st x=f & f is onto "increasing by A2;
hence thesis by A1;
end;
hence thesis;
end;
theorem
0 block k = 1 iff k=0 by Th26,Th27;
theorem Th29:
n{};
then consider x be object such that
A2: x in F by XBOOLE_0:def 1;
ex f be Function of Segm n,Segm k st x=f & f is onto "increasing by A2;
hence contradiction by A1,Th17;
end;
hence thesis;
end;
theorem
n block 0 = 1 iff n=0
proof
n block 0 = 1 implies n=0
proof
set F={f where f is Function of Segm n,Segm 0:f is onto "increasing};
A1: card {{}}= 1 by CARD_1:30;
assume n block 0=1;
then consider x be object such that
A2: F={x} by A1,CARD_1:29;
x in F by A2,TARSKI:def 1;
then ex f be Function of Segm n,Segm 0 st x=f & f is onto "increasing;
hence thesis;
end;
hence thesis by Th26;
end;
theorem Th31:
n<>0 implies n block 0 = 0
proof
set F={f where f is Function of Segm n,Segm 0:f is onto "increasing};
assume
A1: n<>0;
F ={}
proof
assume F<>{};
then consider x be object such that
A2: x in F by XBOOLE_0:def 1;
ex f be Function of Segm n,Segm 0 st x=f & f is onto "increasing by A2;
hence contradiction by A1;
end;
hence thesis;
end;
theorem Th32:
n<>0 implies n block 1 = 1
proof
set F={g where g is Function of Segm n,Segm 1:g is onto "increasing};
assume n<>0;
then n >=1+0 by NAT_1:13;
then consider f be Function of Segm n,Segm 1 such that
A1: f is onto "increasing by Th23;
A2: F c= {f}
proof
let x be object;
assume x in F;
then consider g be Function of Segm n,Segm 1 such that
A3: x=g and
g is onto "increasing;
f=g by CARD_1:49,FUNCT_2:51;
hence thesis by A3,TARSKI:def 1;
end;
f in F by A1;
then F={f} by A2,ZFMISC_1:33;
hence thesis by CARD_1:30;
end;
theorem
1<=k & k <=n or k=n iff n block k qua Nat > 0
proof
thus 1<=k & k <=n or k=n implies n block k > 0
proof
set F={g where g is Function of Segm n,Segm k:g is onto "increasing};
assume that
A1: 1<=k & k <=n or k=n;
k=0 iff n=0 by A1;
then consider f such that
A2: f is onto "increasing by A1,Th23;
f in F by A2;
hence thesis;
end;
thus n block k > 0 implies 1<=k & k <=n or k=n
proof
assume
A3: n block k >0;
assume
A4: not ( 1<=k & k <=n or k=n);
then 1+0>k or k>n;
then k=0 & n<>k or k>n by A4,NAT_1:13;
hence contradiction by A3,Th29,Th31;
end;
end;
reserve x,y for set;
scheme
Sch2{X,Y,X1,Y1()->set,f()->Function of X(),Y(),F(object)->object}:
ex h be
Function of X1(),Y1() st h|X() = f() & for x st x in X1()\X() holds h.x = F(x)
provided
A1: for x st x in X1()\X() holds F(x) in Y1() and
A2: X() c= X1() & Y() c= Y1() and
A3: Y() is empty implies X() is empty
proof
defpred P[object,object] means
($1 in X() implies $2 = f().$1) & ($1 in X1()\X()
implies $2=F($1));
A4: for x being object st x in X1() ex y being object st y in Y1() & P[x,y]
proof
let x being object such that
A5: x in X1();
now
per cases;
suppose
A6: x in X();
then x in dom f() by A3,FUNCT_2:def 1;
then f().x in rng f() by FUNCT_1:def 3;
then
A7: f().x in Y1() by A2;
not x in X1()\X() by A6,XBOOLE_0:def 5;
hence thesis by A7;
end;
suppose
A8: not x in X();
then x in X1()\X() by A5,XBOOLE_0:def 5;
then F(x) in Y1() by A1;
hence thesis by A8;
end;
end;
hence thesis;
end;
consider h be Function of X1(),Y1() such that
A9: for x being object st x in X1() holds P[x,h.x] from FUNCT_2:sch 1(A4);
A10: dom f() = dom h /\ X()
proof
now
per cases;
suppose
Y() is empty;
hence thesis by A3;
end;
suppose
A11: Y() is non empty;
then Y1() is non empty by A2;
then
A12: dom h =X1() by FUNCT_2:def 1;
dom f()=X() by A11,FUNCT_2:def 1;
hence thesis by A2,A12,XBOOLE_1:28;
end;
end;
hence thesis;
end;
take h;
for x being object st x in dom f() holds h.x = f().x
proof
let x be object;
assume x in dom f();
then x in X();
hence thesis by A2,A9;
end;
hence h|X() = f() by A10,FUNCT_1:46;
thus thesis by A9;
end;
scheme
Sch3{X,Y,X1,Y1()->set,F(object)->object,P[set,set,set]}:
card{f where f is Function of X(),Y(): P[f,X(),Y()]}
= card{f where f is Function of X1(),Y1():
P[f,X1(),Y1()]& rng (f|X()) c=Y()&
(for x st x in X1()\X() holds f.x=F(x))}
provided
A1: for x st x in X1()\X() holds F(x) in Y1() and
A2: X() c= X1() & Y() c= Y1() and
A3: Y() is empty implies X() is empty and
A4: for f be Function of X1(),Y1() st (for x st x in X1()\X() holds F(x)
=f.x) holds P[f,X1(),Y1()] iff P[f|X(),X(),Y()]
proof
defpred FF[object,object] means
for f be Function of X(),Y(),h be Function of X1()
,Y1() st f=$1 & h=$2 holds h|X()=f;
set F2={f where f is Function of X1(),Y1(): P[f,X1(),Y1()]& rng (f|X()) c=Y(
)& for x st x in X1()\X() holds f.x=F(x)};
set F1={f where f is Function of X(),Y(): P[f,X(),Y()]};
A5: for f9 be object st f9 in F1 ex g9 be object st g9 in F2 & FF[f9,g9]
proof
let f9 be object;
assume f9 in F1;
then consider f be Function of X(),Y() such that
A6: f=f9 and
A7: P[f,X(),Y()];
consider h be Function of X1(),Y1() such that
A8: h|X() = f & for x st x in X1()\X() holds h.x=F(x) from Sch2(A1,A2
, A3);
A9: FF[f9,h] by A6,A8;
A10: rng f c= Y();
P[h,X1(),Y1()] by A4,A7,A8;
then h in F2 by A8,A10;
hence thesis by A9;
end;
consider ff be Function of F1,F2 such that
A11: for x be object st x in F1 holds FF[x,ff.x] from FUNCT_2:sch 1(A5);
A12: Y1() is empty implies X1() is empty
by A1,A2,A3;
now
per cases;
suppose
A13: Y1() is empty;
set Empty={};
A14: F2 c= {{}}
proof
let x be object;
assume x in F2;
then
ex f be Function of X1(),Y1() st f=x &( P[f,X1(),Y1()])& rng (f
|X()) c=Y() & for x st x in X1()\X() holds f.x=F(x);
then x={} by A13;
hence thesis by TARSKI:def 1;
end;
A15: F1 c= {{}}
proof
let x be object;
assume x in F1;
then ex f be Function of X(),Y() st f=x & P[f,X(),Y()];
then x={} by A2,A13;
hence thesis by TARSKI:def 1;
end;
now
per cases;
suppose
A16: P[{},{},{}];
A17: rng {}={};
A18: Y() is empty by A2,A13;
{} is Function of X(),Y() by A3,A18,A17,FUNCT_2:1;
then {} in F1 by A3,A16,A18;
then
A19: F1={{}} by A15,ZFMISC_1:33;
A20: rng {}={};
reconsider Empty as Function of X1(),Y1() by A12,A13,A20,
FUNCT_2:1;
A21: for x st x in X1()\X() holds Empty.x=F(x) by A12;
rng (Empty|X()) c= Y();
then {} in F2 by A12,A13,A16,A21;
hence thesis by A14,A19,ZFMISC_1:33;
end;
suppose
A22: not P[{},{},{}];
A23: not {} in F1
proof
assume {} in F1;
then ex f be Function of X(),Y() st f={} & P[f,X(),Y()];
hence contradiction by A2,A3,A13,A22;
end;
A24: F2={} or F2={{}} by A14,ZFMISC_1:33;
A25: not {} in F2
proof
assume {} in F2;
then ex f be Function of X1(),Y1() st f={} & P[f,X1(),Y1()] & rng
(f|X()) c= Y() & for x st x in X1()\X() holds f.x=F(x);
hence contradiction by A12,A13,A22;
end;
F1={} or F1={{}} by A15,ZFMISC_1:33;
hence thesis by A23,A25,A24,TARSKI:def 1;
end;
end;
hence thesis;
end;
suppose
A26: Y1() is non empty;
now
per cases;
suppose
A27: F2 is empty;
F1 is empty
proof
assume F1 is non empty;
then consider x being object such that
A28: x in F1;
consider f be Function of X(),Y() such that
f=x and
A29: P[f,X(),Y()] by A28;
A30: rng f c= Y();
consider h be Function of X1(),Y1() such that
A31: h|X() = f & for x st x in X1()\X() holds h.x=F(x) from
Sch2(A1,A2,A3);
P[h,X1(),Y1()] by A4,A29,A31;
then h in F2 by A31,A30;
hence thesis by A27;
end;
hence thesis by A27;
end;
suppose
A32: F2 is non empty;
F2 c= rng ff
proof
let y be object;
assume y in F2;
then consider f be Function of X1(),Y1() such that
A33: f=y and
A34: P[f,X1(),Y1()] and
A35: rng (f|X()) c=Y() and
A36: for x st x in X1()\X() holds f.x=F(x);
A37: dom (f|X())=dom f /\ X() by RELAT_1:61;
dom f =X1() by A26,FUNCT_2:def 1;
then
A38: dom (f|X())=X() by A2,A37,XBOOLE_1:28;
then reconsider h=f|X() as Function of X(),rng(f|X()) by FUNCT_2:1;
rng (f|X()) is empty implies X() is empty by A38,RELAT_1:42;
then reconsider h as Function of X(),Y() by A35,FUNCT_2:6;
P[f|X(),X(),Y()] by A4,A34,A36;
then
A39: h in F1;
A40: dom ff=F1 by A32,FUNCT_2:def 1;
then ff.h in rng ff by A39,FUNCT_1:def 3;
then ff.h in F2;
then consider ffh be Function of X1(),Y1() such that
A41: ffh=ff.h and
P[ffh,X1(),Y1()] and
rng (ffh|X()) c=Y() and
A42: for x st x in X1()\X() holds ffh.x=F(x);
now
let x be object such that
A43: x in X1();
now
per cases;
suppose
x in X();
then
A44: x in dom h by A3,FUNCT_2:def 1;
ffh|X()=h by A11,A39,A41;
then h.x=ffh.x by A44,FUNCT_1:47;
hence ffh.x=f.x by A44,FUNCT_1:47;
end;
suppose
not x in X();
then
A45: x in X1()\X() by A43,XBOOLE_0:def 5;
then ffh.x=F(x) by A42;
hence ffh.x=f.x by A36,A45;
end;
end;
hence ffh.x=f.x;
end;
then ffh=f by FUNCT_2:12;
hence thesis by A33,A39,A40,A41,FUNCT_1:def 3;
end;
then
A46: rng ff=F2;
for x1,x2 be object st x1 in F1 & x2 in F1 & ff.x1=ff.x2
holds x1= x2
proof
let x1,x2 be object such that
A47: x1 in F1 and
A48: x2 in F1 and
A49: ff.x1=ff.x2;
A50: ex f2 be Function of X(),Y() st x2=f2 & P[f2,X(),Y()] by A48;
dom ff= F1 by A32,FUNCT_2:def 1;
then ff.x1 in rng ff by A47,FUNCT_1:def 3;
then ff.x1 in F2;
then consider F1 be Function of X1(),Y1() such that
A51: ff.x1=F1 and
P[F1,X1(),Y1()] and
rng (F1|X()) c=Y() and
for x st x in X1()\X() holds F1.x=F(x);
consider f1 be Function of X(),Y() such that
A52: x1=f1 and
P[f1,X(),Y()] by A47;
F1|X()=f1 by A11,A47,A52,A51;
hence thesis by A11,A48,A49,A52,A50,A51;
end;
then
A53: ff is one-to-one by A32,FUNCT_2:19;
dom ff=F1 by A32,FUNCT_2:def 1;
then F1,F2 are_equipotent by A46,A53,WELLORD2:def 4;
hence thesis by CARD_1:5;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
scheme
Sch4{X,Y()->set, x,y()->object,P[set,set,set]}:
card{f where f is Function of X(),Y(): P[f,X(),Y()]}
= card{f where f is Function of (X()\/{x()}),(Y()\/{y()}): P[f,X()
\/{x()},Y()\/{y()}] & rng (f|X()) c=Y() & f.x()=y()}
provided
A1: Y() is empty implies X() is empty and
A2: not x() in X() and
A3: for f be Function of X()\/{x()},Y()\/{y()} st f.x()=y() holds P[f,X(
)\/{x()},Y()\/{y()}] iff P[f|X(),X(),Y()]
proof
set Y1=Y()\/{y()};
set X1=X()\/{x()};
deffunc F(set)=y();
A4: for f be Function of X1,Y1 holds (for x st x in X1\X() holds F(x)=f.x)
iff f.x()=y()
proof
let f be Function of X1,Y1;
A5: X1\X()={x()}\X() by XBOOLE_1:40
.={x()} by A2,ZFMISC_1:59;
thus (for x st x in X1\X() holds F(x)=f.x) implies f.x()=y()
proof
A6: x() in {x()} by TARSKI:def 1;
assume for x st x in X1\X() holds F(x)=f.x;
hence thesis by A5,A6;
end;
thus thesis by A5,TARSKI:def 1;
end;
A7: for f be Function of X1,Y1 st (for x st x in X1\X() holds F(x)=f.x)
holds P[f,X1,Y1] iff P[f|X(),X(),Y()]
proof
let f be Function of X1,Y1;
assume for x st x in X1\X() holds F(x)=f.x;
then y()=f.x() by A4;
hence thesis by A3;
end;
set F2={f where f is Function of X1,Y1: P[f,X1,Y1]& rng (f|X()) c=Y()& f.x()
=y()};
set F1={f where f is Function of X1,Y1: P[f,X1,Y1]& rng (f|X()) c=Y()& for x
st x in X1\X() holds f.x=F(x)};
A8: for x st x in X1\X() holds F(x) in Y1
proof
let x such that
x in X1\X();
A9: {y()} c=Y1 by XBOOLE_1:7;
y() in {y()} by TARSKI:def 1;
hence thesis by A9;
end;
A10: F1 c= F2
proof
let x be object;
assume x in F1;
then consider f be Function of X1,Y1 such that
A11: x=f and
A12: P[f,X1,Y1] and
A13: rng (f|X()) c=Y() and
A14: for x st x in X1\X() holds f.x=F(x);
f.x()=y() by A4,A14;
hence thesis by A11,A12,A13;
end;
A15: F2 c= F1
proof
let x be object;
assume x in F2;
then consider f be Function of X1,Y1 such that
A16: x=f and
A17: P[f,X1,Y1] and
A18: rng (f|X()) c=Y() and
A19: f.x()=y();
for x st x in X1\X() holds F(x)=f.x by A4,A19;
hence thesis by A16,A17,A18;
end;
A20: X()c=X1 & Y()c=Y1 by XBOOLE_1:7;
card{f where f is Function of X(),Y():P[f,X(),Y()]}= card F1 from Sch3(
A8,A20,A1,A7);
hence thesis by A10,A15,XBOOLE_0:def 10;
end;
theorem Th34:
for f be Function of Segm(n+1),Segm(k+1)
st f is onto "increasing & f"{f.n}=
{n} holds f.n=k
proof
let f be Function of Segm(n+1),Segm(k+1) such that
A1: f is onto "increasing and
A2: f"{f.n}={n};
assume
A3: f.n<>k;
now
per cases by A3,XXREAL_0:1;
suppose
A4: f.n>k;
f.n0 & f"{f.n}<>{n}
ex m st m in f"{f.n} & m<>n
proof
let f be Function of Segm(n+1), Segm k such that
A1: k<>0 and
A2: f"{f.n}<>{n};
A3: nn by A2,ZFMISC_1:35;
hence thesis;
end;
theorem Th36:
for f be Function of Segm n, Segm k,
g be Function of Segm(n+m),Segm(k+l) st g is
"increasing & f=g|n holds for i,j st i in rng f & j in rng f & i=k+1 by A1,Th17;
then k=0 by XREAL_1:6;
hence thesis by A3,Th15;
end;
suppose
A4: n>0;
thus
A5: rng (f|n) c= Segm k
proof
let fi be object such that
A6: fi in rng (f|n);
rng(f|n) c= rng f by RELAT_1:70;
then fi in rng f by A6;
then
A7: fi in k+1;
k+1 is Subset of NAT by Th8;
then reconsider fi as Element of NAT by A7;
consider i be object such that
A8: i in dom (f|n) and
A9: (f|n).i=fi by A6,FUNCT_1:def 3;
i in dom f /\n by A8,RELAT_1:61;
then
A10: i in n by XBOOLE_0:def 4;
n is Subset of NAT by Th8;
then reconsider i as Element of NAT by A10;
A11: f.i=k;
then
A13: f.i=k by A12,XXREAL_0:1;
A14: f.i in {f.i} by TARSKI:def 1;
A15: f.n=k by A1,A2,Th34;
A16: i in dom f/\n by A8,RELAT_1:61;
then i in dom f by XBOOLE_0:def 4;
then i in f"{f.n} by A13,A14,A15,FUNCT_1:def 7;
then i >= min* f"{f.n} & i in NAT & n in NAT
by NAT_1:def 1,ORDINAL1:def 12;
then
A17: i >= n by A2,Th5;
i in Segm n by A16,XBOOLE_0:def 4;
hence contradiction by A17,NAT_1:44;
end;
f.i=(f|n).i by A8,FUNCT_1:47;
hence thesis by A9,A11,NAT_1:44;
end;
thus for g be Function of Segm n,Segm k st g=f|n holds
g is onto "increasing
proof
let g be Function of Segm n,Segm k such that
A18: g=f|n;
Segm k c=rng g
proof
nn by A,A21,A25;
then
A27: n1 < n by A26,XXREAL_0:1;
dom f /\n=dom (f|n) by RELAT_1:61;
then
A28: n1 in dom g by A18,A27,A20,NAT_1:44;
then g.n1 in rng g by FUNCT_1:def 3;
hence thesis by A18,A25,A28,FUNCT_1:47;
end;
then k=rng g;
hence g is onto by FUNCT_2:def 3;
A29: dom f /\n=dom (f|n) by RELAT_1:61;
n{n} & f|n =g holds g is onto "increasing
proof
let f be Function of Segm(n+1),Segm k,
g be Function of Segm n,Segm k such that
A1: f is onto "increasing and
A2: f"{f.n}<>{n} and
A3: f|n =g;
now
per cases;
suppose
k=0;
hence thesis by A1;
end;
suppose
A4: k>0;
A5: rng f = k by A1,FUNCT_2:def 3;
now
k=k+0;
then
A6: for i,j st i in rng g & j in rng g & in by A2,A4,A10,Th35;
f.m in {k1} by A15,FUNCT_1:def 7;
then
A17: f.m=k1 by TARSKI:def 1;
m in dom f by A15,FUNCT_1:def 7;
then mg.n;
dom g=n+1 by A6,FUNCT_2:def 1;
then reconsider x as Element of NAT by A8;
x0 by A1,A11;
then
A13: dom f=n by FUNCT_2:def 1;
f.x=g.x by A3,A11;
hence contradiction by A7,A9,A13,A12,FUNCT_1:def 3;
end;
A14: for l st l in rng g & not l in rng f holds min* g"{l}=n
proof
A15: n n;
min* g"{l} <= (n+1)-1 by Th16;
then
A22: min* g"{l}< n by A21,XXREAL_0:1;
then k<>0 by A1;
then
A23: dom f=n by FUNCT_2:def 1;
min* g"{l} in Segm n by A22,NAT_1:44;
then
A24: f.min* g"{l} in rng f by A23,FUNCT_1:def 3;
f.min* g"{l}=g.min* g"{l} by A3,A22;
hence contradiction by A17,A20,A24,TARSKI:def 1;
end;
A25: for k1 be Element of NAT st k1 in rng f holds min* g"{k1}=min* f"{k1}
proof
n <= n+1 by NAT_1:11;
then
A26: Segm n c= Segm(n+1) by NAT_1:39;
let k1 be Element of NAT such that
A27: k1 in rng f;
consider x be object such that
A28: x in dom f and
A29: f.x=k1 by A27,FUNCT_1:def 3;
A30: x in n by A28;
Segm k is non empty by A27;
then k is non zero;
then k+m is non zero;
then Segm(k+m) is non empty;
then
A31: dom g = Segm(n+1) by FUNCT_2:def 1;
n is Subset of NAT by Th8;
then reconsider x as Element of NAT by A30;
k1 in {k1} by TARSKI:def 1;
then
A32: x in f"{k1} by A28,A29,FUNCT_1:def 7;
then
A33: min* f"{k1} <= x by NAT_1:def 1;
A34: x =k
proof
let l such that
l in rng g and
A47: not l in rng f;
assume l0;
then min* f"{i} <= n-1 by Th16;
then
A53: min* g"{i} <=n-1 by A25,A51,A48;
n-1 is Element of NAT by A52,NAT_1:20;
then
A54: (n-1)<(n-1)+1 by NAT_1:13;
min* g"{j}=n by A44,A14,A51;
hence thesis by A53,A54,XXREAL_0:2;
end;
suppose
A55: not i in rng f & j in rng f;
then
A56: j< k by NAT_1:44;
i>=k by A43,A46,A55;
hence thesis by A45,A56,XXREAL_0:2;
end;
suppose
A57: not i in rng f & not j in rng f;
then i=g.n by A43,A5;
hence thesis by A44,A45,A5,A57;
end;
end;
hence thesis;
end;
theorem Th40:
for f be Function of Segm n,Segm k,
g be Function of Segm(n+1),Segm(k+1) st f is onto
"increasing & f=g|Segm n & g.n = k
holds g is onto "increasing & g"{g.n}={n}
proof
let f be Function of Segm n,Segm k,
g be Function of Segm(n+1),Segm(k+1) such that
A1: f is onto "increasing and
A2: f=g|Segm n and
A3: g.n = k;
Segm(k+1) c= rng g
proof
let x9 be object such that
A4: x9 in Segm(k+1);
reconsider x=x9 as Element of NAT by A4;
x{n};
then consider m such that
A15: m in g"{g.n} and
A16: m<>n by Th35;
g.m in {g.n} by A15,FUNCT_1:def 7;
then
A17: g.m=k by A3,TARSKI:def 1;
m in dom g by A15,FUNCT_1:def 7;
then m{n}
proof
let f be Function of Segm n,Segm k,
g be Function of Segm(n+1),Segm k such that
A1: f is onto "increasing and
A2: f=g|Segm n and
A3: g.n < k;
k=rng f by A1,FUNCT_2:def 3;
then consider x being object such that
A4: x in dom f and
A5: f.x=g.n by A3,FUNCT_1:def 3;
g.n=g.x by A2,A4,A5,FUNCT_1:47;
then
A6: g.x in {g.n} by TARSKI:def 1;
k c= rng g
proof
n<=n+1 by NAT_1:13;
then
A7: Segm n c= Segm(n+1) by NAT_1:39;
n=0 iff k=0 by A1;
then
A8: dom f = n by FUNCT_2:def 1;
let x9 be object such that
A9: x9 in k;
k is Subset of NAT by Th8;
then reconsider x=x9 as Element of NAT by A9;
rng f=k by A1,FUNCT_2:def 3;
then consider y be object such that
A10: y in dom f and
A11: f.y =x by A9,FUNCT_1:def 3;
A12: dom g = n+1 by A3,FUNCT_2:def 1;
f.y=g.y by A2,A10,FUNCT_1:47;
hence thesis by A10,A11,A8,A7,A12,FUNCT_1:def 3;
end;
then k=rng g;
hence g is onto by FUNCT_2:def 3;
k=k+0;
then for i,j st i in rng g & j in rng g & in by A;
dom g=n+1 by A3,FUNCT_2:def 1;
then x in g"{g.n} by A14,A13,A6,FUNCT_1:def 7;
hence thesis by A15,TARSKI:def 1;
end;
Lm1: k0;
A2: F1 is empty
proof
assume F1 is non empty;
then consider x be object such that
A3: x in F1;
consider f be Function of Segm(n+1),Segm(k+1) such that
x=f and
f is onto "increasing and
A4: f"{f.n}={n} by A3;
0 in Segm(n+1) by NAT_1:44;
then
A5: 0 in dom f by FUNCT_2:def 1;
A6: 0 in {0} by TARSKI:def 1;
A7: f.0=0 by A1,CARD_1:49,TARSKI:def 1;
f.n=0 by A1,CARD_1:49,TARSKI:def 1;
then 0 in {n} by A4,A7,A5,A6,FUNCT_1:def 7;
hence thesis by A1;
end;
n block k =0 by A1,Th31;
hence thesis by A2;
end;
suppose
A8: k=0 implies n=0;
defpred P[object,set,set] means for i,j st Segm i=$2 & Segm j=$3
ex f be Function of Segm i,Segm j
st f=$1 & f is onto "increasing & (n < i implies f"{f.n}={n});
A9: not n in Segm n;
set FF2={f where f is Function of Segm n,Segm k: P[f,Segm n,Segm k]};
set FF1={f where f is Function of (Segm n\/{n}),(Segm k\/{k}):
P[f,Segm n\/{n},Segm k\/{k}]& rng (f|Segm n) c= Segm k & f.n=k};
A10: for f be Function of Segm n\/{n},Segm k\/{k} st f.n=k
holds P[f,Segm n\/{n}, Segm k\/{k}] iff P[f|Segm n,Segm n,Segm k]
proof
let f9 be Function of Segm n\/{n},Segm k\/{k} such that
A11: f9.n=k;
thus P[f9,Segm n\/{n},Segm k\/{k}] implies P[f9|Segm n,Segm n,Segm k]
proof
n<=n+1 by NAT_1:11;
then
A12: Segm n c= Segm(n+1) by NAT_1:39;
A13: Segm(n+1)= Segm n \/ {n} by AFINSQ_1:2;
A14: Segm(k+1)= Segm k \/ {k} by AFINSQ_1:2;
assume P[f9,Segm n\/{n},Segm k\/{k}];
then consider f be Function of Segm(n+1),Segm(k+1) such that
A15: f=f9 and
A16: f is onto "increasing and
A17: n < n+1 implies f"{f.n}={n} by A13,A14;
A18: rng (f|n) c= Segm k by A16,A17,Th37,NAT_1:13;
A19: dom (f|n)=dom f /\ n by RELAT_1:61;
dom f=n+1 by FUNCT_2:def 1;
then dom (f|n)=n by A12,A19,XBOOLE_1:28;
then reconsider fn=f|n as Function of n,k by A18,FUNCT_2:2;
let i,j such that
A20: Segm i= Segm n and
A21: Segm j= Segm k;
reconsider fi=fn as Function of Segm i,Segm j by A20,A21;
fi is onto "increasing by A16,A17,A20,A21,Th37,NAT_1:13;
hence thesis by A15,A20;
end;
thus P[f9|Segm n,Segm n,Segm k] implies P[f9,Segm n\/{n},Segm k\/{k}]
proof
Segm n\/{n}= Segm(n+1) by AFINSQ_1:2;
then reconsider f=f9 as Function of Segm(n+1),Segm(k+1)
by AFINSQ_1:2;
assume P[f9|Segm n,Segm n,Segm k];
then
A22: ex fn be Function of Segm n,Segm k
st fn=f9|n & fn is onto "increasing
&( n < n implies fn"{fn.n}={n});
let i,j such that
A23: Segm i= Segm n\/{n} and
A24: Segm j= Segm k\/{k};
reconsider f1=f as Function of Segm i,Segm j by A23,A24;
A25: for f be Function of Segm n,Segm k,
f1 being Function of Segm(n+1),Segm(k+1)
st f is onto
"increasing & f=f1|Segm n & f1.n = k
holds f1"{f1.n}={n} by Th40;
A26: n < i implies f1"{f1.n}={n} by A11,A22,A25;
A27: Segm(k+1) =j by A24,AFINSQ_1:2;
Segm(n+1)=i by A23,AFINSQ_1:2;
then f1 is onto "increasing by A11,A22,A27,Th40;
hence thesis by A26;
end;
end;
A28: Segm k is empty implies Segm n is empty by A8;
A29: card FF2 = card FF1 from Sch4(A28,A9,A10);
A30: F2 c=FF2
proof
let x be object;
assume x in F2;
then
A31: ex f be Function of Segm n,Segm k st x=f & f is onto "increasing;
then P[x,n,k];
hence thesis by A31;
end;
A32: F1 c=FF1
proof
let x be object;
assume x in F1;
then consider f be Function of Segm(n+1),Segm(k+1) such that
A33: f=x and
A34: f is onto "increasing and
A35: f"{f.n}={n};
A36: rng (f|n) c= Segm k by A34,A35,Th37;
A37: P[f,Segm n\/{n}, Segm k\/{k}]
proof
let i,j such that
A38: Segm i= Segm n\/{n} and
A39: Segm j= Segm k\/{k};
A40: Segm j= Segm(k+1) by A39,AFINSQ_1:2;
Segm i= Segm(n+1) by A38,AFINSQ_1:2;
hence thesis by A34,A35,A40;
end;
A41: Segm(k+1)= Segm k\/{k} by AFINSQ_1:2;
A42: Segm(n+1)= Segm n\/{n} by AFINSQ_1:2;
f.n=k by A34,A35,Th34;
hence thesis by A33,A37,A36,A42,A41;
end;
A43: FF2 c= F2
proof
let x be object;
assume x in FF2;
then consider f be Function of n,k such that
A44: x=f and
A45: P[f,n,k];
ex g be Function of Segm n,Segm k
st g=f & g is onto "increasing & (n < n
implies g"{g.n}={n}) by A45;
hence thesis by A44;
end;
FF1 c=F1
proof
let x be object;
assume x in FF1;
then consider f be Function of (n\/{n}),(k\/{k})such that
A46: x=f and
A47: P[f,n\/{n},k\/{k}] and
rng (f|n) c=k and
f.n=k;
A48: Segm(k+1)= Segm k\/{k} by AFINSQ_1:2;
Segm(n+1)= Segm n\/{n} by AFINSQ_1:2;
then
ex f9 be Function of Segm(n+1),Segm(k+1)
st f=f9 & f9 is onto "increasing & (
n < n+1 implies f9"{f9.n}={n}) by A47,A48;
hence thesis by A46,NAT_1:13;
end;
then F1=FF1 by A32;
hence thesis by A29,A30,A43,XBOOLE_0:def 10;
end;
end;
hence thesis;
end;
theorem Th43:
for l st l{n} & f.n=l}
= card{f where f is Function of Segm n,Segm k: f is onto "increasing}
proof
let l such that
A1: l{n}
& f.n=l};
now
per cases;
suppose
k=0 & n<>0;
hence thesis by A1;
end;
suppose
A2: k=0 implies n=0;
defpred P[object,set,set] means for i,j st Segm i= $2 & Segm j=$3
ex f be Function of Segm i,Segm j
st f=$1 & f is onto "increasing & (n < i implies f"{f.n}<>{n});
A3: not n in Segm n;
set FF2={f where f is Function of Segm n,Segm k: P[f,Segm n,Segm k]};
set FF1={f where f is Function of (Segm n\/{n}),(Segm k\/{l}):
P[f,Segm n\/{n},Segm k\/{l}]& rng (f|Segm n) c= Segm k & f.n=l};
A4: for f be Function of Segm n\/{n},Segm k\/{l} st f.n=l
holds P[f,Segm n\/{n},Segm k\/{l}] iff P[f|Segm n,Segm n,Segm k]
proof
let f9 be Function of Segm n\/{n},Segm k\/{l} such that
A5: f9.n=l;
thus P[f9,Segm n\/{n},Segm k\/{l}] implies P[f9|Segm n,Segm n,Segm k]
proof
n<=n+1 by NAT_1:13;
then
A6: Segm n c= Segm(n+1) by NAT_1:39;
assume
A7: P[f9,Segm n\/{n},Segm k\/{l}];
A8: Segm(n+1)= Segm n\/{n} by AFINSQ_1:2;
k=k\/{l} by A1,Lm1;
then consider f be Function of Segm(n+1),Segm k such that
A9: f=f9 and
A10: f is onto "increasing and
A11: n < n+1 implies f"{f.n}<>{n} by A7,A8;
A12: dom (f|n)=dom f /\ n by RELAT_1:61;
rng(f|n) c= rng f by RELAT_1:70;
then
A13: rng (f|n) c= Segm k by XBOOLE_1:1;
dom f=n+1 by A1,FUNCT_2:def 1;
then dom (f|n)=n by A6,A12,XBOOLE_1:28;
then reconsider fn=f|n as Function of Segm n,Segm k by A13,FUNCT_2:2;
let i,j such that
A14: Segm i= Segm n and
A15: Segm j= Segm k;
reconsider fi=fn as Function of Segm i,Segm j by A14,A15;
fi is onto "increasing by A10,A11,A14,A15,Th38,NAT_1:13;
hence thesis by A9,A14;
end;
thus P[f9|Segm n,Segm n,Segm k] implies P[f9,Segm n\/{n},Segm k\/{l}]
proof
Segm n\/{n}= Segm(n+1) by AFINSQ_1:2;
then reconsider f=f9 as Function of n+1,k by A1,Lm1;
assume P[f9|Segm n,Segm n,Segm k];
then
A16: ex fn be Function of Segm n,Segm k
st fn=f9|n & fn is onto "increasing
&( n < n implies fn"{fn.n}<>{n});
let i,j such that
A17: Segm i= Segm n\/{n} and
A18: Segm j= Segm k\/{l};
reconsider f1=f as Function of Segm i,Segm j by A17,A18;
for f be Function of Segm n,Segm k,
g be Function of Segm(n+1),Segm k st f is onto
"increasing & f=g|Segm n & g.n < k holds g is onto "increasing & g"{g.n}<>{n}
by Th41;
then
A19: n < i implies f1"{f1.n}<>{n} by A1,A5,A16;
A20: Segm(n+1)=i by A17,AFINSQ_1:2;
k =j by A1,A18,Lm1;
then f1 is onto "increasing by A1,A5,A16,A20,Th41;
hence thesis by A19;
end;
end;
A21: Segm k is empty implies Segm n is empty by A2;
A22: card FF2 = card FF1 from Sch4(A21,A3,A4);
A23: F2 c=FF2
proof
let x be object;
assume x in F2;
then
A24: ex f be Function of Segm n,Segm k st x=f & f is onto "increasing;
then P[x,n,k];
hence thesis by A24;
end;
A25: F1 c=FF1
proof
let x be object;
assume x in F1;
then consider f be Function of Segm(n+1),Segm k such that
A26: f=x and
A27: f is onto "increasing and
A28: f"{f.n}<>{n} and
A29: f.n=l;
A30: P[f,Segm n\/{n},Segm k\/{l}]
proof
let i,j such that
A31: Segm i= Segm n\/{n} and
A32: Segm j= Segm k\/{l};
A33: i=Segm(n+1) by A31,AFINSQ_1:2;
j=k by A1,A32,Lm1;
hence thesis by A27,A28,A33;
end;
A34: k=k\/{l} by A1,Lm1;
A35: Segm(n+1)= Segm n\/{n} by AFINSQ_1:2;
rng (f|Segm n) c= rng f by RELAT_1:70;
then
rng (f|Segm n) c= Segm k by XBOOLE_1:1;
hence thesis by A26,A29,A30,A35,A34;
end;
A36: FF2 c= F2
proof
let x be object;
assume x in FF2;
then consider f be Function of n,k such that
A37: x=f and
A38: P[f,n,k];
ex g be Function of Segm n,Segm k
st g=f & g is onto "increasing & (n < n
implies g"{g.n}<>{n}) by A38;
hence thesis by A37;
end;
FF1 c=F1
proof
A39: Segm(n+1)= Segm n\/{n} by AFINSQ_1:2;
let x be object;
assume x in FF1;
then consider f be Function of (n\/{n}),(k\/{l})such that
A40: x=f and
A41: P[f,n\/{n},k\/{l}] and
rng (f|n) c=k and
A42: f.n=l;
k=k\/{l} by A1,Lm1;
then ex f9 be Function of Segm(n+1),Segm k
st f=f9 & f9 is onto "increasing & (n
< n+1 implies f9"{f9.n}<>{n}) by A41,A39;
hence thesis by A40,A42,NAT_1:13;
end;
then F1=FF1 by A25;
hence thesis by A22,A23,A36,XBOOLE_0:def 10;
end;
end;
hence thesis;
end;
theorem Th44:
for f be Function, n holds union (rng (f|n)) \/ f.n=union rng (f |(n+1))
proof
let f be Function,n;
thus union (rng (f|n))\/f.n c=union rng (f|(n+1))
proof
let x be object such that
A1: x in union (rng (f|n))\/f.n;
now
per cases by A1,XBOOLE_0:def 3;
suppose
x in union rng (f|n);
then consider Y be set such that
A2: x in Y and
A3: Y in rng (f|n) by TARSKI:def 4;
consider X be object such that
A4: X in dom (f|n) and
A5: (f|n).X=Y by A3,FUNCT_1:def 3;
A6: (f|n).X=f.X by A4,FUNCT_1:47;
n<=n+1 by NAT_1:11;
then Segm n c= Segm(n+1) by NAT_1:39;
then
A7: dom f /\n c= dom f /\(n+1) by XBOOLE_1:26;
X in dom f /\n by A4,RELAT_1:61;
then X in dom f /\(n+1) by A7;
then
A8: X in dom (f|(n+1)) by RELAT_1:61;
then
A9: (f|(n+1)).X=f.X by FUNCT_1:47;
(f|(n+1)).X in rng (f|(n+1)) by A8,FUNCT_1:def 3;
hence thesis by A2,A5,A9,A6,TARSKI:def 4;
end;
suppose
A10: x in f.n;
nnon empty set,n()->Nat,P[object,object]}:
ex p be XFinSequence of D() st dom p = Segm n() &
for k st k in Segm n() holds P[k,p.k]
provided
A1: for k st k in Segm n() ex x be Element of D() st P[k,x]
proof
A2: for k be object st k in n() ex x be object st x in D() & P[k,x]
proof
let k be object such that
A3: k in n();
n() is Subset of NAT by Th8;
then reconsider k9=k as Element of NAT by A3;
ex x be Element of D() st P[k9,x] by A1,A3;
hence thesis;
end;
consider f be Function of n(),D() such that
A4: for x being object st x in n() holds P[x,f.x] from FUNCT_2:sch 1(A2);
dom f=n() by FUNCT_2:def 1;
then reconsider p=f as XFinSequence of D() by AFINSQ_1:5;
take p;
thus thesis by A4,FUNCT_2:def 1;
end;
Lm2: now let D be non empty set, F be XFinSequence of D;
assume that
A1: for i st i in dom F holds F.i is finite and
A2: for i,j st i in dom F & j in dom F & i<>j holds F.i misses F .j;
thus ex CardF be XFinSequence of NAT st dom CardF = dom F &
(for i st i in dom CardF holds CardF.i=card (F.i)) & card union rng F =
Sum(CardF)
proof
defpred FF[Nat,set] means $2=card (F.$1);
A3: for k st k in Segm len F ex x be Element of NAT st FF[k,x]
proof
let k;
assume k in Segm len F;
then F.k is finite by A1;
then reconsider m = card(F.k) as Nat;
card (F.k)=card m;
hence thesis;
end;
consider CardF be XFinSequence of NAT such that
A4: dom CardF=Segm len F & for k st k in Segm len F holds FF[k,CardF.k] from
Sch6(A3);
take CardF;
thus dom CardF = dom F by A4;
thus
A5: for i st i in dom CardF holds CardF.i=card (F.i) by A4;
A6: addnat "**" CardF = Sum CardF by AFINSQ_2:51;
per cases;
suppose
A7: len CardF=0;then
union rng F is empty by A4,RELAT_1:42,ZFMISC_1:2;
hence thesis by A7,A6,AFINSQ_2:def 8,BINOP_2:5;
end;
suppose
A8: len CardF<>0;
then consider f be sequence of NAT such that
A9: f.0 = CardF.0 and
A10: for n be Nat
st n+1k1;
X in dom F by A25,XBOOLE_0:def 4;
then Y misses F.k1 by A2,A23,A19,A26,A24;
hence contradiction by A20,A18,XBOOLE_0:3;
end;
k1 in dom F by A4,A14,NAT_1:44;
then reconsider Fk1=F.k1 as finite set by A1;
k1 in len F by A4,A14,NAT_1:44;
then card Fk1=CardF.k1 by A4;
then
A27: f.k1=f.k + card Fk1 by A15,BINOP_2:def 23;
card (urFk1 \/ Fk1) = f.k + card Fk1 by A13,A14,A16,CARD_2:40,NAT_1:13;
hence thesis by A27,Th44;
end;
reconsider C1=len CardF-1 as Element of NAT by A8,NAT_1:20;
A28: C1 finite set,x()->set,P[set],f()->Function of card Y(),Y()}:
ex F be XFinSequence of NAT st dom F = card Y() &
card{g where g is Function of X(),Y():P[g]} = Sum(F) &
for i st i in dom F holds F.i = card{g where g is Function
of X(),Y(): P[g] & g.x()=f().i}
provided
A1: f() is onto one-to-one and
A2: Y() is non empty and
A3: x() in X()
proof
defpred FF[Nat,set] means $2={g where g is Function of X(),Y():P[
g]& g.x()=f().$1};
set n = card Y();
A4: for k st k in Segm n ex x be Subset of Funcs(X(),Y()) st FF[k,x]
proof
let k such that
k in Segm n;
set F0={g where g is Function of X(),Y():P[g]& g.x()=f().k};
F0 c= Funcs(X(),Y())
proof
let x be object;
assume x in F0;
then ex g be Function of X(),Y() st x=g & P[g]& g.x()=f().k;
hence thesis by A2,FUNCT_2:8;
end;
hence thesis;
end;
consider F be XFinSequence of bool Funcs(X(),Y()) such that
A5: dom F = Segm n & for k st k in Segm n holds FF[k,F.k] from Sch6(A4);
A6: for i,j st i in dom F & j in dom F & i<>j holds F.i misses F.j
proof
let i,j such that
A7: i in dom F and
A8: j in dom F and
A9: i<>j;
assume F.i meets F.j;
then consider x being object such that
A10: x in F.i/\F.j by XBOOLE_0:4;
x in F.i by A10,XBOOLE_0:def 4;
then
x in {g where g is Function of X(),Y():P[g]& g.x()=f().i} by A5,A7;
then
A11: ex gi be Function of X(),Y() st x=gi &( P[gi])& gi.x()=f ().i;
x in F.j by A10,XBOOLE_0:def 4;
then
x in {g where g is Function of X(),Y():P[g]& g.x()=f().j} by A5,A8;
then
A12: ex gj be Function of X(),Y() st x=gj &( P[gj])& gj.x()=f ().j;
dom f()= card Y() by A2,FUNCT_2:def 1;
hence contradiction by A1,A5,A7,A8,A9,A11,A12;
end;
A13: for i st i in dom F holds F.i is finite
proof
let i;
assume i in dom F;
then
A14: F.i in rng F by FUNCT_1:def 3;
A15: Funcs(X(),Y()) is finite by FRAENKEL:6;
thus thesis by A14,A15;
end;
consider CardF be XFinSequence of NAT such that
A16: dom CardF = dom F and
A17: for i st i in dom CardF holds CardF.i=card (F.i) and
A18: card union rng F = Sum(CardF) by Lm2,A13,A6;
take CardF;
thus dom CardF = card Y() by A5,A16;
thus card{g where g is Function of X(),Y():P[g]} = Sum(CardF)
proof
set G={g where g is Function of X(),Y():P[g]};
A19: G c= union rng F
proof
let x be object;
assume x in G;
then consider g be Function of X(),Y() such that
A20: x=g and
A21: P[g];
A22: rng f()=Y() by A1,FUNCT_2:def 3;
dom g=X() by A2,FUNCT_2:def 1;
then g.x() in rng g by A3,FUNCT_1:def 3;
then consider y being object such that
A23: y in dom f() and
A24: f().y=g.x() by A22,FUNCT_1:def 3;
F.y={g1 where g1 is Function of X(),Y():P[g1] & g1.x()=f().y} by A5,A23;
then
A25: g in F.y by A21,A24;
F.y in rng F by A5,A23,FUNCT_1:def 3;
hence thesis by A20,A25,TARSKI:def 4;
end;
union rng F c=G
proof
let x be object;
assume x in union rng F;
then consider Y be set such that
A26: x in Y and
A27: Y in rng F by TARSKI:def 4;
consider X be object such that
A28: X in dom F and
A29: F.X=Y by A27,FUNCT_1:def 3;
Y={g where g is Function of X(),Y():P[g] & g.x()=f().X} by A5,A28,A29;
then ex gX be Function of X(),Y() st x=gX& P[gX] &gX.x()=f().X by A26;
hence thesis;
end;
hence thesis by A18,A19,XBOOLE_0:def 10;
end;
for i st i in dom CardF holds CardF.i = card{g where g is Function of X
(),Y():P[g] & g.x()=f().i}
proof
let i such that
A30: i in dom CardF;
F.i={g where g is Function of X(),Y():P[g] & g.x()=f().i} by A5,A16,A30;
hence thesis by A17,A30;
end;
hence thesis;
end;
theorem Th45:
k * (n block k)= card{f where f is
Function of Segm(n+1),Segm k: f is onto "increasing & f"{f.n}<>{n}}
proof
now
per cases;
suppose
A1: k=0;
reconsider F1={f where f is Function of Segm(n+1),Segm k:
f is onto "increasing} as set;
reconsider F={f where f is Function of Segm(n+1),Segm k:
f is onto "increasing & f"{f.n}<> {n}} as set;
A2: F c= F1
proof
let x be object;
assume x in F;
then
ex f be Function of Segm(n+1),Segm k
st x=f & f is onto "increasing & f"{f.n}
<>{n};
hence thesis;
end;
card F1= (n+1) block k;
then F1 is empty by A1,Th31;
hence thesis by A1,A2;
end;
suppose k>0;
then
A3: Segm k is non empty;
set G1={g where g is Function of Segm(n+1),Segm k:
g is onto "increasing & g"{g.n}
<>{n}};
defpred P[set] means ex f be Function of Segm(n+1),Segm k
st f=$1& f is onto "increasing&f"{f.n}<>{n};
n{n} & g.n=fi};
A16: F1 c= F
proof
let x be object;
assume x in F1;
then ex g be Function of Segm(n+1),Segm k st x=g & P[g] & g.n=fi;
hence thesis;
end;
F c= F1
proof
let x be object;
assume x in F;
then
ex g be Function of Segm(n+1),Segm k
st x=g &g is onto "increasing & g"{g.
n}<>{n} & g.n=fi;
hence thesis;
end;
then F=F1 by A16;
then card F1=card F2 by A15,Th43;
hence thesis by A11,A13;
end;
then for i be Nat st i in dom F holds F.i <= n block k;
then
A17: Sum F <= len F * (n block k) by AFINSQ_2:59;
set G={g where g is Function of Segm(n+1),Segm k:P[g]};
A18: G1 c= G
proof
let x be object;
assume x in G1;
then
ex g be Function of Segm(n+1),Segm k
st x=g &g is onto "increasing & g"{g.n} <>{n};
hence thesis;
end;
A19: G c= G1
proof
let x be object;
assume x in G;
then ex g be Function of Segm(n+1),Segm k st x=g & P[g];
hence thesis;
end;
for i be Nat st i in dom F holds F.i >= n block k by A12;
then
A20: Sum F >= len F * (n block k) by AFINSQ_2:60;
Sum F= k*(n block k) by A9,A17,A20,XXREAL_0:1;
hence thesis by A10,A18,A19,XBOOLE_0:def 10;
end;
end;
hence thesis;
end;
:: Recursive dependence
theorem Th46:
(n+1) block (k+1) = (k+1)*(n block (k+1) ) + (n block k)
proof
set F={f where f is Function of Segm(n+1),Segm(k+1):f is onto "increasing};
set F1={f where f is Function of Segm(n+1),Segm(k+1):
f is onto "increasing&f"{f.n}={n}};
set F2={f where f is Function of Segm(n+1),Segm(k+1):
f is onto "increasing&f"{f.n}<>{n}};
A1: F c= F1\/F2
proof
let x be object;
assume x in F;
then consider f be Function of Segm(n+1),Segm(k+1) such that
A2: f =x and
A3: f is onto "increasing;
f"{f.n}={n} or f"{f.n}<>{n};
then f in F1 or f in F2 by A3;
hence thesis by A2,XBOOLE_0:def 3;
end;
F1\/F2 c= F
proof
let x be object;
assume x in F1\/F2;
then x in F1 or x in F2 by XBOOLE_0:def 3;
then
(ex f be Function of Segm(n+1),Segm(k+1)
st f = x & f is onto "increasing & f"{f.
n}={n}) or ex f be Function of Segm(n+1),Segm(k+1)
st f = x & f is onto "increasing & f"{f.
n}<>{n};
hence thesis;
end;
then
A4: F1\/F2=F by A1;
A5: F1 misses F2
proof
assume F1 meets F2;
then consider x being object such that
A6: x in F1/\F2 by XBOOLE_0:4;
x in F2 by A6,XBOOLE_0:def 4;
then
A7: ex f be Function of Segm(n+1),Segm(k+1) st
f = x & f is onto "increasing & f"{f.n
} <>{n};
x in F1 by A6,XBOOLE_0:def 4;
then
ex f be Function of Segm(n+1),Segm(k+1)
st f = x & f is onto "increasing & f"{f.n
} ={n};
hence contradiction by A7;
end;
A8: F2 c= Funcs(n+1,k+1)
proof
let x be object;
assume x in F2;
then
ex f be Function of Segm(n+1),Segm(k+1)
st f = x & f is onto "increasing & f"{f.n
}<>{n};
hence thesis by FUNCT_2:8;
end;
A9: F1 c= Funcs(n+1,k+1)
proof
let x be object;
assume x in F1;
then
ex f be Function of Segm(n+1),Segm(k+1)
st f = x & f is onto "increasing & f"{f.n
}={n };
hence thesis by FUNCT_2:8;
end;
Funcs(n+1,k+1) is finite by FRAENKEL:6;
then reconsider F1,F2 as finite set by A9,A8;
reconsider k1=k+1 as Element of NAT;
A10: card F2= k1 * (n block k1) by Th45;
card F1= n block k by Th42;
hence thesis by A4,A5,A10,CARD_2:40;
end;
theorem Th47:
n>=1 implies n block 2 = 1/2 * (2 |^ n - 2 )
proof
defpred P[Nat] means $1 block 2 = 1/2 * (2 |^ $1-2);
A1: for k be Nat st k>=1 & P[k] holds P[k + 1]
proof
let k be Nat such that
A2: k >=1 and
A3: P[k];
(k+1) block 2 = 2*( k block (1+1)) + (k block 1) by Th46
.=2 * (1/2 * (2 |^ k - 2)) + 1 by A2,A3,Th32
.=1/2* (2* 2 |^ k - 2)
.=1/2* (2 |^ (k+1)-2) by NEWTON:6;
hence thesis;
end;
A4: P[1] by Th29;
for k be Nat st k>=1 holds P[k] from NAT_1:sch 8(A4,A1);
hence thesis;
end;
theorem Th48:
n >= 2 implies n block 3 = 1/6 * ( 3 |^ n - 3 * 2 |^ n + 3 )
proof
defpred P[Nat] means $1 block 3=1/6*(3|^$1-3*2|^$1+3);
A1: for k be Nat st k>=2 & P[k] holds P[k+1]
proof
let k be Nat such that
A2: k>=2 and
A3: P[k];
k block 2 = 1/2 * (2 |^ k - 2) by A2,Th47,XXREAL_0:2;
hence (k+1) block 3 = 3*(k block (2+1)) +(1/2*(2|^k-2)) by Th46
.=1/6*((3*3|^k)-3*2*2|^k +3) by A3
.=1/6*(3|^(k+1)-3*(2*2|^k) +3) by NEWTON:6
.=1/6*(3|^(k+1)-3*2|^(k+1) +3) by NEWTON:6;
end;
1/6*(3|^2-3*2|^2+3)=1/6*(3*3-3*2|^2+3) by WSIERP_1:1
.=1/6*(3*3-3*(2*2)+3) by WSIERP_1:1
.=2 block 3 by Th29;
then
A4: P[2];
for k be Nat st k>=2 holds P[k] from NAT_1:sch 8(A4,A1);
hence thesis;
end;
Lm3: n|^3=n*n*n
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
n|^(2+1)=(n|^2)*n by NEWTON:6
.=n*n*n by WSIERP_1:1;
hence thesis;
end;
theorem
n >= 3 implies n block 4 = 1/24 * ( 4 |^ n - 4 * 3 |^ n + 6* 2|^ n - 4 )
proof
defpred P[Nat] means $1 block 4= 1/24 * ( 4 |^ $1 - 4 * 3 |^ $1 + 6* 2|^ $1
- 4 );
A1: for k be Nat st k>=3 & P[k] holds P[k+1]
proof
let k be Nat such that
A2: k>=3 and
A3: P[k];
k block 3 = 1/6 * (3|^k-3*2|^k+3) by A2,Th48,XXREAL_0:2;
hence (k+1) block 4 = 4*(k block (3+1)) +(1/6*(3|^k-3*2|^k+3)) by Th46
.=1/24*((4*4|^k)- 4*(3*3|^k)+ 6*(2*2|^k) - 4) by A3
.=1/24*(4|^(k+1)- 4*(3*3|^k)+ 6*(2*2|^k) - 4) by NEWTON:6
.=1/24*(4|^(k+1)- 4*3|^(k+1)+ 6*(2*2|^k) - 4) by NEWTON:6
.=1/24*(4|^(k+1)- 4*(3|^(k+1))+ 6*2|^(k+1) - 4) by NEWTON:6;
end;
1/24*(4|^3-4*3|^3+6*2|^3-4)= 1/24*(4*4*4-4*3|^3+6*2|^3-4) by Lm3
.=1/24*(64-4*(3*3*3)+6*2|^3-4) by Lm3
.=1/24*(64-4*27+6*(2*2*2)-4) by Lm3
.=3 block 4 by Th29;
then
A4: P[3];
for k be Nat st k>=3 holds P[k] from NAT_1:sch 8(A4,A1);
hence thesis;
end;
theorem Th50:
3! = 6 & 4! = 24
proof
thus
A1: 3! = (2+1)! .= 2*3 by NEWTON:14,15
.= 6;
thus 4! = (3+1)! .= 6*4 by A1,NEWTON:15
.= 24;
end;
theorem Th51:
n choose 1=n & n choose 2=n*(n-1)/2 & n choose 3=n*(n-1)*(n-2)/6
& n choose 4=n*(n-1)*(n-2)*(n-3)/24
proof
now
(n = 0 or ... or n = 3) or 3 < n;
then per cases;
suppose
n=0;
hence thesis by NEWTON:def 3;
end;
suppose
n=1;
hence thesis by NEWTON:21,def 3;
end;
suppose
n=2;
hence thesis by NEWTON:21,23,def 3;
end;
suppose
A1: n=3;
then reconsider n1=n-1,n2=n-2 as Element of NAT by NAT_1:20;
A2: (n2+1)!=(n2)!*(n2+1) by NEWTON:15;
A3: (n2!)/(n2!)=1 by XCMPLX_1:60;
(n1+1)!=(n1)!*n by NEWTON:15;
then n choose 2=((n2)!*((n-1)*n))/((n2!)*(2!)) by A1,A2,NEWTON:def 3
.=((n2!)/(n2!)*((n-1)*n))/2 by NEWTON:14,XCMPLX_1:83
.=((n-1)*n)/2 by A3;
hence thesis by A1,NEWTON:21,23,def 3;
end;
suppose
A4: n>3;
then n>=3+1 by NAT_1:13;
then reconsider n1=n-1,n2=n-2,n3=n-3,n4=n-4 as Element of NAT by NAT_1:21
,XXREAL_0:2;
A5: (n1+1)!=(n1)!*n by NEWTON:15;
A6: (n2+1)!=(n2)!*(n2+1) by NEWTON:15;
A7: (n2!)/(n2!)=1 by XCMPLX_1:60;
n>=2 by A4,XXREAL_0:2;
then
A8: n choose 2=((n2)!*(n1*n))/((n2!)*(2!)) by A5,A6,NEWTON:def 3
.=((n2!)/(n2!)*(n1*n))/2 by NEWTON:14,XCMPLX_1:83
.=n*n1/2 by A7;
A9: (n4!)/(n4!)=1 by XCMPLX_1:60;
A10: (n4+1)!=(n4)!*(n4+1) by NEWTON:15;
A11: (n3!)/(n3!)=1 by XCMPLX_1:60;
A12: (n3+1)!=(n3)!*(n3+1) by NEWTON:15;
then
A13: n choose 3=((n3)!*(n2*n1*n))/((n3!)*(3!)) by A4,A5,A6,NEWTON:def 3
.=((n3!)/(n3!)*(n2*n1*n))/6 by Th50,XCMPLX_1:83
.=n*n1*n2/6 by A11;
n>=3+1 by A4,NAT_1:13;
then
n choose 4=((n4!)*(n3*n2*n1*n))/((n4!)*(4!)) by A5,A6,A12,A10,NEWTON:def 3
.=((n4!)/(n4!)*(n3*n2*n1*n))/24 by Th50,XCMPLX_1:83
.=n*n1*n2*n3/24 by A9;
hence thesis by A4,A8,A13,NEWTON:23,XXREAL_0:2;
end;
end;
hence thesis;
end;
theorem Th52:
(n + 1) block n = (n + 1) choose 2
proof
defpred P[Nat] means ($1+1) block $1 = ($1+1) choose 2;
A1: for k st P[k] holds P[k+1]
proof
let k such that
A2: P[k];
set k1=k+1;
thus (k1+1) block k1=k1*(k1 block k1)+(k1 block k) by Th46
.=k1*1+(k1 choose 2) by A2,Th26
.=k1+k1*(k1-1)/2 by Th51
.=(k1+1)*(k1+1-1)/2
.=(k1+1) choose 2 by Th51;
end;
1 block 0 =0 by Th31;
then
A3: P[0] by NEWTON:def 3;
for k holds P[k] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem
(n + 2) block n = 3*((n + 2) choose 4) + ((n + 2) choose 3)
proof
defpred P[Nat] means ($1+2)block $1=3*(($1+2)choose 4)+(($1+2)
choose 3);
A1: 2 choose 3=0 by NEWTON:def 3;
A2: for k st P[k] holds P[k+1]
proof
let k such that
A3: P[k];
set k1=k+1;
set k2=k+2;
set k3=k2+1;
A4: k1*((k1+1) block k1)=k1*(k2 choose 2) by Th52
.=k1*(k2*(k2-1)/2) by Th51
.=k2*(k2-1)*(k1*12/24);
k2 block k=3*(k2*(k2-1)*(k2-2)*(k2-3)/24)+(k2 choose 3) by A3,Th51
.=3*(k2*(k2-1)*(k2-2)*(k2-3)/24)+(k2*(k2-1)*(k2-2)/6) by Th51
.=k2*(k2-1)*(3*(k2-2)*(k2-3)/24 +4*(k2-2)/24);
then k3 block k1= k2*k1*(k1*12/24)+k2*k1*(3*k*(k2-3)/24+4*k/24) by A4,Th46
.=3*(k3*(k3-1)*(k3-2)*(k3-3)/24)+k3*k2*k1/6
.=3*(k3 choose 4) +(k3*(k3-1)*(k3-2)/6) by Th51
.=3*(k3 choose 4)+(k3 choose 3) by Th51;
hence thesis;
end;
2 choose 4=0 by NEWTON:def 3;
then
A5: P[0] by A1,Th31;
for k holds P[k] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
theorem Th54:
for F be Function,y holds rng (F|(dom F\F"{y}))=rng F\{y} & for
x st x<>y holds (F|(dom F\F"{y}))"{x}=F"{x}
proof
let F be Function,y;
set D=dom F\F"{y};
A1: rng(F|D) c= rng F\{y}
proof
let Fx be object;
assume Fx in rng (F|D);
then consider x being object such that
A2: x in dom (F|D) and
A3: Fx=(F|D).x by FUNCT_1:def 3;
A4: x in dom F /\ D by A2,RELAT_1:61;
then x in (dom F/\dom F)\F"{y} by XBOOLE_1:49;
then not x in F"{y} by XBOOLE_0:def 5;
then not F.x in {y} by A4,FUNCT_1:def 7;
then
A5: not Fx in {y} by A2,A3,FUNCT_1:47;
F.x in rng F by A4,FUNCT_1:def 3;
then Fx in rng F by A2,A3,FUNCT_1:47;
hence thesis by A5,XBOOLE_0:def 5;
end;
rng F\{y} c=rng (F|D)
proof
let Fx be object such that
A6: Fx in rng F\{y};
consider x being object such that
A7: x in dom F and
A8: F.x=Fx by A6,FUNCT_1:def 3;
not Fx in {y} by A6,XBOOLE_0:def 5;
then not x in F"{y} by A8,FUNCT_1:def 7;
then x in D by A7,XBOOLE_0:def 5;
then x in dom F /\D by XBOOLE_0:def 4;
then
A9: x in dom (F|D) by RELAT_1:61;
then (F|D).x in rng (F|D) by FUNCT_1:def 3;
hence thesis by A8,A9,FUNCT_1:47;
end;
hence rng (F|D)=rng F\{y} by A1;
let x such that
A10: x<>y;
now
let z be object such that
A11: z in F"{x};
F.z in {x} by A11,FUNCT_1:def 7;
then F.z <> y by A10,TARSKI:def 1;
then not F.z in {y} by TARSKI:def 1;
then
A12: not z in F"{y} by FUNCT_1:def 7;
z in dom F by A11,FUNCT_1:def 7;
hence z in dom F\F"{y} by A12,XBOOLE_0:def 5;
end;
then F"{x} c= D;
hence thesis by FUNCT_2:98;
end;
theorem Th55:
card X=k+1 & x in X implies card (X\{x})=k
proof
assume that
A1: card X=k+1 and
A2: x in X;
reconsider X9=X as finite set by A1;
set Xx=X9\{x};
{x} c= X by A2,ZFMISC_1:31;
then {x} /\X ={x} by XBOOLE_1:28;
then Xx \/ {x} = X by XBOOLE_1:51;
then
A3: card {x}+ card Xx= k+1 by A1,CARD_2:40,XBOOLE_1:79;
card {x}=1 by CARD_1:30;
hence thesis by A3;
end;
scheme
Sch9{P[set],Q[set,Function]}: for F be Function st rng F is finite holds P[F
]
provided
A1: P[{}] and
A2: for F be Function st for x st x in rng F & Q[x,F] holds P[F|(dom F\F
"{x})] holds P[F]
proof
defpred R[Nat] means for F be Function st card rng F=$1 holds P[F
];
A3: for n st R[n] holds R[n+1]
proof
let n such that
A4: R[n];
let F be Function such that
A5: card rng F=n+1;
for x st x in rng F & Q[x,F] holds P[F|(dom F\F"{x})]
proof
let x such that
A6: x in rng F and
Q[x,F];
set D=dom F\F"{x};
card (rng F\{x})=n by A5,A6,Th55;
then card rng (F|D)=n by Th54;
hence thesis by A4;
end;
hence thesis by A2;
end;
let F be Function;
assume rng F is finite;
then reconsider n = card rng F as Nat;
A7: card rng F=n;
A8: R[0]
proof
let F be Function;
assume card rng F=0;
then rng F={};
hence thesis by A1,RELAT_1:41;
end;
for k holds R[k] from NAT_1:sch 2(A8,A3);
hence thesis by A7;
end;
theorem Th56:
for N be Subset of NAT st N is finite ex k st for n st n in N holds n<=k
proof
let N be Subset of NAT;
assume N is finite;
then reconsider n = card N as Nat;
A1: N,n are_equipotent by CARD_1:def 2;
consider F be Function such that
F is one-to-one and
A2: dom F = n and
A3: rng F = N by A1,WELLORD2:def 4;
reconsider F as XFinSequence by A2,AFINSQ_1:5;
reconsider F as XFinSequence of NAT by A3,RELAT_1:def 19;
reconsider k=Sum F as Element of NAT by ORDINAL1:def 12;
take k;
let n such that
A4: n in N;
F <>0 by A3,A4;
then
A5: len F>0;
ex x being object st x in dom F & F.x=n by A3,A4,FUNCT_1:def 3;
hence thesis by A5,AFINSQ_2:61;
end;
theorem Th57:
for X,Y for x,y being object
st (Y is empty implies X is empty) & not x in X
for
F be Function of X,Y ex G be Function of X\/{x},Y\/{y} st G|X = F & G.x=y
proof
let X,Y;
let x,y be object such that
A1: Y is empty implies X is empty and
A2: not x in X;
set Y1=Y\/{y};
set X1=X\/{x};
deffunc F(set)=y;
let F be Function of X,Y;
y in {y} by TARSKI:def 1;
then
A3: for x9 be set st x9 in X1\X holds F(x9) in Y1 by XBOOLE_0:def 3;
A4: X c= X1 & Y c= Y1 by XBOOLE_1:7;
consider G be Function of X1,Y1 such that
A5: G|X = F & for x9 be set st x9 in X1\X holds G.x9 = F(x9) from Sch2(
A3,A4,A1);
x in {x} by TARSKI:def 1;
then x in X1 by XBOOLE_0:def 3;
then x in X1\X by A2,XBOOLE_0:def 5;
then G.x=y by A5;
hence thesis by A5;
end;
theorem Th58:
for X,Y,x,y st (Y is empty implies X is empty) for F be Function
of X,Y,G be Function of X\/{x},Y\/{y} st G|X=F & G.x=y holds ( F is onto
implies G is onto) & ( not y in Y & F is one-to-one implies G is one-to-one)
proof
let X,Y,x,y such that
A1: Y is empty implies X is empty;
let F be Function of X,Y,G be Function of (X\/{x}),(Y\/{y}) such that
A2: G|X=F and
A3: G.x=y;
thus F is onto implies G is onto
proof
assume
A4: F is onto;
Y\/{y} c= rng G
proof
let Fx be object such that
A5: Fx in Y\/{y};
now
per cases by A5,XBOOLE_0:def 3;
suppose
Fx in Y;
then Fx in rng F by A4,FUNCT_2:def 3;
then consider x9 be object such that
A6: x9 in dom F and
A7: F.x9=Fx by FUNCT_1:def 3;
A8: x9 in X by A6;
A9: dom G=X\/{x} by FUNCT_2:def 1;
A10: X c= X\/{x} by XBOOLE_1:7;
G.x9=F.x9 by A2,A6,FUNCT_1:47;
hence thesis by A7,A8,A10,A9,FUNCT_1:def 3;
end;
suppose
A11: Fx in {y};
A12: dom G =X\/{x} by FUNCT_2:def 1;
A13: {x}c=X\/{x} by XBOOLE_1:7;
A14: x in {x} by TARSKI:def 1;
Fx=y by A11,TARSKI:def 1;
hence thesis by A3,A12,A14,A13,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
then Y\/{y}=rng G;
hence thesis by FUNCT_2:def 3;
end;
thus not y in Y & F is one-to-one implies G is one-to-one
proof
assume that
A15: not y in Y and
A16: F is one-to-one;
let x1,x2 be object such that
A17: x1 in dom G and
A18: x2 in dom G and
A19: G.x1=G.x2;
A20: for x9 be set st x9 in X holds x9 in dom F & F.x9=G.x9 & G.x9<>y
proof
let x9 be set such that
A21: x9 in X;
A22: x9 in dom F by A1,A21,FUNCT_2:def 1;
then
A23: F.x9 in rng F by FUNCT_1:def 3;
F.x9=G.x9 by A2,A22,FUNCT_1:47;
hence thesis by A15,A21,A23,FUNCT_2:def 1;
end;
now
per cases by A17,A18,XBOOLE_0:def 3;
suppose
A24: x1 in X & x2 in X;
then
A25: F.x1=G.x1 by A20;
A26: x2 in dom F by A20,A24;
A27: F.x2=G.x2 by A20,A24;
x1 in dom F by A20,A24;
hence thesis by A16,A19,A26,A25,A27;
end;
suppose
A28: x1 in X & x2 in {x};
then G.x2=y by A3,TARSKI:def 1;
hence thesis by A19,A20,A28;
end;
suppose
A29: x1 in {x} & x2 in X;
then G.x1=y by A3,TARSKI:def 1;
hence thesis by A19,A20,A29;
end;
suppose
A30: x1 in {x} & x2 in {x};
then x=x1 by TARSKI:def 1;
hence thesis by A30,TARSKI:def 1;
end;
end;
hence thesis;
end;
end;
theorem Th59:
for N be finite Subset of NAT
ex Order be Function of N, Segm card N
st Order is bijective & for n,k st n in dom Order & k in dom Order & nm by TARSKI:def 1;
M[i] by A16,XBOOLE_0:def 5;
then
i <= m by A7;
hence i < m by A17,XXREAL_0:1;
A18: i in dom F by A16,FUNCT_2:def 1;
then
A19: F.i=G9.i by A13,FUNCT_1:47;
A20: F.i in card Nm by A18,FUNCT_2:5;
card Nm=k by A3,A7,Th55;
hence G9.i 0 by A1;
then reconsider c1=card X-1 as Element of NAT by NAT_1:20;
c1x2;
reconsider Xx=X\{x1} as finite set;
Y c= F.:Xx
proof
let Fy be object;
assume Fy in Y;
then Fy in rng F by A2,FUNCT_2:def 3;
then consider y being object such that
A7: y in dom F and
A8: F.y=Fy by FUNCT_1:def 3;
now
per cases;
suppose
A9: y=x1;
x2 in Xx by A4,A6,ZFMISC_1:56;
hence thesis by A4,A5,A8,A9,FUNCT_1:def 6;
end;
suppose
y<>x1;
then y in Xx by A7,ZFMISC_1:56;
hence thesis by A7,A8,FUNCT_1:def 6;
end;
end;
hence thesis;
end;
then
A10: Segm card Y c= Segm card Xx by CARD_1:66;
card Xx < card X by A3,Lm4;
then Segm card Xx c< Segm card X by NAT_1:39;
then Segm card X c< Segm card Y by A1,A10,XBOOLE_1:58;
hence thesis by A1;
end;
thus F is one-to-one implies F is onto
proof
assume F is one-to-one;
then dom F,F.:dom F are_equipotent by CARD_1:33;
then
A11: card dom F=card (F.:dom F) by CARD_1:5;
assume F is not onto;
then not rng F = Y by FUNCT_2:def 3;
then not Y c= rng F;
then consider y being object such that
A12: y in Y and
A13: not y in rng F;
A14: card rng F <=card (Y\{y}) by A13,NAT_1:43,ZFMISC_1:34;
A15: F.:dom F= rng F by RELAT_1:113;
card (Y\{y})< card Y by A12,Lm4;
hence thesis by A1,A12,A14,A11,A15,FUNCT_2:def 1;
end;
end;
Lm5: for n be Element of NAT,N be finite Subset of NAT, F be Function of N,
Segm card N
st n in N & F is bijective & for n,k st n in dom F & k in dom F & n n implies P.k=k)
proof
let n be Element of NAT,N be finite Subset of NAT,
F be Function of N,Segm card N
such that
A1: n in N and
A2: F is bijective and
A3: for n,k st n in dom F & k in dom F & n n implies $2=k);
A4: dom F=N by A1,FUNCT_2:def 1;
A5: dom F9=card N by A1,FUNCT_2:def 1;
A6: for x being object st x in N ex y being object st y in N & P[x,y]
proof
let x9 be object such that
A7: x9 in N;
reconsider x=x9 as Element of NAT by A7;
now
per cases by XXREAL_0:1;
suppose
A8: x < n;
then F.x < F.n by A1,A3,A4,A7;
then
A9: (F.x)+1 <=F.n by NAT_1:13;
n in dom F by A1,A4;
then F.n in card N by FUNCT_2:5;
then F.n < card N by NAT_1:44;
then (F.x)+1 < card N by A9,XXREAL_0:2;
then (F.x)+1 in dom F9 by A5,NAT_1:44;
then
A10: F9.((F.x)+1) in rng F9 by FUNCT_1:def 3;
set FF=F".((F.x)+1);
P[x9,FF] by A8;
hence thesis by A10;
end;
suppose
A11: x = n;
0 in dom F9 by A1,A5,NAT_1:44;
then
A12: F9.0 in rng F9 by FUNCT_1:def 3;
P[x9,F".0] by A11;
hence thesis by A12;
end;
suppose
x>n;
then P[x,x];
hence thesis by A7;
end;
end;
hence thesis;
end;
consider P be Function of N,N such that
A13: for x being object st x in N holds P[x,P.x] from FUNCT_2:sch 1(A6);
N c= rng P
proof
let Px9 be object such that
A14: Px9 in N;
reconsider Px=Px9 as Element of NAT by A14;
now
per cases;
suppose
A15: Px<=n;
rng (F9)=N by A2,A4,FUNCT_1:33;
then consider x being object such that
A16: x in dom F9 and
A17: F9.x=Px by A14,FUNCT_1:def 3;
reconsider x as Element of NAT by A5,A16;
now
per cases;
suppose
A18: x=0;
A19: dom P=N by A1,FUNCT_2:def 1;
P.n=F".0 by A1,A13;
hence thesis by A1,A17,A18,A19,FUNCT_1:def 3;
end;
suppose
x>0;
then reconsider x1=x-1 as Element of NAT by NAT_1:20;
A20: x1=n;
then y>n or y=n by XXREAL_0:1;
then
A26: x1>=F.n by A1,A3,A4,A22,A23;
x in rng F by A2,A16,FUNCT_1:33;
then
A27: F.Px=x by A2,A17,FUNCT_1:32;
Px x1 by NAT_1:13;
hence contradiction by A26,A27,A28,XXREAL_0:2;
end;
F".(F.y+1)=Px by A17,A23;
then P.y=Px by A13,A22,A25;
hence thesis by A24,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
suppose
A29: Px>n;
A30: Px in dom P by A14,FUNCT_2:def 1;
Px=P.Px by A13,A14,A29;
hence thesis by A30,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
then N=rng P;
then
A31: P is onto by FUNCT_2:def 3;
card N=card N;
then P is onto one-to-one by A31,Th60;
then reconsider P as Permutation of N;
take P;
thus thesis by A13;
end;
theorem Th61:
for F,G be Function,y st y in rng (G*F) & G is one-to-one holds
ex x st x in dom G & x in rng F & G"{y}={x} & F"{x}=(G*F)"{y}
proof
let F,G be Function,y such that
A1: y in rng (G*F) and
A2: G is one-to-one;
consider x being object such that
A3: x in dom (G*F) and
A4: (G*F).x=y by A1,FUNCT_1:def 3;
A5: F.x in dom G by A3,FUNCT_1:11;
A6: G.(F.x)=y by A3,A4,FUNCT_1:12;
then G.(F.x) in {y} by TARSKI:def 1;
then
A7: F.x in G"{y} by A5,FUNCT_1:def 7;
A8: F"{F.x} c= (G*F)"{y}
proof
let d be object such that
A9: d in F"{F.x};
A10: d in dom F by A9,FUNCT_1:def 7;
F.d in {F.x} by A9,FUNCT_1:def 7;
then
A11: F.d = F.x by TARSKI:def 1;
then G.(F.d) in {y} by A6,TARSKI:def 1;
then
A12: (G*F).d in {y} by A10,FUNCT_1:13;
d in dom (G*F) by A5,A10,A11,FUNCT_1:11;
hence thesis by A12,FUNCT_1:def 7;
end;
y in rng G by A1,FUNCT_1:14;
then consider Fx be object such that
A13: G"{y}={Fx} by A2,FUNCT_1:74;
x in dom F by A3,FUNCT_1:11;
then
A14: F.x in rng F by FUNCT_1:def 3;
A15: F.x in dom G by A3,FUNCT_1:11;
(G*F)"{y} c= F"{F.x}
proof
let d be object such that
A16: d in (G*F)"{y};
A17: d in dom (G*F) by A16,FUNCT_1:def 7;
then
A18: d in dom F by FUNCT_1:11;
(G*F).d in {y} by A16,FUNCT_1:def 7;
then
A19: G.(F.d) in {y} by A17,FUNCT_1:12;
A20: F.d in dom G by A17,FUNCT_1:11;
F.x=Fx by A13,A7,TARSKI:def 1;
then F.d in {F.x} by A13,A20,A19,FUNCT_1:def 7;
hence thesis by A18,FUNCT_1:def 7;
end;
then
A21: F"{F.x} = (G*F)"{y} by A8;
G"{y}={F.x} by A13,A7,TARSKI:def 1;
hence thesis by A15,A14,A21;
end;
definition
let Ne,Ke;
let f be Function of Ne,Ke;
attr f is 'increasing means
for l,m st l in rng f & m in rng f & l < m holds min* f"{l} < min* f"{m};
end;
theorem Th62:
for F be Function of Ne,Ke st F is 'increasing holds min* rng F= F.min* dom F
proof
let F be Function of Ne,Ke such that
A1: F is 'increasing;
now
per cases;
suppose
A2: rng F is empty;
then
A3: min* rng F=0 by NAT_1:def 1;
dom F={} by A2,RELAT_1:42;
hence thesis by A3,FUNCT_1:def 2;
end;
suppose
A4: rng F is non empty;
then reconsider rngF=rng F,Ke as non empty Subset of NAT by XBOOLE_1:1;
reconsider domF=dom F as non empty Subset of NAT by A4,FUNCT_2:def 1
,RELAT_1:42;
set md=min* domF;
set mr=min* rngF;
mr=F.md
proof
A5: md in dom F by NAT_1:def 1;
then F.md in rngF by FUNCT_1:def 3;
then
A6: mr <=F.md by NAT_1:def 1;
assume mr<>F.md;
then
A7: mr < F.md by A6,XXREAL_0:1;
A8: md in domF by NAT_1:def 1;
A9: md in dom F by NAT_1:def 1;
mr in rngF by NAT_1:def 1;
then consider x being object such that
A10: x in dom F and
A11: F.x=mr by FUNCT_1:def 3;
A12: F.md in {F.md} by TARSKI:def 1;
F.x in {mr} by A11,TARSKI:def 1;
then reconsider
Fmr=F"{mr},Fmd=F"{F.md} as non empty Subset of NAT by A10,A12,A9,
FUNCT_1:def 7,XBOOLE_1:1;
A13: mr in rngF by NAT_1:def 1;
min* Fmr in Fmr by NAT_1:def 1;
then min* Fmr in domF by FUNCT_1:def 7;
then
A14: min* Fmr >= md by NAT_1:def 1;
F.md in {F.md} by TARSKI:def 1;
then md in Fmd by A8,FUNCT_1:def 7;
then
A15: md >= min* Fmd by NAT_1:def 1;
F.md in rng F by A5,FUNCT_1:def 3;
then min* F"{mr}< min* F"{F.md} by A1,A7,A13;
hence contradiction by A14,A15,XXREAL_0:2;
end;
hence thesis;
end;
end;
hence thesis;
end;
:: existence of an expansion
theorem
for F be Function of Ne,Ke st rng F is finite ex I be Function of Ne,
Ke,P be Permutation of rng F st F=P*I & rng F=rng I & I is 'increasing
proof
defpred Q[set,Function] means $1=$2.min* dom $2;
defpred P[set] means for Ne,Ke be Subset of NAT,F be Function of Ne,Ke st F=
$1 & rng F is finite ex P be Permutation of rng F,G be Function of Ne,Ke st F=P
*G & rng F = rng G & for i,j st i in rng G & j in rng G & i F.m implies P1.k=k) by A9,A42
,A43,Lm5;
dom G2=N by FUNCT_2:def 1;
then
A45: G2 is Function of N,rF by A38,FUNCT_2:1;
reconsider P21=P2*P1" as Function of rF,rF;
reconsider P21 as Permutation of rF;
dom P1=rF by FUNCT_2:def 1;
then
A46: P1"*P1=id rF by FUNCT_1:39;
rng (P1*G2) c= K by XBOOLE_1:1;
then reconsider PG=P1*G2 as Function of N,K by A45,FUNCT_2:6;
dom G2=N by FUNCT_2:def 1;
then G2 is Function of N,rF by A38,FUNCT_2:1;
then (id rF)*G2 = G2 by FUNCT_2:17;
then
A47: P1"*(P1*G2)=G2 by A46,RELAT_1:36;
G2"{F.m}c=F"{F.m}
proof
let x be object such that
A48: x in G2"{F.m};
A49: x in N\dFD
proof
assume not x in N\dFD;
then x in dom G2 & dom G2=N & not x in N or x in dFD by A48,
XBOOLE_0:def 5;
then
A50: x in dom G by FUNCT_2:def 1;
then
A51: G.x in rng G by FUNCT_1:def 3;
A52: rng FD=rng F\{F.m} by Th54;
G.x=G2.x by A22,A50,FUNCT_1:47;
then not G2.x in {F.m} by A51,A52,XBOOLE_0:def 5;
hence thesis by A48,FUNCT_1:def 7;
end;
then
A53: not x in dom F\F"{F.m} by A27,XBOOLE_0:def 5;
dom F=N by A9,FUNCT_2:def 1;
then x in dom F by A49,XBOOLE_0:def 5;
hence thesis by A53,XBOOLE_0:def 5;
end;
then
A54: G2"{F.m}=F"{F.m} by A28;
A55: for n st n in rng FD holds G"{n}=G2"{n}
proof
K is non empty;
then dom F=N by FUNCT_2:def 1;
then
A56: dFD= dom G2\G2"{F.m} by A27,A54,FUNCT_2:def 1;
A57: rng FD=rng F\{F.m} by Th54;
let n;
assume n in rng FD;
then not n in {F.m} by A57,XBOOLE_0:def 5;
then n<>F.m by TARSKI:def 1;
hence thesis by A22,A56,Th54;
end;
A58: for i,j st i in rng PG & j in rng PG & i=k;
then n>k by A70,XXREAL_0:1;
hence contradiction by A43,A68,A69,A70;
end;
A71: for n,k st n in rng Orde & k in rng Orde holds n < k
implies Orde9.n=j1;
then i1>j1 by A83,A93,A96,XXREAL_0:1;
then Orde.i1 >Orde.j1 by A43,A92,A94,A97;
then
A102: Orde.i1+1 >Orde.j1+1 by XREAL_1:8;
A103: Orde.i1+1 in rng Orde by A84,A59,A98;
A104: Orde9.(Orde.j1+1)= j by A44,A94,A96,A98;
A105: Orde.j1+1 in rng Orde by A88,A59,A98;
Orde9.(Orde.i1+1)=i by A44,A92,A93,A98;
hence contradiction by A83,A71,A102,A103,A105,A104;
end;
then min* G"{i1}F.m;
consider x being object such that
A107: x in dom G2 and
A108: G2.x=j1 by A89,FUNCT_1:def 3;
G2.x in {j1} by A108,TARSKI:def 1;
then PG"{j} is non empty Subset of NAT by A91,A107,
FUNCT_1:def 7,XBOOLE_1:1;
then
A109: min* PG"{j} in PG"{j} by NAT_1:def 1;
j1 in rng FD or j1 in {F.m} by A89,A80,XBOOLE_0:def 3;
then
A110: G"{j1} =PG"{j} by A55,A91,A106,TARSKI:def 1;
then min* PG"{j} in dom F by A27,A109,XBOOLE_0:def 5;
then
A111: m<=min* PG"{j} by NAT_1:def 1;
A112: m in domF by NAT_1:def 1;
F.m in {F.m} by TARSKI:def 1;
then
A113: m in F"{F.m} by A112,FUNCT_1:def 7;
then m<>min* PG"{j} by A27,A110,A109,XBOOLE_0:def 5;
then
A114: mOrde9.0 by A71,A116;
A118: P1.j1=Orde9.0 by A44,A94,A115;
Orde9.(Orde.i1+1)=i by A44,A92,A93,A115;
hence thesis by A83,A95,A117,A118,TARSKI:def 1;
end;
suppose
i1 = F.m & j1=F.m;
hence thesis by A83,A95,A93,TARSKI:def 1;
end;
suppose
A119: i1 > F.m & j1>F.m;
A120: i1 in rng FD or i1 in {F.m} by A85,A80,XBOOLE_0:def 3;
then
A121: G"{i1}=PG"{i} by A55,A87,A119,TARSKI:def 1;
A122: P1.j1=j1 by A44,A88,A119;
A123: j1 in rng FD or j1 in {F.m} by A89,A80,XBOOLE_0:def 3;
P1.i1=i1 by A44,A84,A119;
then min* G"{i1}< min* G"{j1} by A19,A20,A83,A93,A96,A119
,A122,A120,A123,TARSKI:def 1;
hence thesis by A55,A91,A119,A123,A121,TARSKI:def 1;
end;
suppose
A124: i1 > F.m & j1=F.m;
A125: dom Orde=rF by FUNCT_2:def 1;
rng (Orde")=dom Orde by A42,FUNCT_1:33;
then consider x being object such that
A126: x in dom Orde9 and
A127: Orde9.x=i1 by A84,A125,FUNCT_1:def 3;
A128: x in card rF by A126;
card rF is Subset of NAT by Th8;
then reconsider x as Element of NAT by A128;
P1.i1=i1 by A44,A84,A124;
then
A129: Orde9.x < Orde9.0 by A44,A83,A88,A93,A96,A124,A127;
A130: card rF=rng Orde by A42,FUNCT_2:def 3;
then 0 in rng Orde by NAT_1:44;
then x <=0 by A71,A126,A130,A129;
hence thesis by A129;
end;
suppose
A131: i1 < F.m & j1>F.m;
A132: i1 in rng FD or i1 in {F.m} by A85,A80,XBOOLE_0:def 3;
then
A133: G"{i1}=PG"{i} by A55,A87,A131,TARSKI:def 1;
A134: j1 in rng FD or j1 in {F.m} by A89,A80,XBOOLE_0:def 3;
i1 F.m & j1{};
let Ne,Ke,Me be Subset of NAT;
let F be Function of Ne,Ke such that
A11: F=F9;
Ke is non empty by A10,A11;
then reconsider domF=dom F as non empty Subset of NAT by A10,A11,
FUNCT_2:def 1;
set m=min* dom F;
let I1,I2 be Function of Ne,Me, P1,P2 be Function such that
A12: P1 is one-to-one and
A13: P2 is one-to-one and
A14: rng I1=rng I2 and
A15: rng I1=dom P1 and
A16: dom P1=dom P2 and
A17: F=P1*I1 and
A18: F=P2*I2 and
A19: I1 is 'increasing and
A20: I2 is 'increasing;
dom I1=dom F by A15,A17,RELAT_1:27;
then
A21: min* rng I1=I1.m by A19,Th62;
reconsider I=rng I1\{I1.m} as Subset of NAT by XBOOLE_1:1;
reconsider D=dom F\F"{F.m} as Subset of NAT by XBOOLE_1:1;
A22: for I be Function of Ne,Me,P be Function st P is one-to-one & rng
I=dom P & F=P*I & I is 'increasing holds dom (I|D)=D & rng (I|D)=rng I\{I.m} &
dom (P|(rng I\{I.m}))=rng I\{I.m} & F|D=(P|(rng I\{I.m}))*(I|D) & P|(rng I\{I.m
}) is one-to-one & for M be Subset of NAT st M=rng I\{I.m} for I1 be Function
of D,M st I1=I|D holds I1 is 'increasing
proof
A23: F.m in {F.m} by TARSKI:def 1;
let I be Function of Ne,Me,P be Function such that
A24: P is one-to-one and
A25: rng I=dom P and
A26: F=P*I and
A27: I is 'increasing;
A28: dom P/\(rng I\{I.m})=rng I\{I.m} by A25,XBOOLE_1:28,36;
m in domF by NAT_1:def 1;
then F.m in rng F by FUNCT_1:def 3;
then consider x such that
x in dom P and
x in rng I and
P"{F.m}={x} and
A29: I"{x}=F"{F.m} by A24,A26,Th61;
A30: dom (P|(rng I\{I.m}))=dom P/\(rng I\{I.m}) by RELAT_1:61;
A31: dom F=dom I by A25,A26,RELAT_1:27;
then
A32: dom I/\D=D by XBOOLE_1:28,36;
m in domF by NAT_1:def 1;
then m in I"{x} by A29,A23,FUNCT_1:def 7;
then I.m in {x} by FUNCT_1:def 7;
then
A33: I.m=x by TARSKI:def 1;
A34: for M be Subset of NAT st M=rng I\{I.m} for I1 be Function of D
,M st I1=I|D holds I1 is 'increasing
proof
let M be Subset of NAT such that
M=rng I\{I.m};
let I1 be Function of D,M such that
A35: I1=I|D;
A36: rng I1=rng I\{I.m} by A29,A33,A31,A35,Th54;
let l,n such that
A37: l in rng I1 and
A38: n in rng I1 and
A39: l < n;
A40: n in rng I by A38,A36,ZFMISC_1:56;
n<>I.m by A38,A36,ZFMISC_1:56;
then
A41: I1"{n}=I"{n} by A29,A33,A31,A35,Th54;
l<>I.m by A37,A36,ZFMISC_1:56;
then
A42: I1"{l}=I"{l} by A29,A33,A31,A35,Th54;
l in rng I by A37,A36,ZFMISC_1:56;
hence thesis by A27,A39,A40,A42,A41;
end;
set rI=rng I\{I.m};
A43: dom (I|D)=dom I/\D by RELAT_1:61;
A44: rng (I|D)=rng I\{I.m} by A29,A33,A31,Th54;
A45: for x being object st x in dom (F|D)
holds (F|D).x = (P|rI).((I|D).x)
proof
let x being object such that
A46: x in dom (F|D);
A47: x in dom F/\D by A46,RELAT_1:61;
then
A48: x in dom F by XBOOLE_0:def 4;
(I|D).x in dom (P|rI) by A31,A43,A30,A28,A44,A47,FUNCT_1:def 3;
then
A49: (P|rI).((I|D).x)=P.((I|D).x) by FUNCT_1:47;
A50: (F|D).x=F.x by A46,FUNCT_1:47;
I.x=(I|D).x by A31,A43,A47,FUNCT_1:47;
hence thesis by A26,A48,A49,A50,FUNCT_1:12;
end;
dom F/\D=D by XBOOLE_1:28,36;
then dom (F|D)=D by RELAT_1:61;
then for x being object
holds x in dom (F|D) iff x in dom (I|D) & (I|D).x in dom
(P|rI) by A43,A32,A30,A28,A44,FUNCT_1:def 3;
hence thesis by A24,A29,A33,A31,A32,A28,A45,A34,Th54,FUNCT_1:10,52
,RELAT_1:61;
end;
then
A51: P1|I is one-to-one by A12,A15,A17,A19;
dom I2=dom F by A14,A15,A16,A18,RELAT_1:27;
then
A52: min* rng I2=I2.m by A20,Th62;
then
A53: P2|I is one-to-one by A13,A14,A15,A16,A18,A20,A22,A21;
A54: dom (I2|D)=D by A13,A14,A15,A16,A18,A20,A22;
A55: dom (I1|D)=D by A12,A15,A17,A19,A22;
A56: rng (I1|D)=I by A12,A15,A17,A19,A22;
rng (I2|D)=I by A13,A14,A15,A16,A18,A20,A22,A21,A52;
then reconsider I1D=I1|D,I2D=I2|D as Function of D,I by A55,A54,A56,
FUNCT_2:1;
A57: I2D is 'increasing by A13,A14,A15,A16,A18,A20,A22,A21,A52;
A58: rng I1D=I by A12,A15,A17,A19,A22;
then
A59: rng I1D=dom (P1|I) by A12,A15,A17,A19,A22;
reconsider rFD=rng (F|D) as Subset of NAT by XBOOLE_1:1;
dom F/\D=D by XBOOLE_1:28,36;
then dom (F|D)=D by RELAT_1:61;
then reconsider FD=F|D as Function of D,rFD by FUNCT_2:1;
A60: FD=(P1|I)*I1D by A12,A15,A17,A19,A22;
A61: FD=(P2|I)*I2D by A13,A14,A15,A16,A18,A20,A22,A21,A52;
m in domF by NAT_1:def 1;
then
A62: F.m in rng F by FUNCT_1:def 3;
dom (P1|I)=I by A12,A15,A17,A19,A22;
then
A63: dom (P1|I)=dom (P2|I) by A13,A14,A15,A16,A18,A20,A22,A21,A52;
A64: I1D is 'increasing by A12,A15,A17,A19,A22;
A65: rng I1D=rng I2D by A13,A14,A15,A16,A18,A20,A22,A21,A52,A58;
for x being object st x in dom P1 holds P1.x = P2.x
proof
A66: m in domF by NAT_1:def 1;
dom I1=dom F by A15,A17,RELAT_1:27;
then I1.m in rng I1 by A66,FUNCT_1:def 3;
then
A67: dom P1=I\/{I1.m} by A15,ZFMISC_1:116;
let x being object such that
A68: x in dom P1;
now
per cases by A68,A67,XBOOLE_0:def 3;
suppose
A69: x in I;
dom P1/\I=I by A15,XBOOLE_1:28,36;
then x in dom (P1|I) by A69,RELAT_1:61;
then
A70: (P1|I).x=P1.x by FUNCT_1:47;
dom P2/\I=I by A15,A16,XBOOLE_1:28,36;
then x in dom (P2|I) by A69,RELAT_1:61;
then (P2|I).x=P2.x by FUNCT_1:47;
hence
thesis by A9,A11,A62,A51,A53,A65,A59,A63,A60,A61,A64,A57,A70;
end;
suppose
A71: x in {I1.m};
A72: m in domF by NAT_1:def 1;
A73: x=I1.m by A71,TARSKI:def 1;
then F.m=P1.x by A17,A72,FUNCT_1:12;
hence thesis by A14,A18,A21,A52,A73,A72,FUNCT_1:12;
end;
end;
hence thesis;
end;
then
A74: P1=P2 by A16;
I2 is Function of dom I2,rng I2 by FUNCT_2:1;
then
A75: I2=(id rng I2)*I2 by FUNCT_2:17;
I1 is Function of dom I1,rng I1 by FUNCT_2:1;
then
A76: I1=(id rng I1)*I1 by FUNCT_2:17;
P1"*P1 = id dom P1 by A12,FUNCT_1:39;
then
A77: I1=P1"*(P1*I1) by A15,A76,RELAT_1:36;
P2"*P2 = id dom P2 by A13,FUNCT_1:39;
hence P1=P2 & I1=I2 by A14,A15,A17,A18,A74,A75,A77,RELAT_1:36;
end;
end;
hence thesis;
end;
for F be Function st rng F is finite holds P[F] from Sch9(A1,A8 );
hence thesis;
end;
theorem
for F be Function of Ne,Ke st rng F is finite for I1,I2 be Function of
Ne,Ke, P1,P2 be Permutation of rng F st F=P1*I1 & F=P2*I2 & rng F=rng I1 & rng
F=rng I2 & I1 is 'increasing & I2 is 'increasing holds P1=P2 & I1=I2
proof
let F be Function of Ne,Ke such that
A1: rng F is finite;
let I1,I2 be Function of Ne,Ke, P1,P2 be Permutation of rng F such that
A2: F=P1*I1 and
A3: F=P2*I2 and
A4: rng F=rng I1 and
A5: rng F=rng I2 and
A6: I1 is 'increasing and
A7: I2 is 'increasing;
A8: rng F ={} implies rng F={};
then
A9: dom P2=rng F by FUNCT_2:def 1;
dom P1=rng F by A8,FUNCT_2:def 1;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A9,Th64;
end;
::$N Stirling numbers of the second kind
theorem
for D be non empty set, F be XFinSequence of D st
(for i st i in dom F holds F.i is finite) &
(for i,j st i in dom F & j in dom F & i<>j holds F.i misses F.j)
ex CardF be XFinSequence of NAT st dom CardF = dom F &
(for i st i in dom CardF holds CardF.i=card (F.i)) &
card union rng F = Sum(CardF) by Lm2;