let X, Y be finite set ; ( card X <= card Y implies card { F where F is Function of X,Y : F is one-to-one } = ((card Y) !) / (((card Y) -' (card X)) !) )
defpred S1[ Nat] means for X, Y being finite set st card Y = $1 & card X <= card Y holds
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) !) / (((card Y) -' (card X)) !);
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
let X,
Y be
finite set ;
( card Y = n + 1 & card X <= card Y implies card { F where F is Function of X,Y : F is one-to-one } = ((card Y) !) / (((card Y) -' (card X)) !) )
assume that A3:
card Y = n + 1
and A4:
card X <= card Y
;
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) !) / (((card Y) -' (card X)) !)
per cases
( X is empty or not X is empty )
;
suppose A5:
X is
empty
;
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) !) / (((card Y) -' (card X)) !)set F1 =
{ F where F is Function of X,Y : F is one-to-one } ;
A6:
{ F where F is Function of X,Y : F is one-to-one } c= {{}}
A7:
rng {} c= Y
by XBOOLE_1:2;
(card Y) - (card X) = card Y
by A5, CARD_1:27;
then A8:
((card Y) -' (card X)) ! = (card Y) !
by XREAL_0:def 2;
(card Y) ! > 0
by NEWTON:17;
then A9:
((card Y) !) / (((card Y) -' (card X)) !) = 1
by A8, XCMPLX_1:60;
dom {} = X
by A5;
then
{} is
Function of
X,
Y
by A7, FUNCT_2:2;
then
{} in { F where F is Function of X,Y : F is one-to-one }
;
then
{ F where F is Function of X,Y : F is one-to-one } = {{}}
by A6, ZFMISC_1:33;
hence
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) !) / (((card Y) -' (card X)) !)
by A9, CARD_1:30;
verum end; suppose
not
X is
empty
;
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) !) / (((card Y) -' (card X)) !)then consider x being
set such that A10:
x in X
by XBOOLE_0:def 1;
defpred S2[
Function]
means $1 is
one-to-one ;
card Y,
Y are_equipotent
by CARD_1:def 2;
then consider f being
Function such that A11:
f is
one-to-one
and A12:
dom f = card Y
and A13:
rng f = Y
by WELLORD2:def 4;
reconsider f =
f as
Function of
(card Y),
Y by A12, A13, FUNCT_2:1;
A14:
not
Y is
empty
by A3;
A15:
(
f is
onto &
f is
one-to-one )
by A11, A13, FUNCT_2:def 3;
consider F being
XFinSequence of
such that A16:
dom F = card Y
and A17:
card { g where g is Function of X,Y : S2[g] } = Sum F
and A18:
for
k being
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 6(A15, A14, A10);
A19:
for
k being
Nat st
k in dom F holds
F . k = (n !) / (((card Y) -' (card X)) !)
proof
card X > 0
by A10;
then reconsider cX1 =
(card X) - 1 as
Element of
NAT by NAT_1:20;
set Xx =
X \ {x};
x in {x}
by TARSKI:def 1;
then A20:
not
x in X \ {x}
by XBOOLE_0:def 5;
A21:
X = (X \ {x}) \/ {x}
by A10, ZFMISC_1:116;
A22:
(cX1 + 1) - 1
<= (n + 1) - 1
by A3, A4, XREAL_1:9;
then A23:
n - cX1 >= cX1 - cX1
by XREAL_1:9;
let k be
Nat;
( k in dom F implies F . k = (n !) / (((card Y) -' (card X)) !) )
assume A24:
k in dom F
;
F . k = (n !) / (((card Y) -' (card X)) !)
A25:
f . k in Y
by A12, A13, A16, A24, FUNCT_1:def 3;
set Yy =
Y \ {(f . k)};
A26:
Y = (Y \ {(f . k)}) \/ {(f . k)}
by A25, ZFMISC_1:116;
f . k in {(f . k)}
by TARSKI:def 1;
then A27:
not
f . k in Y \ {(f . k)}
by XBOOLE_0:def 5;
cX1 + 1
<= n + 1
by A3, A4;
then A28:
card (X \ {x}) = cX1
by A10, STIRL2_1:55;
A29:
card (Y \ {(f . k)}) = n
by A3, A25, STIRL2_1:55;
then A30:
(
Y \ {(f . k)} is
empty implies
X \ {x} is
empty )
by A22, A28, CARD_1:27;
A31:
card { g where g is Function of (X \ {x}),(Y \ {(f . k)}) : g is one-to-one } = (n !) / (((card (Y \ {(f . k)})) -' (card (X \ {x}))) !)
by A2, A22, A28, A29;
(card Y) - (card X) >= (card X) - (card X)
by A4, XREAL_1:9;
then (card Y) -' (card X) =
(((card (Y \ {(f . k)})) + 1) - 1) - (((card (X \ {x})) + 1) - 1)
by A3, A28, A29, XREAL_0:def 2
.=
(card (Y \ {(f . k)})) -' (card (X \ {x}))
by A28, A29, A23, XREAL_0:def 2
;
then
card { g where g is Function of X,Y : ( g is one-to-one & g . x = f . k ) } = (n !) / (((card Y) -' (card X)) !)
by A31, A26, A21, A27, A20, A30, Th5;
hence
F . k = (n !) / (((card Y) -' (card X)) !)
by A18, A24;
verum
end; then
for
k being
Nat st
k in dom F holds
F . k >= (n !) / (((card Y) -' (card X)) !)
;
then A32:
Sum F >= (len F) * ((n !) / (((card Y) -' (card X)) !))
by AFINSQ_2:60;
for
k being
Nat st
k in dom F holds
F . k <= (n !) / (((card Y) -' (card X)) !)
by A19;
then
Sum F <= (len F) * ((n !) / (((card Y) -' (card X)) !))
by AFINSQ_2:59;
then Sum F =
(n + 1) * ((n !) / (((card Y) -' (card X)) !))
by A3, A16, A32, XXREAL_0:1
.=
((n + 1) * (n !)) / (((card Y) -' (card X)) !)
by XCMPLX_1:74
.=
((card Y) !) / (((card Y) -' (card X)) !)
by A3, NEWTON:15
;
hence
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) !) / (((card Y) -' (card X)) !)
by A17;
verum end;
end;
A33:
S1[ 0 ]
proof
let X,
Y be
finite set ;
( card Y = 0 & card X <= card Y implies card { F where F is Function of X,Y : F is one-to-one } = ((card Y) !) / (((card Y) -' (card X)) !) )
assume that A34:
card Y = 0
and A35:
card X <= card Y
;
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) !) / (((card Y) -' (card X)) !)
(card Y) - (card X) = 0
by A34, A35;
then A36:
((card Y) -' (card X)) ! = 1
by NEWTON:12, XREAL_0:def 2;
set F1 =
{ F where F is Function of X,Y : F is one-to-one } ;
A37:
{ F where F is Function of X,Y : F is one-to-one } c= {{}}
(
dom {} = X &
rng {} = Y )
by A34, A35;
then
{} is
Function of
X,
Y
by FUNCT_2:1;
then
{} in { F where F is Function of X,Y : F is one-to-one }
;
then
{ F where F is Function of X,Y : F is one-to-one } = {{}}
by A37, ZFMISC_1:33;
hence
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) !) / (((card Y) -' (card X)) !)
by A34, A36, CARD_1:30, NEWTON:12;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A33, A1);
hence
( card X <= card Y implies card { F where F is Function of X,Y : F is one-to-one } = ((card Y) !) / (((card Y) -' (card X)) !) )
; verum