let n, q be Nat; :: thesis: ( 0 < q implies card (Funcs n,q) = q |^ n )
assume A1:
0 < q
; :: thesis: card (Funcs n,q) = q |^ n
reconsider q = q as Element of NAT by ORDINAL1:def 13;
defpred S1[ Nat] means card (Funcs $1,q) = q |^ $1;
A2:
S1[ 0 ]
A3:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
:: thesis: S1[n + 1]
reconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
reconsider q' =
q as non
empty set by A1;
defpred S2[
set ,
set ]
means ex
x being
Function of
(n + 1),
q st
( $1
= x & $2
= x | n );
A5:
for
x being
set st
x in Funcs (n + 1),
q' holds
ex
y being
set st
(
y in Funcs n,
q' &
S2[
x,
y] )
proof
let x be
set ;
:: thesis: ( x in Funcs (n + 1),q' implies ex y being set st
( y in Funcs n,q' & S2[x,y] ) )
assume A6:
x in Funcs (n + 1),
q'
;
:: thesis: ex y being set st
( y in Funcs n,q' & S2[x,y] )
consider f being
Function such that A7:
x = f
and A8:
(
dom f = n + 1 &
rng f c= q' )
by A6, FUNCT_2:def 2;
reconsider f =
f as
Function of
(n + 1),
q' by A8, FUNCT_2:4;
not
n in n
;
then A9:
n misses {n}
by ZFMISC_1:56;
(n + 1) /\ n = (n \/ {n}) /\ n
by AFINSQ_1:4;
then
(n + 1) /\ n = (n /\ n) \/ ({n} /\ n)
by XBOOLE_1:23;
then
(n + 1) /\ n = n \/ {}
by A9, XBOOLE_0:def 7;
then A10:
dom (f | n) = n
by A8, RELAT_1:90;
rng (f | n) c= q'
;
then
f | n in Funcs n,
q'
by A10, FUNCT_2:def 2;
hence
ex
y being
set st
(
y in Funcs n,
q' &
S2[
x,
y] )
by A7;
:: thesis: verum
end;
consider G being
Function of
(Funcs (n + 1),q'),
(Funcs n,q') such that A11:
for
x being
set st
x in Funcs (n + 1),
q' holds
S2[
x,
G . x]
from FUNCT_2:sch 1(A5);
A12:
rng G = Funcs n,
q'
proof
for
x being
set st
x in Funcs n,
q' holds
x in rng G
proof
let x be
set ;
:: thesis: ( x in Funcs n,q' implies x in rng G )
assume A13:
x in Funcs n,
q'
;
:: thesis: x in rng G
consider y being
set such that A14:
y in q'
by XBOOLE_0:def 1;
reconsider g =
x as
Element of
Funcs n,
q' by A13;
set fx =
g +* (n .--> y);
for
y being
set st
y in q holds
g +* (n .--> y) in G " {g}
proof
let y be
set ;
:: thesis: ( y in q implies g +* (n .--> y) in G " {g} )
assume A15:
y in q
;
:: thesis: g +* (n .--> y) in G " {g}
consider f being
Function such that A16:
f = g +* (n .--> y)
;
A17:
(
dom g = n &
dom (n .--> y) = {n} )
by FUNCT_2:def 1;
then
dom f = n \/ {n}
by A16, FUNCT_4:def 1;
then A18:
dom f = n + 1
by AFINSQ_1:4;
rng (n .--> y) = {y}
by FUNCOP_1:14;
then A19:
rng f c= (rng g) \/ {y}
by A16, FUNCT_4:18;
consider gg being
Function;
{y} c= q
by A15, ZFMISC_1:37;
then
(rng g) \/ {y} c= q
by XBOOLE_1:8;
then
rng f c= q
by A19, XBOOLE_1:1;
then A20:
f in Funcs (n + 1),
q
by A18, FUNCT_2:def 2;
then reconsider f =
f as
Function of
(n + 1),
q by FUNCT_2:121;
not
n in n
;
then
n misses {n}
by ZFMISC_1:56;
then A21:
f | n = g
by A16, A17, FUNCT_4:34;
S2[
f,
G . f]
by A11, A20;
then A22:
G . f in {x}
by A21, TARSKI:def 1;
dom G = Funcs (n + 1),
q
by FUNCT_2:def 1;
hence
g +* (n .--> y) in G " {g}
by A16, A20, A22, FUNCT_1:def 13;
:: thesis: verum
end;
then
g +* (n .--> y) in G " {g}
by A14;
then consider b being
set such that A23:
(
b in rng G &
[(g +* (n .--> y)),b] in G &
b in {g} )
by RELAT_1:166;
(
b in rng G &
g +* (n .--> y) in dom G &
G . (g +* (n .--> y)) = b )
by A23, FUNCT_1:8;
then
S2[
g +* (n .--> y),
G . (g +* (n .--> y))]
by A11;
then A24:
(g +* (n .--> y)) | n = b
by A23, FUNCT_1:8;
A25:
(
dom g = n &
dom (n .--> y) = {n} )
by FUNCT_2:def 1;
not
n in n
;
then
n misses {n}
by ZFMISC_1:56;
hence
x in rng G
by A23, A24, A25, FUNCT_4:34;
:: thesis: verum
end;
then
Funcs n,
q' c= rng G
by TARSKI:def 3;
hence
rng G = Funcs n,
q'
by XBOOLE_0:def 10;
:: thesis: verum
end;
A26:
for
x being
Element of
Funcs n,
q' holds
(
G " {x} is
finite &
card (G " {x}) = q )
proof
let x be
Element of
Funcs n,
q';
:: thesis: ( G " {x} is finite & card (G " {x}) = q )
deffunc H1(
set )
-> set =
x +* (n .--> $1);
A27:
for
y being
set st
y in q holds
H1(
y)
in G " {x}
proof
let y be
set ;
:: thesis: ( y in q implies H1(y) in G " {x} )
assume A28:
y in q
;
:: thesis: H1(y) in G " {x}
consider f being
Function such that A29:
f = x +* (n .--> y)
;
A30:
(
dom x = n &
dom (n .--> y) = {n} )
by FUNCT_2:def 1;
then
dom f = n \/ {n}
by A29, FUNCT_4:def 1;
then A31:
dom f = n + 1
by AFINSQ_1:4;
rng (n .--> y) = {y}
by FUNCOP_1:14;
then A32:
rng f c= (rng x) \/ {y}
by A29, FUNCT_4:18;
consider gg being
Function;
{y} c= q
by A28, ZFMISC_1:37;
then
(rng x) \/ {y} c= q
by XBOOLE_1:8;
then
rng f c= q
by A32, XBOOLE_1:1;
then A33:
f in Funcs (n + 1),
q
by A31, FUNCT_2:def 2;
then reconsider f =
f as
Function of
(n + 1),
q by FUNCT_2:121;
not
n in n
;
then
n misses {n}
by ZFMISC_1:56;
then A34:
f | n = x
by A29, A30, FUNCT_4:34;
S2[
f,
G . f]
by A11, A33;
then A35:
G . f in {x}
by A34, TARSKI:def 1;
dom G = Funcs (n + 1),
q
by FUNCT_2:def 1;
hence
H1(
y)
in G " {x}
by A29, A33, A35, FUNCT_1:def 13;
:: thesis: verum
end;
consider H being
Function of
q,
(G " {x}) such that A36:
for
y being
set st
y in q holds
H . y = H1(
y)
from FUNCT_2:sch 2(A27);
A37:
for
c being
set st
c in G " {x} holds
ex
y being
set st
(
y in q &
H . y = c )
(
{x} <> {} &
{x} c= rng G )
by A12, ZFMISC_1:37;
then A44:
G " {x} <> {}
by RELAT_1:174;
then A45:
rng H = G " {x}
by A37, FUNCT_2:16;
A46:
dom H = q
by A44, FUNCT_2:def 1;
for
x1,
x2 being
set st
x1 in dom H &
x2 in dom H &
H . x1 = H . x2 holds
x1 = x2
proof
let x1,
x2 be
set ;
:: thesis: ( x1 in dom H & x2 in dom H & H . x1 = H . x2 implies x1 = x2 )
assume that A47:
x1 in dom H
and A48:
x2 in dom H
and A49:
H . x1 = H . x2
;
:: thesis: x1 = x2
A50:
H . x2 = x +* (n .--> x2)
by A36, A48;
A51:
(
dom (n .--> x1) = {n} &
dom (n .--> x2) = {n} )
by FUNCOP_1:19;
set fx1 =
x +* (n .--> x1);
set fx2 =
x +* (n .--> x2);
A52:
x +* (n .--> x1) = x +* (n .--> x2)
by A36, A47, A49, A50;
A53:
(
(n .--> x1) . n = x1 &
(n .--> x2) . n = x2 )
by FUNCOP_1:87;
A54:
n in {n}
by TARSKI:def 1;
then
(x +* (n .--> x1)) . n = x1
by A51, A53, FUNCT_4:14;
hence
x1 = x2
by A51, A52, A53, A54, FUNCT_4:14;
:: thesis: verum
end;
then
H is
one-to-one
by FUNCT_1:def 8;
then
q,
H .: q are_equipotent
by A46, CARD_1:60;
then
q,
rng H are_equipotent
by A46, RELAT_1:146;
then
card (G " {x}) = card q
by A45, CARD_1:21;
hence
(
G " {x} is
finite &
card (G " {x}) = q )
by CARD_1:def 5;
:: thesis: verum
end;
A55:
for
x,
y being
set st
x is
Element of
Funcs n,
q' &
y is
Element of
Funcs n,
q' &
x <> y holds
G " {x} misses G " {y}
proof
let x,
y be
set ;
:: thesis: ( x is Element of Funcs n,q' & y is Element of Funcs n,q' & x <> y implies G " {x} misses G " {y} )
assume that
x is
Element of
Funcs n,
q'
and
y is
Element of
Funcs n,
q'
and A56:
x <> y
;
:: thesis: G " {x} misses G " {y}
now assume
not
G " {x} misses G " {y}
;
:: thesis: contradictionthen
not
(G " {x}) /\ (G " {y}) = {}
by XBOOLE_0:def 7;
then consider f being
set such that A57:
f in (G " {x}) /\ (G " {y})
by XBOOLE_0:def 1;
f in G " {x}
by A57, XBOOLE_0:def 4;
then A58:
(
f in dom G &
G . f in {x} )
by FUNCT_1:def 13;
reconsider f =
f as
Function of
(n + 1),
q by A57, FUNCT_2:121;
f in Funcs (n + 1),
q
by A1, FUNCT_2:11;
then A59:
S2[
f,
G . f]
by A11;
then A60:
f | n = x
by A58, TARSKI:def 1;
f in G " {y}
by A57, XBOOLE_0:def 4;
then
G . f in {y}
by FUNCT_1:def 13;
hence
contradiction
by A56, A59, A60, TARSKI:def 1;
:: thesis: verum end;
hence
G " {x} misses G " {y}
;
:: thesis: verum
end;
reconsider X =
{ (G " {x}) where x is Element of Funcs n,q' : verum } as
set ;
A61:
union X = Funcs (n + 1),
q
proof
A62:
for
y being
set st
y in union X holds
y in Funcs (n + 1),
q
for
y being
set st
y in Funcs (n + 1),
q holds
y in union X
proof
let x be
set ;
:: thesis: ( x in Funcs (n + 1),q implies x in union X )
assume A67:
x in Funcs (n + 1),
q
;
:: thesis: x in union X
consider f being
Function of
(n + 1),
q such that A68:
(
x = f &
G . x = f | n )
by A11, A67;
A69:
f in Funcs (n + 1),
q
by A1, FUNCT_2:11;
then
(
f in dom G &
G . f in {(f | n)} )
by A68, FUNCT_2:def 1, TARSKI:def 1;
then A70:
f in G " {(f | n)}
by FUNCT_1:def 13;
consider y being
set such that A71:
(
y in Funcs n,
q' &
S2[
f,
y] )
by A5, A69;
G " {(f | n)} in X
by A71;
hence
x in union X
by A68, A70, TARSKI:def 4;
:: thesis: verum
end;
hence
union X = Funcs (n + 1),
q
by A62, TARSKI:2;
:: thesis: verum
end;
Funcs (n + 1),
q is
finite
by FRAENKEL:16;
then reconsider X =
X as
finite set by A61, FINSET_1:25;
A72:
card X = q |^ n
proof
deffunc H1(
set )
-> Element of
bool (Funcs (n + 1),q') =
G " {$1};
A73:
for
x being
set st
x in Funcs n,
q holds
H1(
x)
in X
;
consider F being
Function of
(Funcs n,q),
X such that A74:
for
x being
set st
x in Funcs n,
q holds
F . x = H1(
x)
from FUNCT_2:sch 2(A73);
A75:
for
c being
set st
c in X holds
ex
x being
set st
(
x in Funcs n,
q &
c = F . x )
consider gg being
Element of
Funcs n,
q';
A78:
G " {gg} in X
;
then A79:
rng F = X
by A75, FUNCT_2:16;
A80:
dom F = Funcs n,
q
by A78, FUNCT_2:def 1;
for
x1,
x2 being
set st
x1 in dom F &
x2 in dom F &
F . x1 = F . x2 holds
x1 = x2
then
F is
one-to-one
by FUNCT_1:def 8;
then
Funcs n,
q,
F .: (Funcs n,q) are_equipotent
by A80, CARD_1:60;
then
Funcs n,
q,
rng F are_equipotent
by A80, RELAT_1:146;
hence
card X = q |^ n
by A4, A79, CARD_1:21;
:: thesis: verum
end;
for
Y being
set st
Y in X holds
ex
B being
finite set st
(
B = Y &
card B = q & ( for
Z being
set st
Z in X &
Y <> Z holds
(
Y,
Z are_equipotent &
Y misses Z ) ) )
then
ex
C being
finite set st
(
C = union X &
card C = q * (card X) )
by GROUP_2:186;
hence
S1[
n + 1]
by A61, A72, NEWTON:11;
:: thesis: verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A2, A3);
hence
card (Funcs n,q) = q |^ n
; :: thesis: verum