:: Stirling Numbers of the Second Kind
:: by Karol P\c{a}k
::
:: Received March 15, 2005
:: Copyright (c) 2005-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, 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;
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, FINSEQ_4;
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<n};
then ex l be Nat st x=l & l<n;
hence x in NAT by ORDINAL1:def 12;
end;
then {l where l is Nat:l<n} c= NAT;
hence thesis by AXIOMS:4;
end;
registration
let n;
cluster -> 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} by AXIOMS:4;
then ex l be Nat st min* N = l & l<n;
hence thesis by NAT_1:20;
end;
theorem Th10:
k in Segm n implies k<=n-1 & n-1 is Element of NAT
proof
assume k in Segm n;
then k in {l where l is Nat:l<n} by AXIOMS:4;
then
A1: ex l be Nat st k=l & l<n;
then
A2: n-1 is Element of NAT by NAT_1:20;
k<(n-1)+1 by A1;
hence thesis by A2,NAT_1:13;
end;
theorem
min* n = 0
proof
now
per cases;
suppose
0=n;
hence thesis by NAT_1:def 1;
end;
suppose
0<n;
then 0 in {l where l is Nat:l<n};
then
A1: 0 in n by AXIOMS:4;
n is Subset of NAT by Th8;
hence thesis by A1,NAT_1:def 1;
end;
end;
hence thesis;
end;
theorem Th12:
N c= Segm n implies min* N <= n-1
proof
A1: min* N in N by NAT_1:def 1;
assume N c= Segm n;
hence thesis by A1,Th10;
end;
theorem
N c= Segm n & N <> {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; :: redefines " (FUNCT_1, redefinition) → " (RELAT_1, definition)
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; :: redefines . (FUNCT_1, definition)
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 $1<k implies $1<=min* f"{$1};
assume that
A1: f is onto "increasing;
A2: for m st M[m] holds M[m + 1]
proof
A3: k=rng f by A1,FUNCT_2:def 3;
let m such that
A4: M[m];
assume
A5: m+1<k;
m<m+1 by NAT_1:19;
then m < k by A5,XXREAL_0:2;
then
A6: m in rng f by A3,NAT_1:44;
A7: m < m+1 by NAT_1:19;
m+1 in rng f by A5,A3,NAT_1:44;
then min* f"{m}< min* f"{m+1} by A1,A6,A7;
then m < min* f"{m+1} by A4,A5,A7,XXREAL_0:2;
hence thesis by NAT_1:13;
end;
A8: M[0];
for m holds M[m] from NAT_1:sch 2(A8,A2);
hence thesis;
end;
theorem Th19:
f is onto "increasing implies for m st m < k holds min* f"{m} <= n-k+m
proof
assume that
A1: f is onto "increasing;
now
per cases;
suppose
k=0;
hence thesis;
end;
suppose
k>0;
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: k1<k1+1 by NAT_1:13;
A3: for m be Integer st m <= k1 holds I[m] implies I[m-1]
proof
reconsider nk=n-k as Element of NAT by A1,Th17,NAT_1:21;
A4: k = rng f by A1,FUNCT_2:def 3;
let m be Integer;
assume m <= k1;
then
A5: m < k by A2,XXREAL_0:2;
assume
A6: I[m];
assume 0<=m-1;
then reconsider m1=m-1 as Element of NAT by INT_1:3;
A7: m1<m1+1 by NAT_1:19;
then m1<k by A5,XXREAL_0:2;
then
A8: m1 in Segm k by NAT_1:44;
m1+1 in Segm k by A5,NAT_1:44;
then min* f"{m1}<min* f"{m1+1} by A1,A7,A8,A4;
then min* f"{m1} < (nk+m1)+1 by A6,XXREAL_0:2;
hence thesis by NAT_1:13;
end;
A9: I[k1]
proof
assume 0<= k1;
k=0 iff n=0 by A1;
then min* f"{k1}<=n-1 by Th16;
hence thesis;
end;
A10: for m be Integer st m <= k1 holds I[m] from INT_1:sch 3(A9,A3);
now
let m;
assume m < k;
then m<k1+1;
then m<=k1 by NAT_1:13;
hence min* f"{m} <= n-k+m by A10;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th20:
f is onto "increasing & n = k implies f = id n
proof
assume that
A1: f is onto "increasing and
A2: n=k;
now
per cases;
suppose
A3: n=0;
thus thesis by A3;
end;
suppose
A4: n>0;
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: l<m;
A8: ex x be object st f"{l} = {x} by A1,A5,FUNCT_1:74;
A9: l in {l} by TARSKI:def 1;
consider l9 be object such that
A10: l9 in dom f and
A11: f.l9=l by A5,FUNCT_1:def 3;
l = l9 by A1,A10,A11,FUNCT_1:18;
then l in f"{l} by A10,A11,A9,FUNCT_1:def 7;
then f"{l}={l} & l in NAT by A8,TARSKI:def 1;
then
A12: min* f"{l} = l by Th5;
A13: m in {m} by TARSKI:def 1;
A14: ex x be object st f"{m} = {x} by A1,A6,FUNCT_1:74;
consider m9 be object such that
A15: m9 in dom f and
A16: f.m9=m by A6,FUNCT_1:def 3;
m = m9 by A1,A15,A16,FUNCT_1:18;
then m in f"{m} by A15,A16,A13,FUNCT_1:def 7;
then f"{m}={m} & m in NAT by A14,TARSKI:def 1;
hence min* f"{l} < min* f"{m} by A7,A12,Th5;
end;
rng f=n by A1;
hence thesis by A3,A4;
end;
theorem
(n=0 iff k=0) implies
ex f be Function of Segm n, Segm k st f is "increasing
proof
assume
A1: n=0 iff k=0;
now
per cases;
suppose
A2: n=0;
set f={};
A3: dom f = n by A2;
rng f= k by A1,A2;
then reconsider f as Function of Segm n,Segm k by A3,FUNCT_2:1;
f is "increasing by A1;
hence thesis;
end;
suppose
n>0;
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<k1+1 by NAT_1:13;
min(x,k1)<=k1 by XXREAL_0:17;
then min(x,k1)<k by A7,XXREAL_0:2;
then min(x,k1) in Segm k by NAT_1:44;
hence thesis;
end;
consider f be Function of Segm n,Segm k such that
A8: for m be Element of Segm n holds
F[m,f.m qua Element of Segm k] from FUNCT_2:sch 3(A6);
now
let m9 be object such that
A9: m9 in Segm k;
reconsider m=m9 as Element of NAT by A9;
A10: m<k1+1 by A9,NAT_1:44;
then m <n by A2,XXREAL_0:2;
then
A11: m in Segm n by NAT_1:44;
then
A12: m in dom f by FUNCT_2:def 1;
m<=k1 by A10,NAT_1:13;
then min(m,k1)=m by XXREAL_0:def 9;
then f.m=m by A8,A11;
hence m9 in rng f by A12,FUNCT_1:def 3;
end;
then k c= rng f;
then k=rng f;
then
A13: f is onto by FUNCT_2:def 3;
A14: for m st m in rng f holds min* f"{m} =m
proof
let m;
assume m in rng f;
then
A15: m<k1+1 by NAT_1:44;
then
A16: m<=k1 by NAT_1:13;
m <n by A2,A15,XXREAL_0:2;
then
A17: m in Segm n by NAT_1:44;
then
A18: m in dom f by FUNCT_2:def 1;
m<=k1 by A15,NAT_1:13;
then min(m,k1)=m by XXREAL_0:def 9;
then f.m=m by A8,A17;
then
A19: f.m in {m} by TARSKI:def 1;
then
A20: m in f"{m} by A18,FUNCT_1:def 7;
A21: f"{m} is non empty by A19,A18,FUNCT_1:def 7;
now
per cases by A16,XXREAL_0:1;
suppose
A22: m<k1;
now
A23: n is Subset of NAT by Th8;
let l9 be object such that
A24: l9 in f"{m};
l9 in dom f by A24,FUNCT_1:def 7;
then l9 in n;
then reconsider l=l9 as Element of NAT by A23;
f.l in {m} by A24,FUNCT_1:def 7;
then
A25: f.l=m by TARSKI:def 1;
l in dom f by A24,FUNCT_1:def 7;
then min(l,k1)=m by A8,A25;
then l=m by A22,XXREAL_0:15;
hence l9 in {m} by TARSKI:def 1;
end;
then
A26: f"{m} c= {m};
min* f"{m} in f"{m} by A21,NAT_1:def 1;
hence thesis by A26,TARSKI:def 1;
end;
suppose
A27: m=k1;
for l be Nat st l in f"{m} holds m <= l
proof
let l be Nat such that
A28: l in f"{m};
f.l in {m} by A28,FUNCT_1:def 7;
then
A29: f.l=m by TARSKI:def 1;
l in dom f by A28,FUNCT_1:def 7;
then f.l=min(l,m) by A8,A27;
hence thesis by A29,XXREAL_0:def 9;
end;
hence thesis by A20,NAT_1:def 1;
end;
end;
hence thesis;
end;
now
let l,m such that
A30: l in rng f and
A31: m in rng f and
A32: l < m;
min* f"{l}=l by A14,A30;
hence min* f"{l} < min* f"{m} by A14,A31,A32;
end;
then f is "increasing;
hence thesis by A13;
end;
end;
hence thesis;
end;
scheme :: uogolnic na skonczone zbiory, a moze gdzies jest ??? !!!
Sch1{n,k() -> 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<k implies n block k = 0
proof
set F={f where f is Function of Segm n,Segm k:f is onto "increasing};
assume
A1: n<k;
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 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.n<k+1 by NAT_1:44;
hence contradiction by A4,NAT_1:13;
end;
suppose
A5: f.n<k;
A6: min* f"{k} <=(n+1)-1 by Th16;
A7: rng f = k+1 by A1,FUNCT_2:def 3;
k<k+1 by NAT_1:13;
then
k in rng f by A7,NAT_1:44;
then min* f"{f.n} < min* f"{k} & k in NAT & n in NAT
by A1,A5,A7,ORDINAL1:def 12;
hence contradiction by A2,A6,Th5;
end;
end;
hence contradiction;
end;
theorem Th35:
for f be Function of Segm(n+1),Segm k st k<>0 & 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: n<n+1 by NAT_1:13;
A4: f.n in {f.n} by TARSKI:def 1;
dom f =n+1 by A1,FUNCT_2:def 1;
then n in dom f by A3,NAT_1:44;
then n in f"{f.n} by A4,FUNCT_1:def 7;
then ex m be object st m in f"{f.n} & m<>n 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<j holds min* f
"{i} < min* f"{j}
proof
let f be Function of Segm n,Segm k,
g be Function of Segm(n+m),Segm(k+l) such that
A1: g is "increasing and
A2: f=g|n;
let i,j such that
A3: i in rng f and
A4: j in rng f and
A5: i<j;
A6: for k1 be Element of NAT st k1 in rng f holds k1 in rng g& min* f"{k1}=
min* g"{k1}
proof
A7: n is Subset of NAT by Th8;
let k1 be Element of NAT such that
A8: k1 in rng f;
consider x be object such that
A9: x in dom f and
A10: f.x=k1 by A8,FUNCT_1:def 3;
A11: dom f = n by A8,FUNCT_2:def 1;
x in n by A9;
then reconsider x9=x as Element of NAT by A7;
A12: x9 <n by A9,NAT_1:44;
A13: f.x9=g.x9 by A2,A9,FUNCT_1:47;
Segm k is non empty by A8;
then k is non zero;
then k+l is non zero;
then Segm(k+l) is non empty;
then
A14: dom g =Segm(n+m) by FUNCT_2:def 1;
n <= n+m by NAT_1:11;
then
A15: Segm n c= Segm(n+m) by NAT_1:39;
A16: now
let n1 be Nat such that
A17: n1 in f"{k1};
A18: n1 in n by A11,A17,FUNCT_1:def 7;
f.n1 in {k1} by A17,FUNCT_1:def 7;
then g.n1 in {k1} by A2,A11,A18,FUNCT_1:47;
then n1 in g"{k1} by A14,A15,A18,FUNCT_1:def 7;
hence min* g"{k1}<=n1 by NAT_1:def 1;
end;
k1 in {k1} by TARSKI:def 1;
then
A19: x9 in g"{k1} by A9,A10,A11,A14,A15,A13,FUNCT_1:def 7;
then min* g"{k1} <= x9 by NAT_1:def 1;
then min* g"{k1} < n by A12,XXREAL_0:2;
then
A20: min* g"{k1} in dom f by A11,NAT_1:44;
min* g"{k1} in g"{k1} by A19,NAT_1:def 1;
then g.(min* g"{k1}) in {k1} by FUNCT_1:def 7;
then f.(min* g"{k1}) in {k1} by A2,A20,FUNCT_1:47;
then min* g"{k1} in f"{k1} by A20,FUNCT_1:def 7;
hence thesis by A9,A10,A11,A14,A15,A13,A16,FUNCT_1:def 3,NAT_1:def 1;
end;
A21: i in NAT & j in NAT by ORDINAL1:def 12;
then A22: j in rng g by A4,A6;
A23: min* f"{j}=min* g"{ j} by A4,A6,A21;
A24: min* f"{i}=min* g"{i} by A3,A6,A21;
i in rng g by A3,A6,A21;
hence thesis by A1,A5,A22,A24,A23;
end;
theorem Th37:
for f be Function of Segm(n+1),Segm(k+1)
st f is onto "increasing & f"{f.n}= {n} holds rng (f|n) c= Segm k &
for g be Function of Segm n,Segm k st g=f|n holds g is onto
"increasing
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};
now
per cases;
suppose
A3: n=0;
then 0+1>=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
proof
f.i<k+1 by NAT_1:44;
then
A12: f.i<=k by NAT_1:13;
assume 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
n<n+1 by NAT_1:13;
then
A19: Segm n c= Segm(n+1) by NAT_1:39;
dom f=n+1 by FUNCT_2:def 1;
then
A20: n=dom f /\n by A19,XBOOLE_1:28;
let k1 be object such that
A21: k1 in Segm k;
reconsider k9=k1 as Element of NAT by A21;
k9<k by A21,NAT_1:44;
then k9 < k+1 by NAT_1:13;
then
A22: k9 in Segm(k+1) by NAT_1:44;
A23: dom f=n+1 by FUNCT_2:def 1;
rng f = k+1 by A1,FUNCT_2:def 3;
then consider n1 be object such that
A24: n1 in dom f and
A25: f.n1=k9 by A22,FUNCT_1:def 3;
reconsider n1 as Element of NAT by A24,A23;
n1<n+1 by A24,NAT_1:44;
then
A26: n1<=n by NAT_1:13;
reconsider nn = k1 as set by TARSKI:1;
A: not nn in nn;
f.n=k by A1,A2,Th34;
then n1<>n 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+1 by NAT_1:13;
then
A30: Segm n c= Segm(n+1) by NAT_1:39;
dom f=n+1 by FUNCT_2:def 1;
then
A31: n=dom f /\n by A30,XBOOLE_1:28;
0 in Segm n by A4,NAT_1:44;
then (f|n).0 in rng (f|n) by A31,A29,FUNCT_1:def 3;
then
A32: n=0 iff k=0 by A5;
for i,j st i in rng g & j in rng g & i<j holds min* g"{i} < min*
g"{j} by A1,A18,Th36;
hence g is "increasing by A32;
end;
end;
end;
hence thesis;
end;
theorem Th38:
for f be Function of Segm(n+1),Segm k,
g be Function of Segm n,Segm k st f is onto
"increasing & f"{f.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 & i<j holds min* g"{i} <
min* g"{j} by A1,A3,Th36;
A7: k c= rng g
proof
let k1 be object such that
A8: k1 in k;
consider x be object such that
A9: x in dom f and
A10: f.x=k1 by A5,A8,FUNCT_1:def 3;
dom f =n+1 by A8,FUNCT_2:def 1;
then reconsider x as Element of NAT by A9;
x<n+1 by A9,NAT_1:44;
then
A11: x<=n by NAT_1:13;
now
per cases by A11,XXREAL_0:1;
suppose
A12: x<n;
A13: dom g = n by A4,FUNCT_2:def 1;
A14: x in Segm n by A12,NAT_1:44;
then g.x=f.x by A3,A13,FUNCT_1:47;
hence thesis by A10,A14,A13,FUNCT_1:def 3;
end;
suppose
x=n;
then consider m such that
A15: m in f"{k1} and
A16: m<>n 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 m<n+1 by NAT_1:44;
then m<=n by NAT_1:13;
then m < n by A16,XXREAL_0:1;
then
A18: m in Segm n by NAT_1:44;
A19: n=dom g by A4,FUNCT_2:def 1;
then g.m=f.m by A3,A18,FUNCT_1:47;
hence thesis by A18,A19,A17,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
then
A20: rng g =k;
n=0 iff k=0 by A4,A7;
hence thesis by A20,A6,FUNCT_2:def 3;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th39:
for f be Function of Segm n,Segm k, g be Function of Segm(n+1),Segm(k+m)
st f is onto
"increasing & f=g|n holds for i,j st i in rng g & j in rng g & i<j holds min* g
"{i} < min* g"{j}
proof
let f be Function of Segm n,Segm k,
g be Function of Segm(n+1),Segm(k+m) such that
A1: f is onto "increasing and
A2: f=g|n;
A3: for i st i<n holds f.i=g.i
proof
k=0 iff n=0 by A1;
then
A4: dom f=n by FUNCT_2:def 1;
let i;
assume i <n;
then i in Segm n by NAT_1:44;
hence thesis by A2,A4,FUNCT_1:47;
end;
A5: for l st l in rng g & not l in rng f holds l=g.n
proof
let l such that
A6: l in rng g and
A7: not l in rng f;
consider x be object such that
A8: x in dom g and
A9: g.x=l by A6,FUNCT_1:def 3;
assume
A10: l<>g.n;
dom g=n+1 by A6,FUNCT_2:def 1;
then reconsider x as Element of NAT by A8;
x<n+1 by A8,NAT_1:44;
then x<=n by NAT_1:13;
then
A11: x<n by A10,A9,XXREAL_0:1;
then
A12: x in Segm n by NAT_1:44;
k<>0 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+1 by NAT_1:13;
let l such that
A16: l in rng g and
A17: not l in rng f;
A18: l in {l} by TARSKI:def 1;
dom g=n+1 by A16,FUNCT_2:def 1;
then
A19: n in dom g by A15,NAT_1:44;
g.n=l by A5,A16,A17;
then n in g"{l} by A19,A18,FUNCT_1:def 7;
then min* g"{l} in g"{l} by NAT_1:def 1;
then
A20: g.min* g"{l} in {l} by FUNCT_1:def 7;
assume
A21: min* g"{l}<>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 <n by A28,NAT_1:44;
then
A35: min* f"{k1} < n by A33,XXREAL_0:2;
A36: dom f = n by A27,FUNCT_2:def 1;
A37: now
let n1 be Nat such that
A38: n1 in g"{k1};
n1 in Segm(n+1) by A31,A38,FUNCT_1:def 7;
then n1<n+1 by NAT_1:44;
then
A39: n1<=n by NAT_1:13;
now
per cases by A39,XXREAL_0:1;
suppose
A40: n1<n;
g.n1 in {k1} by A38,FUNCT_1:def 7;
then
A41: f.n1 in {k1} by A3,A40;
n1 in dom f by A36,A40,NAT_1:44;
then n1 in f"{k1} by A41,FUNCT_1:def 7;
hence min* f"{k1}<=n1 by NAT_1:def 1;
end;
suppose
n1=n;
hence min* f"{k1} <= n1 by A33,A34,XXREAL_0:2;
end;
end;
hence min* f"{k1} <= n1;
end;
min* f"{k1} in f"{k1} by A32,NAT_1:def 1;
then f.(min* f"{k1}) in {k1} by FUNCT_1:def 7;
then
A42: g.(min* f"{k1}) in {k1} by A3,A35;
min* f"{k1} in n by A35,NAT_1:44;
then min* f"{k1} in g"{k1} by A31,A26,A42,FUNCT_1:def 7;
hence thesis by A37,NAT_1:def 1;
end;
let i,j such that
A43: i in rng g and
A44: j in rng g and
A45: i<j;
A46: for l st l in rng g & not l in rng f holds l>=k
proof
let l such that
l in rng g and
A47: not l in rng f;
assume l<k;
then l in Segm k by NAT_1:44;
hence thesis by A1,A47,FUNCT_2:def 3;
end;
A48:i in NAT & j in NAT by ORDINAL1:def 12;
now
per cases;
suppose
A49: i in rng f & j in rng f;
then
A50: min* g"{j}=min* f"{j} by A25,A48;
min* g"{i}=min* f"{i} by A25,A49,A48;
hence thesis by A1,A45,A49,A50;
end;
suppose
A51: i in rng f & not j in rng f;
then
A52: n<>0;
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<k+1 by A4,NAT_1:44;
then
A5: x<=k by NAT_1:13;
now
per cases by A5,XXREAL_0:1;
suppose
A6: x<k;
A7: rng f=k by A1,FUNCT_2:def 3;
x in Segm k by A6,NAT_1:44;
then consider y be object such that
A8: y in dom f and
A9: f.y =x by A7,FUNCT_1:def 3;
A10: dom g = n+1 by FUNCT_2:def 1;
n=0 iff k=0 by A1;
then
A11: dom f = n by FUNCT_2:def 1;
n<=n+1 by NAT_1:11;
then
A12: Segm n c= Segm(n+1) by NAT_1:39;
f.y=g.y by A2,A8,FUNCT_1:47;
hence thesis by A8,A9,A11,A12,A10,FUNCT_1:def 3;
end;
suppose
A13: x=k;
n<n+1 by NAT_1:13;
then
A14: n in Segm(n+1) by NAT_1:44;
dom g =n+1 by FUNCT_2:def 1;
hence thesis by A3,A13,A14,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
then k+1=rng g;
hence g is onto by FUNCT_2:def 3;
for i,j st i in rng g & j in rng g & i<j holds min* g"{i} < min* g"{j}
by A1,A2,Th39;
hence g is "increasing;
thus g"{g.n}={n}
proof
assume g"{g.n}<>{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+1 by NAT_1:44;
then m<=n by NAT_1:13;
then
A18: m<n by A16,XXREAL_0:1;
n=0 iff k=0 by A1;
then dom f=n by FUNCT_2:def 1;
then
A19: m in dom f by A18,NAT_1:44;
then
A20: f.m in rng f by FUNCT_1:def 3;
f.m=g.m by A2,A19,FUNCT_1:47;
hence contradiction by A20,A17,NAT_1:44;
end;
end;
theorem Th41:
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}
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 & i<j holds min* g"{i} < min* g"{j}
by A1,A2,Th39;
hence g is "increasing by A3;
n<=n+1 by NAT_1:11;
then
A13: Segm n c= Segm(n+1) by NAT_1:39;
reconsider nn = n as set;
A: not nn in nn;
A14: x in n by A4;
then
A15: x<>n 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: k<n implies n\/{k}=n
proof
assume k<n;
then k in Segm n by NAT_1:44;
then {k} c= n by ZFMISC_1:31;
hence thesis by XBOOLE_1:12;
end;
theorem Th42:
card{f where f is Function of Segm(n+1),Segm(k+1):
f is onto "increasing & f
"{f.n}={n}}=
card{f where f is Function of Segm n,Segm k: f is onto "increasing}
proof
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,Segm k: f is onto "increasing};
now
per cases;
suppose
A1: k=0 & n<>0;
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 (Segm n\/{n}),(Segm k\/{k})such that
A46: x=f and
A47: P[f,Segm n\/{n},Segm k\/{k}] and
rng (f|Segm n) c= Segm 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<k holds card{f where f is Function of Segm(n+1),Segm k: f is
onto "increasing & f"{f.n}<>{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<k;
set F2={f where f is Function of Segm n,Segm k: f is onto "increasing};
set F1={f where f is Function of Segm(n+1),Segm k:
f is onto "increasing & f"{f.n}<>{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 (Segm n\/{n}),(Segm k\/{l})such that
A40: x=f and
A41: P[f,Segm n\/{n},Segm k\/{l}] and
rng (f|Segm 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;
n<n+1 by NAT_1:13;
then
A11: n in Segm(n+1) by NAT_1:44;
n in dom f by A10,FUNCT_1:def 2;
then n in dom f /\ (n+1) by A11,XBOOLE_0:def 4;
then
A12: n in dom (f|(n+1)) by RELAT_1:61;
then
A13: (f|(n+1)).n=f.n by FUNCT_1:47;
(f|(n+1)).n in rng (f|(n+1)) by A12,FUNCT_1:def 3;
hence thesis by A10,A13,TARSKI:def 4;
end;
end;
hence thesis;
end;
thus union rng (f|(n+1))c=union (rng (f|n))\/f.n
proof
let x be object;
assume x in union rng (f|(n+1));
then consider Y be set such that
A14: x in Y and
A15: Y in rng (f|(n+1)) by TARSKI:def 4;
consider X be object such that
A16: X in dom (f|(n+1)) and
A17: (f|(n+1)).X=Y by A15,FUNCT_1:def 3;
A18: X in dom f /\(n+1) by A16,RELAT_1:61;
then
A19: X in Segm(n+1) by XBOOLE_0:def 4;
A20: X in dom f by A18,XBOOLE_0:def 4;
reconsider X as Element of NAT by A19;
X < n+1 by A19,NAT_1:44;
then
A21: X<=n by NAT_1:13;
now
per cases by A21,XXREAL_0:1;
suppose
X < n;
then X in Segm n by NAT_1:44;
then X in dom f/\n by A20,XBOOLE_0:def 4;
then
A22: X in dom (f|n) by RELAT_1:61;
then
A23: (f|n).X in rng (f|n) by FUNCT_1:def 3;
A24: f.X=(f|(n+1)).X by A16,FUNCT_1:47;
(f|n).X=f.X by A22,FUNCT_1:47;
then x in union rng (f|n) by A14,A17,A24,A23,TARSKI:def 4;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A25: X=n;
f.X=(f|(n+1)).X by A16,FUNCT_1:47;
hence thesis by A14,A17,A25,XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
end;
scheme Sch6{D()->non 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+1<len CardF holds f.(n+1)=addnat.(f.n,CardF.(n + 1)) and
A11: addnat "**" CardF = f.(len CardF-1) by AFINSQ_2:def 8;
defpred P[Nat] means $1<len CardF implies
card union rng (F|($1+1))=f.$1 &
union rng (F|($1+1)) is finite;
A12: for k st P[k] holds P[k + 1]
proof
let k such that
A13: P[k];
set k1=k+1;
set Fk1=F|k1;
set rFk1=rng Fk1;
assume that
A14: k1<len CardF;
reconsider urFk1=union rFk1 as finite set by A13,A14,NAT_1:13;
A15: f.k1=addnat.(f.k,CardF.k1) by A10,A14;
A16: union (rng Fk1) misses F.k1
proof
assume union (rng Fk1) meets F.k1;
then consider x being object such that
A17: x in union (rng Fk1)/\F.k1 by XBOOLE_0:4;
A18: x in F.k1 by A17,XBOOLE_0:def 4;
A19: k1 in dom F by A4,A14,NAT_1:44;
x in union (rng Fk1) by A17,XBOOLE_0:def 4;
then consider Y be set such that
A20: x in Y and
A21: Y in rng Fk1 by TARSKI:def 4;
consider X be object such that
A22: X in dom Fk1 and
A23: Fk1.X=Y by A21,FUNCT_1:def 3;
reconsider X as Element of NAT by A22;
A24: Fk1.X=F.X by A22,FUNCT_1:47;
A25: X in dom F/\k1 by A22,RELAT_1:61;
then X in k1 by XBOOLE_0:def 4;
then
A26: X<>k1;
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 <C1+1 by NAT_1:13;
A29: F|len CardF =F by A4;
A30: P[0]
proof
assume 0<len CardF;
A31: union rng (F|(0+1)) = union rng (F|0)\/F.0 by Th44;
A32: 0 in len CardF by A8,AFINSQ_1:86;
thus card union rng (F|(0+1))
= card({} \/ F.0) by A31,ZFMISC_1:2
.= card(F.0)
.= CardF.0 by A32,A5
.= f.0 by A9;
hence union rng (F|(0+1)) is finite;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A30,A12);
hence thesis by A11,A28,A29,A6;
end;
end;
end;
scheme
Sch8{X,Y()->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+1 by NAT_1:13;
then
A4: n in Segm(n+1) by NAT_1:44;
consider f be Function such that
A5: f is one-to-one and
A6: dom f = card k and
A7: rng f = k by WELLORD2:def 4;
reconsider f as Function of card Segm k,Segm k by A6,A7,FUNCT_2:1;
A8: f is onto one-to-one by A5,A7,FUNCT_2:def 3;
consider F be XFinSequence of NAT such that
A9: dom F = card Segm k and
A10: card{g where g is Function of Segm(n+1),Segm k:P[g]} = Sum(F) and
A11: for i st i in dom F holds F.i =
card{g where g is Function of Segm(n+1),Segm k:P[g] & g.n=f.i}
from Sch8(A8,A3,A4);
A12: for i be Nat st i in dom F holds F.i = n block k
proof
set F2={g where g is Function of Segm n,Segm k:
g is onto "increasing};
let i be Nat such that
A13: i in dom F;
A14: f.i in rng f by A6,A9,A13,FUNCT_1:def 3;
reconsider fi=f.i as Element of NAT by A7,A14;
A15: fi<k by A14,NAT_1:44;
set F1={g where g is Function of Segm(n+1),Segm k:P[g] & g.n=fi};
set F={g where g is Function of Segm(n+1),Segm k:
g is onto "increasing & g"{g.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 & n<k
holds Order.n < Order.k
proof
defpred P[Nat] means for N be finite Subset of NAT st card N = $1
ex F be Function of N,Segm card N st F is bijective & for n,k st n in dom F &
k in dom F & n<k holds F.n < F.k;
A1: for k st P[k] holds P[k+1]
proof
let k such that
A2: P[k];
let N be finite Subset of NAT such that
A3: card N = k+1;
defpred M[set] means $1 in N;
ex x being object st x in N by A3,CARD_1:27,XBOOLE_0:def 1;
then
A4: ex n be Nat st M[n];
consider m9 be Nat such that
A5: for n st n in N holds n<=m9 by Th56;
A6: for n be Nat st M[n] holds n<=m9 by A5;
consider m be Nat such that
A7: M[m] & for n be Nat st M[n] holds n <= m from NAT_1:sch 6(A6,A4
);
set Nm=N\{m};
consider F be Function of Nm,Segm card Nm such that
A8: F is bijective and
A9: for n,k st n in dom F & k in dom F & n<k holds F.n < F.k by A2,A3,A7,Th55;
A10: card Nm=k by A3,A7,Th55;
A11: Segm(k)\/{k}= Segm(k+1) by AFINSQ_1:2;
A12: card Nm is empty implies Nm is empty;
m in {m} by TARSKI:def 1;
then not m in Nm by XBOOLE_0:def 5;
then consider G be Function of Nm\/{m},card Nm\/{k} such that
A13: G|Nm=F and
A14: G.m=k by A12,Th57;
N= Nm\/{m} by A7,ZFMISC_1:116;
then reconsider G9=G as Function of N, Segm card N by A3,A10,A11;
take G9;
not k in card Nm by A10;
then G is one-to-one onto by A8,A12,A13,A14,Th58;
hence G9 is bijective by A11,A3,A10;
thus for n,k st n in dom G9 & k in dom G9 & n<k holds G9.n < G9.k
proof
A15: for i st i in Nm holds i < m & G9.i <k
proof
let i such that
A16: i in Nm;
not i in {m} by A16,XBOOLE_0:def 5;
then
A17: i<>m 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 <k by A19,NAT_1:44,A20;
end;
let i,j such that
A21: i in dom G9 and
A22: j in dom G9 and
A23: i<j;
A24: dom G9=Nm\/{m} by FUNCT_2:def 1;
now
per cases by A21,A22,A24,XBOOLE_0:def 3;
suppose
A25: i in Nm & j in Nm;
then
A26: j in dom F by FUNCT_2:def 1;
then
A27: F.j=G9.j by A13,FUNCT_1:47;
A28: i in dom F by A25,FUNCT_2:def 1;
then F.i=G9.i by A13,FUNCT_1:47;
hence thesis by A9,A23,A28,A26,A27;
end;
suppose
A29: i in Nm & j in {m};
then G9.i<k by A15;
hence thesis by A14,A29,TARSKI:def 1;
end;
suppose
A30: i in {m} & j in Nm;
then i=m by TARSKI:def 1;
hence thesis by A23,A15,A30;
end;
suppose
A31: i in {m} & j in {m};
then i=m by TARSKI:def 1;
hence thesis by A23,A31,TARSKI:def 1;
end;
end;
hence thesis;
end;
end;
A32: P[0]
proof
set P={};
A33: rng P={};
let N be finite Subset of NAT such that
A34: card N=0;
N is empty by A34;
then reconsider P as Function of N,Segm card N by A33,FUNCT_2:1;
take P;
rng P={};
then P is one-to-one onto by A34,FUNCT_2:def 3;
hence P is bijective;
thus thesis;
end;
for k holds P[k] from NAT_1:sch 2(A32,A1);
hence thesis;
end;
::$CT
Th60:
for X,Y be finite set,F be Function of X,Y st card X=card Y
holds F is onto iff F is one-to-one by FINSEQ_4:63;
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<k
holds F.n < F.k ex P be Permutation of N st for k st k in N holds (k < n
implies P.k=F".((F.k)+1)) & (k = n implies P.k=F".0) & (k > 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<k holds F.n < F.k;
rng F=card N by A2,FUNCT_2:def 3;
then reconsider F9=F" as Function of card N,N by A2,FUNCT_2:25;
defpred P[object,object] means
for k st k=$1 holds (k < n implies $2=F".((F.k)+1))
& (k = n implies $2=F".0) & (k > 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<x1+1 by NAT_1:13;
x < card N by A16,NAT_1:44;
then x1 < card N by A20,XXREAL_0:2;
then
A21: x1 in Segm card N by NAT_1:44;
card N=rng F by A2,FUNCT_2:def 3;
then consider y being object such that
A22: y in dom F and
A23: F.y=x1 by A21,FUNCT_1:def 3;
reconsider y as Element of NAT by A4,A22;
A24: y in dom P by A4,A22,FUNCT_2:def 1;
A25: y<n
proof
assume y>=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 <n or Px=n by A15,XXREAL_0:1;
then
A28: F.Px<=F.n by A1,A3,A4,A14;
x1+1>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<j holds min* G"{i}
< min* G"{j};
A1: P[{}]
proof
let Ne,Me be Subset of NAT,F be Function of Ne,Me such that
A2: F={} and
rng F is finite;
reconsider R=rng F as empty set by A2;
set P={};
A3: rng P={};
reconsider P as Function of R,R by A3,FUNCT_2:1;
rng R= {};
then P is one-to-one onto by FUNCT_2:def 3;
then reconsider P as Permutation of rng F;
take P,F;
rng F=R;
then F={};
hence thesis;
end;
A4: 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
let F9 be Function such that
A5: for x st x in rng F9 & Q[x,F9] holds P[F9|(dom F9\F9"{x})];
let N,K be Subset of NAT,F be Function of N,K such that
A6: F=F9 and
A7: rng F is finite;
now
per cases;
suppose
rng F9 is empty;
then F9={};
hence thesis by A1,A6;
end;
suppose
A8: rng F9 is non empty;
then reconsider domF=dom F as non empty Subset of NAT by A6,RELAT_1:42
,XBOOLE_1:1;
reconsider K as non empty Subset of NAT by A6,A8;
set m=min* domF;
set D=dom F\F"{F.m};
min* domF in domF by NAT_1:def 1;
then
A9: F.m in rng F by FUNCT_1:def 3;
now
per cases;
suppose
rng (F|D) is empty;
then rng F\{F.m}={} by Th54;
then
A10: rng F={F.m} by A9,ZFMISC_1:58;
A11: for i,j st i in rng F & j in rng F & i<j holds min* F"{i} <
min* F"{j}
proof
let i,j such that
A12: i in rng F and
A13: j in rng F and
A14: i<j;
i =F.m by A10,A12,TARSKI:def 1;
hence thesis by A10,A13,A14,TARSKI:def 1;
end;
set P=id rng F;
rng P=rng F;
then P is one-to-one onto by FUNCT_2:def 3;
then reconsider P as Permutation of rng F;
F is Function of dom F,rng F by FUNCT_2:1;
then P*F = F by FUNCT_2:17;
hence thesis by A11;
end;
suppose
A15: rng (F|D) is non empty;
rng (F|D) c= rng F by RELAT_1:70;
then reconsider
rFD=rng (F|D) as non empty finite Subset of NAT by A7,A15,
XBOOLE_1:1;
deffunc G(set)=F.m;
reconsider dFD=dom (F|D) as Subset of NAT by XBOOLE_1:1;
reconsider FD=F|D as Function of dFD,rFD by FUNCT_2:1;
A16: rFD is empty implies dFD is empty;
reconsider rF=rng F as non empty finite Subset of NAT by A7,A9,
XBOOLE_1:1;
A17: dFD c= N & rFD c= K;
consider P be Permutation of rng FD, G be Function of dFD,rFD such
that
A18: FD=P*G and
A19: rng FD = rng G and
A20: for i,j st i in rng G & j in rng G & i<j holds min* G"{i}
< min* G"{j} by A5,A6,A9;
A21: for x st x in N\dFD holds G(x) in K by A9;
consider G2 be Function of N,K such that
A22: G2|dFD=G & for x st x in N\dFD holds G2.x = G(x) from
Sch2(A21,A17,A16);
A23: rng G2 c= rng F
proof
let Gx be object;
assume Gx in rng G2;
then consider x being object such that
A24: x in dom G2 and
A25: G2.x=Gx by FUNCT_1:def 3;
dom G2=N by FUNCT_2:def 1;
then dom G2/\dFD \/(N\dFD)=dom G2 by XBOOLE_1:51;
then dom G=dom G2/\dFD & x in dom G2/\dFD or x in N\dFD by A22
,A24,RELAT_1:61,XBOOLE_0:def 3;
then
G.x in rng FD & G.x=G2.x & rng FD=rng F\{F.m} or G2.x=F.m &
m in domF by A19,A22,Th54,FUNCT_1:47,def 3,NAT_1:def 1;
hence thesis by A25,FUNCT_1:def 3,XBOOLE_0:def 5;
end;
A26: rng FD =rng F\{F.m} by Th54;
dom FD = dom F /\(dom F\F"{F.m}) by RELAT_1:61;
then
A27: dFD=dom F\F"{F.m} by XBOOLE_1:28,36;
A28: F"{F.m}c=G2"{F.m}
proof
let x be object such that
A29: x in F"{F.m};
not x in dom F\F"{F.m} by A29,XBOOLE_0:def 5;
then x in N\dFD by A27,A29,XBOOLE_0:def 5;
then G2.x=F.m by A22;
then
A30: G2.x in {F.m} by TARSKI:def 1;
x in N by A29;
then x in dom G2 by FUNCT_2:def 1;
hence thesis by A30,FUNCT_1:def 7;
end;
rng F c= rng G2
proof
rng FD=rng F\{F.m} by Th54;
then
A31: rng F=rng FD\/{F.m} by A9,ZFMISC_1:116;
let Fx be object such that
A32: Fx in rng F;
now
per cases by A32,A31,XBOOLE_0:def 3;
suppose
A33: Fx in rng FD;
rng (G2|dFD) c=rng G2 by RELAT_1:70;
hence thesis by A19,A22,A33;
end;
suppose
A34: Fx in {F.m};
A35: m in dom F by NAT_1:def 1;
then m in N;
then m in dom G2 by FUNCT_2:def 1;
then
A36: G2.m in rng G2 by FUNCT_1:def 3;
F.m in {F.m} by TARSKI:def 1;
then m in F"{F.m} by A35,FUNCT_1:def 7;
then not m in dom F\F"{F.m} by XBOOLE_0:def 5;
then
A37: m in N\dFD by A27,A35,XBOOLE_0:def 5;
Fx=F.m by A34,TARSKI:def 1;
hence thesis by A22,A37,A36;
end;
end;
hence thesis;
end;
then
A38: rng G2=rng F by A23;
not F.m in rng F\{F.m} by ZFMISC_1:56;
then not F.m in rng FD by Th54;
then consider
P2 be Function of rng FD\/{F.m},rng FD\/{F.m} such that
A39: P2|(rng FD) = P and
A40: P2.(F.m)=(F.m) by Th57;
not F.m in rng F\{F.m} by ZFMISC_1:56;
then
A41: P2 is one-to-one onto by A39,A40,A26,Th58;
rng FD\/{F.m} = rng F by A9,A26,ZFMISC_1:116;
then reconsider P2 as Permutation of rng F by A41;
consider Orde be Function of rF,Segm card rF such that
A42: Orde is bijective and
A43: for n,k st n in dom Orde & k in dom Orde & n<k holds Orde
.n < Orde.k by Th59;
rng Orde=card rF by A42,FUNCT_2:def 3;
then reconsider Orde9=Orde" as Function of card rF,rF by A42,
FUNCT_2:25;
consider P1 be Permutation of rF such that
A44: for k st k in rF holds (k < F.m implies P1.k=Orde".((Orde
.k)+1)) & (k = F.m implies P1.k=Orde".0) & (k > 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<j holds min* PG"{i}
< min* PG"{j}
proof
A59: for l st l in rF & l < F.m holds Orde.l+1 in rng Orde &
Orde.l+1 is Element of NAT & Orde.l+1<=Orde.(F.m) & Orde.(F.m) is Element of
NAT & dom Orde=rF
proof
A60: dom Orde=rF by FUNCT_2:def 1;
A61: Orde.(F.m) in card rF;
A62: Orde.(F.m) < card rF by NAT_1:44;
let l such that
A63: l in rF and
A64: l < F.m;
A65: Orde.l < Orde.(F.m) by A9,A43,A63,A64,A60;
then Orde.l+1<=Orde.(F.m) by NAT_1:13;
then
A66: Orde.l+1 < card rF by A62,XXREAL_0:2;
card rF=rng Orde by A42,FUNCT_2:def 3;
hence thesis by A65,A61,A66,FUNCT_2:def 1,NAT_1:13,44;
end;
A67: for n,k st n in dom Orde & k in dom Orde & Orde.n<Orde.k
holds n < k
proof
let n,k such that
A68: n in dom Orde and
A69: k in dom Orde and
A70: Orde.n<Orde.k;
assume n>=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<Orde9.k
proof
let n,k such that
A72: n in rng Orde and
A73: k in rng Orde;
A74: n = Orde.(Orde9.n) by A42,A72,FUNCT_1:35;
A75: dom Orde = rng Orde9 by A42,FUNCT_1:33;
A76: k = Orde.(Orde9.k) by A42,A73,FUNCT_1:35;
assume
A77: n < k;
A78: rng Orde = dom Orde9 by A42,FUNCT_1:33;
then
A79: Orde9.n in dom Orde by A72,A75,FUNCT_1:def 3;
Orde9.k in dom Orde by A73,A78,A75,FUNCT_1:def 3;
hence thesis by A67,A77,A74,A76,A79;
end;
rng FD =rng F\{F.m} by Th54;
then
A80: rng FD\/{F.m} = rng G2 by A9,A38,ZFMISC_1:116;
let i,j such that
A81: i in rng PG and
A82: j in rng PG and
A83: i<j;
consider i1 be set such that
A84: i1 in dom P1 and
A85: i1 in rng G2 and
A86: P1"{i}={i1} and
A87: G2"{i1}=PG"{i} by A81,Th61;
consider j1 be set such that
A88: j1 in dom P1 and
A89: j1 in rng G2 and
A90: P1"{j}={j1} and
A91: G2"{j1}=PG"{j} by A82,Th61;
dom P1=rF by FUNCT_2:def 1;
then reconsider i1,j1 as Element of NAT by A84,A88;
A92: i1 in P1"{i} by A86,TARSKI:def 1;
then P1.i1 in {i} by FUNCT_1:def 7;
then
A93: P1.i1=i by TARSKI:def 1;
A94: j1 in P1"{j} by A90,TARSKI:def 1;
then
A95: P1.j1 in {j} by FUNCT_1:def 7;
then
A96: P1.j1=j by TARSKI:def 1;
A97: dom Orde=rF by FUNCT_2:def 1;
now
per cases by XXREAL_0:1;
suppose
A98: i1 < F.m & j1<F.m;
A99: i1 in rng FD or i1 in {F.m} by A85,A80,XBOOLE_0:def 3;
then
A100: G"{i1}=PG"{i} by A55,A87,A98,TARSKI:def 1;
A101: j1 in rng FD or j1 in {F.m} by A89,A80,XBOOLE_0:def 3;
i1<j1
proof
assume i1>=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}<min* G"{j1} by A19,A20,A98,A99,A101,
TARSKI:def 1;
hence thesis by A55,A91,A98,A101,A100,TARSKI:def 1;
end;
suppose
A106: i1 = F.m & j1<>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: m<min* PG"{j} by A111,XXREAL_0:1;
PG"{i} is Subset of NAT by XBOOLE_1:1;
then min* PG"{i} <= m by A28,A87,A106,A113,NAT_1:def 1;
hence thesis by A114,XXREAL_0:2;
end;
suppose
A115: i1 < F.m & j1=F.m;
card rF=rng Orde by A42,FUNCT_2:def 3;
then
A116: 0 in rng Orde by NAT_1:44;
Orde.i1+1 in rng Orde by A84,A59,A115;
then
A117: Orde9.(Orde.i1+1)>Orde9.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<j1 by A131,XXREAL_0:2;
then min* G"{i1}<min* G"{j1} by A19,A20,A131,A132,A134,
TARSKI:def 1;
hence thesis by A55,A91,A131,A134,A133,TARSKI:def 1;
end;
suppose
A135: i1 > F.m & j1<F.m;
then dom Orde=rF by A88,A59;
then
A136: Orde.(F.m) in rng Orde by A9,FUNCT_1:def 3;
Orde.j1+1 <= Orde.(F.m) by A88,A59,A135;
then
A137: Orde.j1+1 < Orde.(F.m) or Orde.j1+1 = Orde.(F.m) by
XXREAL_0:1;
F.m in dom Orde by A9,A88,A59,A135;
then
A138: Orde9.(Orde.(F.m))=F.m by A42,FUNCT_1:34;
A139: P1.i1=i1 by A44,A84,A135;
A140: Orde9.(Orde.j1+1)=P1.j1 by A44,A88,A135;
Orde.j1+1 in rng Orde by A88,A59,A135;
then P1.j1<=F.m by A71,A137,A136,A138,A140;
hence thesis by A83,A93,A96,A135,A139,XXREAL_0:2;
end;
end;
hence thesis;
end;
K is non empty;
then
A141: dom F=N by FUNCT_2:def 1;
A142: for x being object st x in dom F holds F.x = P2.(G2.x)
proof
let x being object such that
A143: x in dom F;
now
per cases by A143,XBOOLE_0:def 5;
suppose
A144: x in N\dFD;
then
A145: not x in dom F\F"{F.m} by A27,XBOOLE_0:def 5;
x in dom F by A141,A144,XBOOLE_0:def 5;
then x in F"{F.m} by A145,XBOOLE_0:def 5;
then
A146: F.x in {F.m} by FUNCT_1:def 7;
P2.(G2.x)=F.m by A22,A40,A144;
hence thesis by A146,TARSKI:def 1;
end;
suppose
A147: x in dFD;
then
A148: F.x=FD.x by FUNCT_1:47;
A149: FD.x=P.(G.x) by A18,A147,FUNCT_1:12;
A150: dom P=rng FD by FUNCT_2:def 1;
A151: x in dom G by A147,FUNCT_2:def 1;
then
A152: G.x in rng FD by A19,FUNCT_1:def 3;
G.x=G2.x by A22,A151,FUNCT_1:47;
hence thesis by A39,A148,A149,A152,A150,FUNCT_1:47;
end;
end;
hence thesis;
end;
A153: dom G2=N by FUNCT_2:def 1;
for x being object holds x in dom F iff x in dom G2&G2.x in dom P2
proof
let x be object;
thus x in dom F implies x in dom G2 & G2.x in dom P2
proof
assume
A154: x in dom F;
then dom P2=rng F by A153,FUNCT_2:def 1;
hence thesis by A38,A153,A154,FUNCT_1:def 3;
end;
thus thesis by A141;
end;
then F=P2*G2 by A142,FUNCT_1:10;
then
A155: F=P21*PG by A47,RELAT_1:36;
rng P1=rF by FUNCT_2:def 3;
then rng (P1*G2)=rF by A38,A45,FUNCT_2:14;
hence thesis by A155,A58;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A156: for F be Function st rng F is finite holds P[F] from Sch9(A1,A4);
let F be Function of Ne,Ke;
assume rng F is finite;
then consider P be Permutation of rng F,G be Function of Ne,Ke such that
A157: F=P*G and
A158: rng F=rng G and
A159: for i,j st i in rng G& j in rng G & i<j holds min* G"{i}<min* G"{j
} by A156;
G is 'increasing by A159;
hence thesis by A157,A158;
end;
:: uniqueness of expansion
theorem Th64:
for F be Function of Ne,Ke st rng F is finite for I1,I2 be
Function of Ne,Me,P1,P2 be Function st P1 is one-to-one & P2 is one-to-one &
rng I1=rng I2 & rng I1=dom P1 & dom P1=dom P2 & F=P1*I1 & F=P2*I2 & I1 is
'increasing & I2 is 'increasing holds P1=P2 & I1=I2
proof
defpred Q[set,Function] means $1=$2.(min* dom $2);
defpred P[set] means for Ne,Ke,Me be Subset of NAT for F be Function of Ne,
Ke st F=$1 for I1,I2 be Function of Ne,Me, P1,P2 be Function st P1 is
one-to-one & P2 is one-to-one & rng I1=rng I2 & rng I1=dom P1 & dom P1=dom P2 &
F=P1*I1 & F=P2*I2 & I1 is 'increasing & I2 is 'increasing holds P1=P2 & I1=I2;
A1: P[{}]
proof
let Ne,Ke,Me be Subset of NAT;
let F be Function of Ne,Ke such that
A2: F={};
let I1,I2 be Function of Ne,Me, P1,P2 be Function such that
P1 is one-to-one and
P2 is one-to-one and
A3: rng I1=rng I2 and
A4: rng I1=dom P1 and
A5: dom P1=dom P2 and
A6: F=P1*I1 and
F=P2*I2 and
I1 is 'increasing and
I2 is 'increasing;
dom I1={} by A2,A4,A6,RELAT_1:27;
then
A7: I1={};
rng P1={} by A2,A4,A6,RELAT_1:28,38;
then P1={};
hence thesis by A3,A5,A7;
end;
A8: 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
let F9 be Function such that
A9: for x st x in rng F9 & Q[x,F9] holds P[F9|(dom F9\F9"{x})];
now
per cases;
suppose
F9={};
hence thesis by A1;
end;
suppose
A10: F9<>{};
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
::$L https://en.wikipedia.org/wiki/Stirling_numbers_of_the_second_kind 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;