let X, Y be finite set ; :: thesis: ( 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[ Element of 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:
S1[ 0 ]
A7:
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 A8:
S1[
n]
;
:: thesis: S1[n + 1]
let X,
Y be
finite set ;
:: thesis: ( 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 A9:
(
card Y = n + 1 &
card X <= card Y )
;
:: thesis: 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
not
X is
empty
;
:: thesis: 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 A15:
x in X
by XBOOLE_0:def 1;
card Y,
Y are_equipotent
by CARD_1:def 5;
then consider f being
Function such that A16:
(
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 A16, FUNCT_2:3;
A17:
(
f is
onto &
f is
one-to-one )
by A16, FUNCT_2:def 3;
A18:
not
Y is
empty
by A9;
defpred S2[
Function]
means $1 is
one-to-one ;
consider F being
XFinSequence of
such that A19:
dom F = card Y
and A20:
card { g where g is Function of X,Y : S2[g] } = Sum F
and A21:
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(A17, A18, A15);
not
card X is
empty
by A15;
then
(card Y) -' (card X) < n + 1
by A9, NAT_2:11;
then
(card Y) -' (card X) <= n
by NAT_1:13;
then A22:
(
(n ! ) / (((card Y) -' (card X)) ! ) is
integer &
(n ! ) / (((card Y) -' (card X)) ! ) > 0 )
by IRRAT_1:34, IRRAT_1:37;
for
k being
Element of
NAT st
k in dom F holds
F . k = (n ! ) / (((card Y) -' (card X)) ! )
proof
let k be
Element of
NAT ;
:: thesis: ( k in dom F implies F . k = (n ! ) / (((card Y) -' (card X)) ! ) )
assume A23:
k in dom F
;
:: thesis: F . k = (n ! ) / (((card Y) -' (card X)) ! )
A24:
f . k in Y
by A16, A19, A23, FUNCT_1:def 5;
set Xx =
X \ {x};
set Yy =
Y \ {(f . k)};
card X <> 0
by A15;
then
card X > 0
;
then reconsider cX1 =
(card X) - 1 as
Element of
NAT by NAT_1:20;
cX1 + 1
<= n + 1
by A9;
then A25:
(
(cX1 + 1) - 1
<= (n + 1) - 1 &
card (X \ {x}) = cX1 &
card (Y \ {(f . k)}) = n )
by A9, A15, A24, STIRL2_1:65, XREAL_1:11;
then A26:
(
n - cX1 >= cX1 - cX1 &
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 A8, XREAL_1:11;
(card Y) - (card X) >= (card X) - (card X)
by A9, XREAL_1:11;
then A27:
(card Y) -' (card X) =
(((card (Y \ {(f . k)})) + 1) - 1) - (((card (X \ {x})) + 1) - 1)
by A9, A25, XREAL_0:def 2
.=
(card (Y \ {(f . k)})) -' (card (X \ {x}))
by A25, A26, XREAL_0:def 2
;
A28:
(
Y \ {(f . k)} is
empty implies
X \ {x} is
empty )
by A25, CARD_1:47;
(
f . k in {(f . k)} &
x in {x} )
by TARSKI:def 1;
then
(
Y = (Y \ {(f . k)}) \/ {(f . k)} &
X = (X \ {x}) \/ {x} & not
f . k in Y \ {(f . k)} & not
x in X \ {x} & (
Y \ {(f . k)} is
empty implies
X \ {x} is
empty ) )
by A15, A24, A28, XBOOLE_0:def 5, ZFMISC_1:140;
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 A26, A27, Th5;
hence
F . k = (n ! ) / (((card Y) -' (card X)) ! )
by A21, A23;
:: thesis: verum
end; then
( ( for
k being
Element of
NAT st
k in dom F holds
F . k >= (n ! ) / (((card Y) -' (card X)) ! ) ) & ( for
k being
Element of
NAT st
k in dom F holds
F . k <= (n ! ) / (((card Y) -' (card X)) ! ) ) &
(n ! ) / (((card Y) -' (card X)) ! ) is
Element of
NAT )
by A22, INT_1:16;
then
(
Sum F <= (len F) * ((n ! ) / (((card Y) -' (card X)) ! )) &
Sum F >= (len F) * ((n ! ) / (((card Y) -' (card X)) ! )) &
dom F = len F )
by STIRL2_1:50, STIRL2_1:51;
then Sum F =
(n + 1) * ((n ! ) / (((card Y) -' (card X)) ! ))
by A9, A19, XXREAL_0:1
.=
((n + 1) * (n ! )) / (((card Y) -' (card X)) ! )
by XCMPLX_1:75
.=
((card Y) ! ) / (((card Y) -' (card X)) ! )
by A9, NEWTON:21
;
hence
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) ! ) / (((card Y) -' (card X)) ! )
by A20;
:: thesis: verum end;
end;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A1, A7);
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)) ! ) )
; :: thesis: verum