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 12;
defpred S1[ Nat] means card (Funcs ($1,q)) = q |^ $1;
Funcs ({},q) = {{}}
by FUNCT_5:57;
then card (Funcs (0,q)) =
1
by CARD_1:30
.=
q #Z 0
by PREPOWER:34
.=
q |^ 0
by PREPOWER:36
;
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 12;
reconsider q9 =
q as non
empty set by A1;
defpred S2[
object ,
object ]
means ex
x being
Function of
(n + 1),
q st
( $1
= x & $2
= x | n );
A5:
for
x being
object st
x in Funcs (
(n + 1),
q9) holds
ex
y being
object st
(
y in Funcs (
n,
q9) &
S2[
x,
y] )
proof
let x be
object ;
( x in Funcs ((n + 1),q9) implies ex y being object st
( y in Funcs (n,q9) & S2[x,y] ) )
assume
x in Funcs (
(n + 1),
q9)
;
ex y being object 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:2;
not
n in n
;
then A9:
n misses {n}
by ZFMISC_1:50;
(Segm (n + 1)) /\ n = ((Segm n) \/ {n}) /\ n
by AFINSQ_1:2;
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:61;
rng (f | n) c= q9
;
then
f | n in Funcs (
n,
q9)
by A10, FUNCT_2:def 2;
hence
ex
y being
object 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
object st
x in Funcs (
(n + 1),
q9) holds
S2[
x,
G . x]
from FUNCT_2:sch 1(A5);
for
x being
object st
x in Funcs (
n,
q9) holds
x in rng G
proof
let x be
object ;
( x in Funcs (n,q9) implies x in rng G )
assume A12:
x in Funcs (
n,
q9)
;
x in rng G
consider y being
object 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}
;
then
dom f = (Segm n) \/ {n}
by A15, A16, FUNCT_4:def 1;
then A18:
dom f = Segm (n + 1)
by AFINSQ_1:2;
rng (n .--> y) = {y}
by FUNCOP_1:8;
then A19:
rng f c= (rng g) \/ {y}
by A15, FUNCT_4:17;
{y} c= q
by A14, ZFMISC_1:31;
then
(rng g) \/ {y} c= q
by XBOOLE_1:8;
then
rng f c= q
by A19;
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:66;
not
n in n
;
then
n misses {n}
by ZFMISC_1:50;
then A21:
f | n = g
by A15, A16, A17, FUNCT_4:33;
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 7;
verum
end;
then
g +* (n .--> y) in G " {g}
by A13;
then consider b being
object such that A23:
b in rng G
and A24:
[(g +* (n .--> y)),b] in G
and
b in {g}
by RELAT_1:131;
g +* (n .--> y) in dom G
by A24, FUNCT_1:1;
then
S2[
g +* (n .--> y),
G . (g +* (n .--> y))]
by A11;
then A25:
(g +* (n .--> y)) | n = b
by A24, FUNCT_1:1;
A26:
dom g = n
by FUNCT_2:def 1;
A27:
dom (n .--> y) = {n}
;
not
n in n
;
then
n misses {n}
by ZFMISC_1:50;
hence
x in rng G
by A23, A25, A26, A27, FUNCT_4:33;
verum
end;
then
Funcs (
n,
q9)
c= rng G
;
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(
object )
-> set =
x +* (n .--> $1);
A30:
for
y being
object st
y in q holds
H1(
y)
in G " {x}
proof
let y be
object ;
( 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}
;
then
dom f = (Segm n) \/ {n}
by A32, A33, FUNCT_4:def 1;
then A35:
dom f = Segm (n + 1)
by AFINSQ_1:2;
rng (n .--> y) = {y}
by FUNCOP_1:8;
then A36:
rng f c= (rng x) \/ {y}
by A32, FUNCT_4:17;
{y} c= q
by A31, ZFMISC_1:31;
then
(rng x) \/ {y} c= q
by XBOOLE_1:8;
then
rng f c= q
by A36;
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:66;
not
n in n
;
then
n misses {n}
by ZFMISC_1:50;
then A38:
f | n = x
by A32, A33, A34, FUNCT_4:33;
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 7;
verum
end;
consider H being
Function of
q,
(G " {x}) such that A40:
for
y being
object st
y in q holds
H . y = H1(
y)
from FUNCT_2:sch 2(A30);
A41:
for
c being
object st
c in G " {x} holds
ex
y being
object st
(
y in q &
H . y = c )
{x} c= rng G
by A28, ZFMISC_1:31;
then A48:
G " {x} <> {}
by RELAT_1:139;
A49:
rng H = G " {x}
by A41, FUNCT_2:10;
A50:
dom H = q
by A48, FUNCT_2:def 1;
for
x1,
x2 being
object st
x1 in dom H &
x2 in dom H &
H . x1 = H . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom H & x2 in dom H & H . x1 = H . x2 implies x1 = x2 )
assume that A51:
x1 in dom H
and A52:
x2 in dom H
and A53:
H . x1 = H . x2
;
x1 = x2
A54:
H . x2 = x +* (n .--> x2)
by A40, A52;
A55:
dom (n .--> x1) = {n}
;
A56:
dom (n .--> x2) = {n}
;
set fx1 =
x +* (n .--> x1);
set fx2 =
x +* (n .--> x2);
A57:
x +* (n .--> x1) = x +* (n .--> x2)
by A40, A51, A53, A54;
A58:
(n .--> x1) . n = x1
by FUNCOP_1:72;
A59:
(n .--> x2) . n = x2
by FUNCOP_1:72;
A60:
n in {n}
by TARSKI:def 1;
then
(x +* (n .--> x1)) . n = x1
by A55, A58, FUNCT_4:13;
hence
x1 = x2
by A56, A57, A59, A60, FUNCT_4:13;
verum
end;
then
H is
one-to-one
;
then
q,
H .: q are_equipotent
by A50, CARD_1:33;
then
q,
rng H are_equipotent
by A50, RELAT_1:113;
hence
(
G " {x} is
finite &
card (G " {x}) = q )
by A49, CARD_1:def 2;
verum
end;
A61:
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 A62:
x <> y
;
G " {x} misses G " {y}
now G " {x} misses G " {y}assume
not
G " {x} misses G " {y}
;
contradictionthen
not
(G " {x}) /\ (G " {y}) = {}
by XBOOLE_0:def 7;
then consider f being
object such that A63:
f in (G " {x}) /\ (G " {y})
by XBOOLE_0:def 1;
f in G " {x}
by A63, XBOOLE_0:def 4;
then A64:
G . f in {x}
by FUNCT_1:def 7;
reconsider f =
f as
Function of
(n + 1),
q by A63, FUNCT_2:66;
f in Funcs (
(n + 1),
q)
by A1, FUNCT_2:8;
then A65:
S2[
f,
G . f]
by A11;
then A66:
f | n = x
by A64, TARSKI:def 1;
f in G " {y}
by A63, XBOOLE_0:def 4;
then
G . f in {y}
by FUNCT_1:def 7;
hence
contradiction
by A62, A65, A66, 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 ;
A67:
for
y being
object st
y in union X holds
y in Funcs (
(n + 1),
q)
for
y being
object st
y in Funcs (
(n + 1),
q) holds
y in union X
proof
let x be
object ;
( 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 A70:
x = f
and A71:
G . x = f | n
by A11;
A72:
f in Funcs (
(n + 1),
q)
by A1, FUNCT_2:8;
then A73:
f in dom G
by FUNCT_2:def 1;
G . f in {(f | n)}
by A70, A71, TARSKI:def 1;
then A74:
f in G " {(f | n)}
by A73, FUNCT_1:def 7;
ex
y being
object st
(
y in Funcs (
n,
q9) &
S2[
f,
y] )
by A5, A72;
then
G " {(f | n)} in X
;
hence
x in union X
by A70, A74, TARSKI:def 4;
verum
end;
then A75:
union X = Funcs (
(n + 1),
q)
by A67, TARSKI:2;
Funcs (
(n + 1),
q) is
finite
by FRAENKEL:6;
then reconsider X =
X as
finite set by A75, FINSET_1:7;
A76:
card X = q |^ n
proof
deffunc H1(
object )
-> Element of
bool (Funcs ((n + 1),q9)) =
G " {$1};
A77:
for
x being
object st
x in Funcs (
n,
q) holds
H1(
x)
in X
;
consider F being
Function of
(Funcs (n,q)),
X such that A78:
for
x being
object st
x in Funcs (
n,
q) holds
F . x = H1(
x)
from FUNCT_2:sch 2(A77);
A79:
for
c being
object st
c in X holds
ex
x being
object st
(
x in Funcs (
n,
q) &
c = F . x )
set gg = the
Element of
Funcs (
n,
q9);
A81:
G " { the Element of Funcs (n,q9)} in X
;
A82:
rng F = X
by A79, FUNCT_2:10;
A83:
dom F = Funcs (
n,
q)
by A81, FUNCT_2:def 1;
for
x1,
x2 being
object st
x1 in dom F &
x2 in dom F &
F . x1 = F . x2 holds
x1 = x2
then
F is
one-to-one
;
then
Funcs (
n,
q),
F .: (Funcs (n,q)) are_equipotent
by A83, CARD_1:33;
then
Funcs (
n,
q),
rng F are_equipotent
by A83, RELAT_1:113;
hence
card X = q |^ n
by A4, A82, CARD_1:5;
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:156;
hence
S1[
n + 1]
by A75, A76, NEWTON:6;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A2, A3);
hence
card (Funcs (n,q)) = q |^ n
; verum