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 12;
defpred S₁[ 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: S₁[ 0 ] ;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
reconsider n = n as Element of NAT by ORDINAL1:def 12;
reconsider q9 = q as non empty set by A1;
defpred S₂[ 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) & S₂[x,y] )

proof

let x be object ; :: thesis: ( x in Funcs ((n + 1),q9) implies ex y being object st
( y in Funcs (n,q9) & S₂[x,y] ) )
assume x in Funcs ((n + 1),q9) ; :: thesis: ex y being object st
( y in Funcs (n,q9) & S₂[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) & S₂[x,y] ) by A6; :: thesis: 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
S₂[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 ; :: thesis: ( x in Funcs (n,q9) implies x in rng G )
assume A12: x in Funcs (n,q9) ; :: thesis: 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 ; :: thesis: ( y in q implies g +* (n .--> y) in G " {g} )
assume A14: y in q ; :: thesis: 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;
S₂[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; :: thesis: 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 S₂[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; :: thesis: 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); :: thesis: ( G " {x} is finite & card (G " {x}) = q )
deffunc H₁( object ) -> set = x +* (n .--> $1);
A30: for y being object st y in q holds
H₁(y) in G " {x}

proof

let y be object ; :: thesis: ( y in q implies H₁(y) in G " {x} )
assume A31: y in q ; :: thesis: H₁(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;
S₂[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 H₁(y) in G " {x} by A32, A37, A39, FUNCT_1:def 7; :: thesis: verum

end;

consider H being Function of q,(G " {x}) such that
A40: for y being object st y in q holds
H . y = H₁(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 )

proof

let c be object ; :: thesis: ( c in G " {x} implies ex y being object st
( y in q & H . y = c ) )
assume A42: c in G " {x} ; :: thesis: ex y being object st
( y in q & H . y = c )
then consider f being Function of (n + 1),q9 such that
A43: c = f and
A44: G . c = f | n by A11;
take y = f . n; :: thesis: ( y in q & H . y = c )
G . c in {x} by A42, FUNCT_1:def 7;
then A45: G . c = x by TARSKI:def 1;
Segm (n + 1) = (Segm n) \/ {n} by AFINSQ_1:2;
then dom f = n \/ {n} by FUNCT_2:def 1;
then A46: f = (f | n) +* (n .--> (f . n)) by FUNCT_7:14;
A47: n in Segm (n + 1) by NAT_1:45;
hence y in q by FUNCT_2:5; :: thesis: H . y = c
thus H . y = c by A40, A43, A44, A45, A46, A47, FUNCT_2:5; :: thesis: verum

end;

{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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: G " {x} misses G " {y}

now :: thesis: G " {x} misses G " {y}

assume not G " {x} misses G " {y} ; :: thesis: contradiction
then 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: S₂[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; :: thesis: verum

end;

hence G " {x} misses G " {y} ; :: thesis: 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)

proof

let x be object ; :: thesis: ( x in union X implies x in Funcs ((n + 1),q) )
assume x in union X ; :: thesis: x in Funcs ((n + 1),q)
then consider Y being set such that
A68: x in Y and
A69: Y in X by TARSKI:def 4;
ex z being Element of Funcs (n,q) st G " {z} = Y by A69;
hence x in Funcs ((n + 1),q) by A68; :: thesis: verum

end;

for y being object st y in Funcs ((n + 1),q) holds
y in union X

proof

let x be object ; :: thesis: ( x in Funcs ((n + 1),q) implies x in union X )
assume x in Funcs ((n + 1),q) ; :: thesis: 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) & S₂[f,y] ) by A5, A72;
then G " {(f | n)} in X ;
hence x in union X by A70, A74, TARSKI:def 4; :: thesis: 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 H₁( object ) -> Element of bool (Funcs ((n + 1),q9)) = G " {$1};
A77: for x being object st x in Funcs (n,q) holds
H₁(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 = H₁(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 )

proof

let c be object ; :: thesis: ( c in X implies ex x being object st
( x in Funcs (n,q) & c = F . x ) )
assume c in X ; :: thesis: ex x being object st
( x in Funcs (n,q) & c = F . x )
then consider y being Element of Funcs (n,q) such that
A80: c = G " {y} ;
F . y = c by A78, A80;
hence ex x being object st
( x in Funcs (n,q) & c = F . x ) ; :: thesis: verum

end;

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

proof

let x1, x2 be object ; :: thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )
assume that
A84: x1 in dom F and
A85: x2 in dom F and
A86: F . x1 = F . x2 ; :: thesis: x1 = x2
F . x1 = G " {x1} by A78, A84;
then A87: G " {x1} = G " {x2} by A78, A85, A86;

now :: thesis: not x1 <> x2

assume x1 <> x2 ; :: thesis: contradiction
then G " {x1} misses G " {x2} by A61, A84, A85;
then (G " {x1}) /\ (G " {x1}) = {} by A87, XBOOLE_0:def 7;
hence contradiction by A29, A84, CARD_1:27; :: thesis: verum

end;

hence x1 = x2 ; :: thesis: verum

end;

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; :: 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 ) ) )

proof

let Y be set ; :: thesis: ( Y in X implies 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 ) ) ) )
assume Y in X ; :: thesis: 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 consider x being Element of Funcs (n,q9) such that
A88: Y = G " {x} ;
A89: Y is finite by A29, A88;
A90: card Y = q by A29, A88;
for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z )

proof

let Z be set ; :: thesis: ( Z in X & Y <> Z implies ( Y,Z are_equipotent & Y misses Z ) )
assume that
A91: Z in X and
A92: Y <> Z ; :: thesis: ( Y,Z are_equipotent & Y misses Z )
consider y being Element of Funcs (n,q9) such that
A93: Z = G " {y} by A91;
A94: card Z = q by A29, A93;

now :: thesis: Y misses Z

per cases ( x = y or x <> y ) ;

suppose x = y ; :: thesis: Y misses Z

hence Y misses Z by A88, A92, A93; :: thesis: verum

end;

suppose x <> y ; :: thesis: Y misses Z

hence Y misses Z by A61, A88, A93; :: thesis: verum

end;

end;

end;

hence ( Y,Z are_equipotent & Y misses Z ) by A90, A94, CARD_1:5; :: thesis: verum

end;

hence 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 ) ) ) by A89, A90; :: thesis: verum

end;

then ex C being finite set st
( C = union X & card C = q * (card X) ) by GROUP_2:156;
hence S₁[n + 1] by A75, A76, NEWTON:6; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence card (Funcs (n,q)) = q |^ n ; :: thesis: verum