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_{1}[ 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_{1}[ 0 ]
;

A3: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A2, A3);

hence card (Funcs (n,q)) = q |^ n ; :: thesis: verum

assume A1: 0 < q ; :: thesis: card (Funcs (n,q)) = q |^ n

reconsider q = q as Element of NAT by ORDINAL1:def 12;

defpred S

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

A3: for n being Nat st S

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A4: S_{1}[n]
; :: thesis: S_{1}[n + 1]

reconsider n = n as Element of NAT by ORDINAL1:def 12;

reconsider q9 = q as non empty set by A1;

defpred S_{2}[ 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_{2}[x,y] )

A11: for x being object st x in Funcs ((n + 1),q9) holds

S_{2}[x,G . x]
from FUNCT_2:sch 1(A5);

for x being object st x in Funcs (n,q9) holds

x in 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 )

G " {x} misses G " {y}

A67: for y being object st y in union X holds

y in Funcs ((n + 1),q)

y in union X

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

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

( C = union X & card C = q * (card X) ) by GROUP_2:156;

hence S_{1}[n + 1]
by A75, A76, NEWTON:6; :: thesis: verum

end;assume A4: S

reconsider n = n as Element of NAT by ORDINAL1:def 12;

reconsider q9 = q as non empty set by A1;

defpred S

( $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

proof

consider G being Function of (Funcs ((n + 1),q9)),(Funcs (n,q9)) such that
let x be object ; :: thesis: ( x in Funcs ((n + 1),q9) implies ex y being object st

( y in Funcs (n,q9) & S_{2}[x,y] ) )

assume x in Funcs ((n + 1),q9) ; :: thesis: ex y being object st

( y in Funcs (n,q9) & S_{2}[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_{2}[x,y] )
by A6; :: thesis: verum

end;( y in Funcs (n,q9) & S

assume x in Funcs ((n + 1),q9) ; :: thesis: ex y being object st

( y in Funcs (n,q9) & S

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

A11: for x being object st x in Funcs ((n + 1),q9) holds

S

for x being object st x in Funcs (n,q9) holds

x in rng G

proof

then
Funcs (n,q9) c= rng G
;
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}

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_{2}[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;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

then
g +* (n .--> y) in G " {g}
by A13;
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_{2}[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;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

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

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

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

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

A61:
for x, y being set st x is Element of Funcs (n,q9) & y is Element of Funcs (n,q9) & x <> y holds
let x be Element of Funcs (n,q9); :: thesis: ( G " {x} is finite & card (G " {x}) = q )

deffunc H_{1}( object ) -> set = x +* (n .--> $1);

A30: for y being object st y in q holds

H_{1}(y) in G " {x}

A40: for y being object st y in q holds

H . y = H_{1}(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 )

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

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;deffunc H

A30: for y being object st y in q holds

H

proof

consider H being Function of q,(G " {x}) such that
let y be object ; :: thesis: ( y in q implies H_{1}(y) in G " {x} )

assume A31: y in q ; :: thesis: H_{1}(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_{2}[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_{1}(y) in G " {x}
by A32, A37, A39, FUNCT_1:def 7; :: thesis: verum

end;assume A31: y in q ; :: thesis: H

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

then A39: G . f in {x} by A38, TARSKI:def 1;

dom G = Funcs ((n + 1),q) by FUNCT_2:def 1;

hence H

A40: for y being object st y in q holds

H . y = H

A41: for c being object st c in G " {x} holds

ex y being object st

( y in q & H . y = c )

proof

{x} c= rng G
by A28, ZFMISC_1:31;
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;( 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

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

then
H is one-to-one
;
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;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

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

G " {x} misses G " {y}

proof

reconsider X = { (G " {x}) where x is Element of Funcs (n,q9) : verum } as set ;
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}

end;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}

hence
G " {x} misses G " {y}
; :: thesis: verumassume
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_{2}[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;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

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

A67: for y being object st y in union X holds

y in Funcs ((n + 1),q)

proof

for y being object st y in Funcs ((n + 1),q) holds
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;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

y in union X

proof

then A75:
union X = Funcs ((n + 1),q)
by A67, TARSKI:2;
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_{2}[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;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

then G " {(f | n)} in X ;

hence x in union X by A70, A74, TARSKI:def 4; :: thesis: verum

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

for Y being set st Y in X holds
deffunc H_{1}( object ) -> Element of bool (Funcs ((n + 1),q9)) = G " {$1};

A77: for x being object st x in Funcs (n,q) holds

H_{1}(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_{1}(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 )

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 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;A77: for x being object st x in Funcs (n,q) holds

H

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

A79: for c being object st c in X holds

ex x being object st

( x in Funcs (n,q) & c = F . x )

proof

set gg = the Element of Funcs (n,q9);
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;( 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

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

then
F is one-to-one
;
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;

end;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

hence
x1 = x2
; :: thesis: verumassume
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;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

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

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

then
ex C being finite set st
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 )

( 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;( 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

hence
ex B being finite set st
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;

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

end;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;

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

( 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

( C = union X & card C = q * (card X) ) by GROUP_2:156;

hence S

hence card (Funcs (n,q)) = q |^ n ; :: thesis: verum