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