let n, q be Nat; ( 0 < q implies card (Funcs (n,q)) = q |^ n )
assume A1:
0 < q
; 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;
Funcs ({},q) = {{}}
by FUNCT_5:64;
then card (Funcs (0,q)) =
1
by CARD_1:50
.=
q #Z 0
by PREPOWER:44
.=
q |^ 0
by PREPOWER:46
;
then A2:
S1[ 0 ]
;
A3:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
S1[n + 1]
reconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
reconsider q9 =
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),
q9) holds
ex
y being
set st
(
y in Funcs (
n,
q9) &
S2[
x,
y] )
proof
let x be
set ;
( x in Funcs ((n + 1),q9) implies ex y being set st
( y in Funcs (n,q9) & S2[x,y] ) )
assume
x in Funcs (
(n + 1),
q9)
;
ex y being set st
( y in Funcs (n,q9) & S2[x,y] )
then consider f being
Function such that A6:
x = f
and A7:
dom f = n + 1
and A8:
rng f c= q9
by FUNCT_2:def 2;
reconsider f =
f as
Function of
(n + 1),
q9 by A7, 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 A7, RELAT_1:90;
rng (f | n) c= q9
;
then
f | n in Funcs (
n,
q9)
by A10, FUNCT_2:def 2;
hence
ex
y being
set st
(
y in Funcs (
n,
q9) &
S2[
x,
y] )
by A6;
verum
end;
consider G being
Function of
(Funcs ((n + 1),q9)),
(Funcs (n,q9)) such that A11:
for
x being
set st
x in Funcs (
(n + 1),
q9) holds
S2[
x,
G . x]
from FUNCT_2:sch 1(A5);
for
x being
set st
x in Funcs (
n,
q9) holds
x in rng G
proof
let x be
set ;
( x in Funcs (n,q9) implies x in rng G )
assume A12:
x in Funcs (
n,
q9)
;
x in rng G
consider y being
set such that A13:
y in q9
by XBOOLE_0:def 1;
reconsider g =
x as
Element of
Funcs (
n,
q9)
by A12;
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 ;
( y in q implies g +* (n .--> y) in G " {g} )
assume A14:
y in q
;
g +* (n .--> y) in G " {g}
consider f being
Function such that A15:
f = g +* (n .--> y)
;
A16:
dom g = n
by FUNCT_2:def 1;
A17:
dom (n .--> y) = {n}
by FUNCT_2:def 1;
then
dom f = n \/ {n}
by A15, 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 A15, FUNCT_4:18;
consider gg being
Function;
{y} c= q
by A14, 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 A15, 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 A15, A20, A22, FUNCT_1:def 13;
verum
end;
then
g +* (n .--> y) in G " {g}
by A13;
then consider b being
set such that A23:
b in rng G
and A24:
[(g +* (n .--> y)),b] in G
and
b in {g}
by RELAT_1:166;
g +* (n .--> y) in dom G
by A24, FUNCT_1:8;
then
S2[
g +* (n .--> y),
G . (g +* (n .--> y))]
by A11;
then A25:
(g +* (n .--> y)) | n = b
by A24, FUNCT_1:8;
A26:
dom g = n
by FUNCT_2:def 1;
A27:
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, A25, A26, A27, FUNCT_4:34;
verum
end;
then
Funcs (
n,
q9)
c= rng G
by TARSKI:def 3;
then A28:
rng G = Funcs (
n,
q9)
by XBOOLE_0:def 10;
A29:
for
x being
Element of
Funcs (
n,
q9) holds
(
G " {x} is
finite &
card (G " {x}) = q )
proof
let x be
Element of
Funcs (
n,
q9);
( G " {x} is finite & card (G " {x}) = q )
deffunc H1(
set )
-> set =
x +* (n .--> $1);
A30:
for
y being
set st
y in q holds
H1(
y)
in G " {x}
proof
let y be
set ;
( y in q implies H1(y) in G " {x} )
assume A31:
y in q
;
H1(y) in G " {x}
consider f being
Function such that A32:
f = x +* (n .--> y)
;
A33:
dom x = n
by FUNCT_2:def 1;
A34:
dom (n .--> y) = {n}
by FUNCT_2:def 1;
then
dom f = n \/ {n}
by A32, A33, FUNCT_4:def 1;
then A35:
dom f = n + 1
by AFINSQ_1:4;
rng (n .--> y) = {y}
by FUNCOP_1:14;
then A36:
rng f c= (rng x) \/ {y}
by A32, FUNCT_4:18;
consider gg being
Function;
{y} c= q
by A31, ZFMISC_1:37;
then
(rng x) \/ {y} c= q
by XBOOLE_1:8;
then
rng f c= q
by A36, XBOOLE_1:1;
then A37:
f in Funcs (
(n + 1),
q)
by A35, 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 A38:
f | n = x
by A32, A33, A34, FUNCT_4:34;
S2[
f,
G . f]
by A11, A37;
then A39:
G . f in {x}
by A38, TARSKI:def 1;
dom G = Funcs (
(n + 1),
q)
by FUNCT_2:def 1;
hence
H1(
y)
in G " {x}
by A32, A37, A39, FUNCT_1:def 13;
verum
end;
consider H being
Function of
q,
(G " {x}) such that A40:
for
y being
set st
y in q holds
H . y = H1(
y)
from FUNCT_2:sch 2(A30);
A41:
for
c being
set st
c in G " {x} holds
ex
y being
set st
(
y in q &
H . y = c )
{x} c= rng G
by A28, ZFMISC_1:37;
then A49:
G " {x} <> {}
by RELAT_1:174;
A50:
rng H = G " {x}
by A41, FUNCT_2:16;
A51:
dom H = q
by A49, 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 ;
( x1 in dom H & x2 in dom H & H . x1 = H . x2 implies x1 = x2 )
assume that A52:
x1 in dom H
and A53:
x2 in dom H
and A54:
H . x1 = H . x2
;
x1 = x2
A55:
H . x2 = x +* (n .--> x2)
by A40, A53;
A56:
dom (n .--> x1) = {n}
by FUNCOP_1:19;
A57:
dom (n .--> x2) = {n}
by FUNCOP_1:19;
set fx1 =
x +* (n .--> x1);
set fx2 =
x +* (n .--> x2);
A58:
x +* (n .--> x1) = x +* (n .--> x2)
by A40, A52, A54, A55;
A59:
(n .--> x1) . n = x1
by FUNCOP_1:87;
A60:
(n .--> x2) . n = x2
by FUNCOP_1:87;
A61:
n in {n}
by TARSKI:def 1;
then
(x +* (n .--> x1)) . n = x1
by A56, A59, FUNCT_4:14;
hence
x1 = x2
by A57, A58, A60, A61, FUNCT_4:14;
verum
end;
then
H is
one-to-one
by FUNCT_1:def 8;
then
q,
H .: q are_equipotent
by A51, CARD_1:60;
then
q,
rng H are_equipotent
by A51, RELAT_1:146;
hence
(
G " {x} is
finite &
card (G " {x}) = q )
by A50, CARD_1:def 5;
verum
end;
A62:
for
x,
y being
set st
x is
Element of
Funcs (
n,
q9) &
y is
Element of
Funcs (
n,
q9) &
x <> y holds
G " {x} misses G " {y}
proof
let x,
y be
set ;
( x is Element of Funcs (n,q9) & y is Element of Funcs (n,q9) & x <> y implies G " {x} misses G " {y} )
assume that
x is
Element of
Funcs (
n,
q9)
and
y is
Element of
Funcs (
n,
q9)
and A63:
x <> y
;
G " {x} misses G " {y}
now assume
not
G " {x} misses G " {y}
;
contradictionthen
not
(G " {x}) /\ (G " {y}) = {}
by XBOOLE_0:def 7;
then consider f being
set such that A64:
f in (G " {x}) /\ (G " {y})
by XBOOLE_0:def 1;
f in G " {x}
by A64, XBOOLE_0:def 4;
then A65:
G . f in {x}
by FUNCT_1:def 13;
reconsider f =
f as
Function of
(n + 1),
q by A64, FUNCT_2:121;
f in Funcs (
(n + 1),
q)
by A1, FUNCT_2:11;
then A66:
S2[
f,
G . f]
by A11;
then A67:
f | n = x
by A65, TARSKI:def 1;
f in G " {y}
by A64, XBOOLE_0:def 4;
then
G . f in {y}
by FUNCT_1:def 13;
hence
contradiction
by A63, A66, A67, TARSKI:def 1;
verum end;
hence
G " {x} misses G " {y}
;
verum
end;
reconsider X =
{ (G " {x}) where x is Element of Funcs (n,q9) : verum } as
set ;
A68:
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 ;
( x in Funcs ((n + 1),q) implies x in union X )
assume
x in Funcs (
(n + 1),
q)
;
x in union X
then consider f being
Function of
(n + 1),
q such that A71:
x = f
and A72:
G . x = f | n
by A11;
A73:
f in Funcs (
(n + 1),
q)
by A1, FUNCT_2:11;
then A74:
f in dom G
by FUNCT_2:def 1;
G . f in {(f | n)}
by A71, A72, TARSKI:def 1;
then A75:
f in G " {(f | n)}
by A74, FUNCT_1:def 13;
ex
y being
set st
(
y in Funcs (
n,
q9) &
S2[
f,
y] )
by A5, A73;
then
G " {(f | n)} in X
;
hence
x in union X
by A71, A75, TARSKI:def 4;
verum
end;
then A76:
union X = Funcs (
(n + 1),
q)
by A68, TARSKI:2;
Funcs (
(n + 1),
q) is
finite
by FRAENKEL:16;
then reconsider X =
X as
finite set by A76, FINSET_1:25;
A77:
card X = q |^ n
proof
deffunc H1(
set )
-> Element of
bool (Funcs ((n + 1),q9)) =
G " {$1};
A78:
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 A79:
for
x being
set st
x in Funcs (
n,
q) holds
F . x = H1(
x)
from FUNCT_2:sch 2(A78);
A80:
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,
q9);
A82:
G " {gg} in X
;
A83:
rng F = X
by A80, FUNCT_2:16;
A84:
dom F = Funcs (
n,
q)
by A82, 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 A84, CARD_1:60;
then
Funcs (
n,
q),
rng F are_equipotent
by A84, RELAT_1:146;
hence
card X = q |^ n
by A4, A83, CARD_1:21;
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 A76, A77, NEWTON:11;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A2, A3);
hence
card (Funcs (n,q)) = q |^ n
; verum