let Y, X be finite set ; :: thesis: ( ( Y = {} implies X = {} ) implies card (Funcs X,Y) = (card Y) |^ (card X) )
assume A1:
( Y = {} implies X = {} )
; :: thesis: card (Funcs X,Y) = (card Y) |^ (card X)
per cases
( Y is empty or not Y is empty )
;
suppose A2:
not
Y is
empty
;
:: thesis: card (Funcs X,Y) = (card Y) |^ (card X)defpred S1[
Element of
NAT ]
means for
X,
Y being
finite set st not
Y is
empty &
card X = $1 holds
card (Funcs X,Y) = (card Y) |^ (card X);
A3:
S1[
0 ]
A5:
for
n being
Element of
NAT st
S1[
n] holds
S1[
n + 1]
proof
let n be
Element of
NAT ;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A6:
S1[
n]
;
:: thesis: S1[n + 1]
let X,
Y be
finite set ;
:: thesis: ( not Y is empty & card X = n + 1 implies card (Funcs X,Y) = (card Y) |^ (card X) )
assume that A7:
not
Y is
empty
and A8:
card X = n + 1
;
:: thesis: card (Funcs X,Y) = (card Y) |^ (card X)
card Y,
Y are_equipotent
by CARD_1:def 5;
then consider f being
Function such that A9:
(
f is
one-to-one &
dom f = card Y &
rng f = Y )
by WELLORD2:def 4;
reconsider f =
f as
Function of
(card Y),
Y by A9, FUNCT_2:3;
A10:
(
f is
onto &
f is
one-to-one )
by A9, FUNCT_2:def 3;
consider x being
set such that A11:
x in X
by A8, CARD_1:47, XBOOLE_0:def 1;
defpred S2[
set ]
means 1
= 1;
consider F being
XFinSequence of
such that A12:
dom F = card Y
and A13:
card { g where g is Function of X,Y : S2[g] } = Sum F
and A14:
for
k being
Element of
NAT st
k in dom F holds
F . k = card { g where g is Function of X,Y : ( S2[g] & g . x = f . k ) }
from STIRL2_1:sch 8(A10, A7, A11);
set F1 =
{ g where g is Function of X,Y : S2[g] } ;
A15:
{ g where g is Function of X,Y : S2[g] } c= Funcs X,
Y
Funcs X,
Y c= { g where g is Function of X,Y : S2[g] }
then A18:
Funcs X,
Y = { g where g is Function of X,Y : S2[g] }
by A15, XBOOLE_0:def 10;
reconsider cY =
(card Y) |^ n as
Element of
NAT ;
for
k being
Element of
NAT st
k in dom F holds
F . k = cY
proof
let k be
Element of
NAT ;
:: thesis: ( k in dom F implies F . k = cY )
assume A19:
k in dom F
;
:: thesis: F . k = cY
set Xx =
X \ {x};
set F2 =
{ g where g is Function of ((X \ {x}) \/ {x}),Y : g . x = f . k } ;
set F3 =
{ g where g is Function of X,Y : ( S2[g] & g . x = f . k ) } ;
A20:
{ g where g is Function of ((X \ {x}) \/ {x}),Y : g . x = f . k } c= { g where g is Function of X,Y : ( S2[g] & g . x = f . k ) }
{ g where g is Function of X,Y : ( S2[g] & g . x = f . k ) } c= { g where g is Function of ((X \ {x}) \/ {x}),Y : g . x = f . k }
then A23:
{ g where g is Function of ((X \ {x}) \/ {x}),Y : g . x = f . k } = { g where g is Function of X,Y : ( S2[g] & g . x = f . k ) }
by A20, XBOOLE_0:def 10;
(
x in {x} &
f . k in rng f )
by A9, A12, A19, FUNCT_1:def 5, TARSKI:def 1;
then
( not
x in X \ {x} &
f . k in Y &
card (X \ {x}) = n )
by A8, A11, STIRL2_1:65, XBOOLE_0:def 5;
then
(
card (Funcs (X \ {x}),Y) = card { g where g is Function of ((X \ {x}) \/ {x}),Y : g . x = f . k } &
card (Funcs (X \ {x}),Y) = cY )
by A6, Th3;
hence
F . k = cY
by A14, A19, A23;
:: thesis: verum
end;
then
( ( for
k being
Element of
NAT st
k in dom F holds
F . k <= cY ) & ( for
k being
Element of
NAT st
k in dom F holds
F . k >= cY ) )
;
then
(
Sum F <= (len F) * ((card Y) |^ n) &
Sum F >= (len F) * ((card Y) |^ n) &
dom F = len F )
by STIRL2_1:50, STIRL2_1:51;
then
Sum F = (card Y) * ((card Y) |^ n)
by A12, XXREAL_0:1;
hence
card (Funcs X,Y) = (card Y) |^ (card X)
by A8, A13, A18, NEWTON:11;
:: thesis: verum
end;
for
n being
Element of
NAT holds
S1[
n]
from NAT_1:sch 1(A3, A5);
hence
card (Funcs X,Y) = (card Y) |^ (card X)
by A2;
:: thesis: verum end;