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: Y is empty ; :: thesis: card (Funcs (X,Y)) = (card Y) |^ (card X)
then card (Funcs (X,Y)) = 1 by A1, ALTCAT_1:2, CARD_1:30;
hence card (Funcs (X,Y)) = (card Y) |^ (card X) by A1, A2, CARD_1:27, NEWTON:4; :: thesis: verum
end;
suppose A3: not Y is empty ; :: thesis: card (Funcs (X,Y)) = (card Y) |^ (card X)
defpred S1[ 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);
A4: for n being Nat st S1[n] holds
S1[n + 1]
proof
defpred S2[ set ] means 1 = 1;
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A5: 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
A6: not Y is empty and
A7: card X = n + 1 ; :: thesis: card (Funcs (X,Y)) = (card Y) |^ (card X)
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
reconsider cY = (card Y) |^ nn as Element of NAT ;
card Y,Y are_equipotent by CARD_1:def 2;
then consider f being Function such that
A8: f is one-to-one and
A9: dom f = card Y and
A10: rng f = Y by WELLORD2:def 4;
reconsider f = f as Function of (card Y),Y by A9, A10, FUNCT_2:1;
consider x being set such that
A11: x in X by A7, CARD_1:27, XBOOLE_0:def 1;
A12: ( f is onto & f is one-to-one ) by A8, A10, FUNCT_2:def 3;
consider F being XFinSequence of such that
A13: dom F = card Y and
A14: card { g where g is Function of X,Y : S2[g] } = Sum F and
A15: 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(A12, A6, A11);
 A16: for k being Nat st k in dom F holds
F . k = cY
proof
set Xx = X \ {x};
let k be Nat; :: thesis: ( k in dom F implies F . k = cY )
assume A17: k in dom F ; :: thesis: F . k = cY
A18: f . k in rng f by A9, A13, A17, FUNCT_1:def 3;
set F3 = { g where g is Function of X,Y : ( S2[g] & g . x = f . k ) } ;
set F2 = { g where g is Function of ((X \ {x}) \/ {x}),Y : g . x = f . k } ;
A19: { 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 }
proof
let G be set ; :: according to TARSKI:def 3 :: thesis: ( not G in { g where g is Function of X,Y : ( S2[g] & g . x = f . k ) } or G in { g where g is Function of ((X \ {x}) \/ {x}),Y : g . x = f . k } )
assume G in { g where g is Function of X,Y : ( S2[g] & g . x = f . k ) } ; :: thesis: G in { g where g is Function of ((X \ {x}) \/ {x}),Y : g . x = f . k }
then A20: ex g being Function of X,Y st
( g = G & S2[g] & g . x = f . k ) ;
(X \ {x}) \/ {x} = X by A11, ZFMISC_1:116;
hence G in { g where g is Function of ((X \ {x}) \/ {x}),Y : g . x = f . k } by A20; :: thesis: verum
end;
{ 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 ) }
proof
let G be set ; :: according to TARSKI:def 3 :: thesis: ( not G in { g where g is Function of ((X \ {x}) \/ {x}),Y : g . x = f . k } or G in { g where g is Function of X,Y : ( S2[g] & g . x = f . k ) } )
assume G in { g where g is Function of ((X \ {x}) \/ {x}),Y : g . x = f . k } ; :: thesis: G in { g where g is Function of X,Y : ( S2[g] & g . x = f . k ) }
then A21: ex g being Function of ((X \ {x}) \/ {x}),Y st
( g = G & g . x = f . k ) ;
(X \ {x}) \/ {x} = X by A11, ZFMISC_1:116;
hence G in { g where g is Function of X,Y : ( S2[g] & g . x = f . k ) } by A21; :: thesis: verum
end;
then A22: { 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 A19, XBOOLE_0:def 10;
card (X \ {x}) = n by A7, A11, STIRL2_1:55;
then A23: card (Funcs ((X \ {x}),Y)) = cY by A5, A18;
x in {x} by TARSKI:def 1;
then not x in X \ {x} by 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 } by A18, Th3;
hence F . k = cY by A15, A17, A22, A23; :: thesis: verum
end;
then for k being Nat st k in dom F holds
F . k >= cY ;
then A24: Sum F >= (len F) * ((card Y) |^ n) by AFINSQ_2:60;
set F1 = { g where g is Function of X,Y : S2[g] } ;
A25: Funcs (X,Y) c= { g where g is Function of X,Y : S2[g] }
proof
let G be set ; :: according to TARSKI:def 3 :: thesis: ( not G in Funcs (X,Y) or G in { g where g is Function of X,Y : S2[g] } )
assume G in Funcs (X,Y) ; :: thesis: G in { g where g is Function of X,Y : S2[g] }
then G is Function of X,Y by FUNCT_2:66;
hence G in { g where g is Function of X,Y : S2[g] } ; :: thesis: verum
end;
{ g where g is Function of X,Y : S2[g] } c= Funcs (X,Y)
proof
let G be set ; :: according to TARSKI:def 3 :: thesis: ( not G in { g where g is Function of X,Y : S2[g] } or G in Funcs (X,Y) )
assume G in { g where g is Function of X,Y : S2[g] } ; :: thesis: G in Funcs (X,Y)
then ex g being Function of X,Y st
( g = G & S2[g] ) ;
hence G in Funcs (X,Y) by A6, FUNCT_2:8; :: thesis: verum
end;
then A26: Funcs (X,Y) = { g where g is Function of X,Y : S2[g] } by A25, XBOOLE_0:def 10;
for k being Nat st k in dom F holds
F . k <= cY by A16;
then Sum F <= (len F) * ((card Y) |^ n) by AFINSQ_2:59;
then Sum F = (card Y) * ((card Y) |^ n) by A13, A24, XXREAL_0:1;
hence card (Funcs (X,Y)) = (card Y) |^ (card X) by A7, A14, A26, NEWTON:6; :: thesis: verum
end;
A27: S1[ 0 ]
proof
let X, Y be finite set ; :: thesis: ( not Y is empty & card X = 0 implies card (Funcs (X,Y)) = (card Y) |^ (card X) )
assume that
not Y is empty and
A28: card X = 0 ; :: thesis: card (Funcs (X,Y)) = (card Y) |^ (card X)
X is empty by A28;
then Funcs (X,Y) = {{}} by FUNCT_5:57;
then card (Funcs (X,Y)) = 1 by CARD_1:30;
hence card (Funcs (X,Y)) = (card Y) |^ (card X) by A28, NEWTON:4; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A27, A4);
hence card (Funcs (X,Y)) = (card Y) |^ (card X) by A3; :: thesis: verum
end;
end;