let X, Y be finite set ; :: thesis: for x, y being set st not x in X & y in Y holds
card (Funcs X,Y) = card { F where F is Function of (X \/ {x}),Y : F . x = y }
let x, y be set ; :: thesis: ( not x in X & y in Y implies card (Funcs X,Y) = card { F where F is Function of (X \/ {x}),Y : F . x = y } )
assume A1: ( not x in X & y in Y ) ; :: thesis: card (Funcs X,Y) = card { F where F is Function of (X \/ {x}),Y : F . x = y }
set F1 = { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) } ;
set F2 = { F where F is Function of (X \/ {x}),Y : F . x = y } ;
{y} c= Y by A1, ZFMISC_1:37;
then A2: Y = Y \/ {y} by XBOOLE_1:12;
A3: { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) } c= { F where F is Function of (X \/ {x}),Y : F . x = y }

proof

let f be set ; :: according to TARSKI:def 3 :: thesis: ( not f in { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) } or f in { F where F is Function of (X \/ {x}),Y : F . x = y } )
assume A4: f in { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) } ; :: thesis: f in { F where F is Function of (X \/ {x}),Y : F . x = y }
ex F being Function of (X \/ {x}),(Y \/ {y}) st
( f = F & rng (F | X) c= Y & F . x = y ) by A4;
hence f in { F where F is Function of (X \/ {x}),Y : F . x = y } by A2; :: thesis: verum

end;

{ F where F is Function of (X \/ {x}),Y : F . x = y } c= { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) }

proof

let f be set ; :: according to TARSKI:def 3 :: thesis: ( not f in { F where F is Function of (X \/ {x}),Y : F . x = y } or f in { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) } )
assume A5: f in { F where F is Function of (X \/ {x}),Y : F . x = y } ; :: thesis: f in { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) }
consider F being Function of (X \/ {x}),Y such that
A6: ( f = F & F . x = y ) by A5;
rng (F | X) c= Y ;
hence f in { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) } by A2, A6; :: thesis: verum

end;

then { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) } = { F where F is Function of (X \/ {x}),Y : F . x = y } by A3, XBOOLE_0:def 10;
hence card (Funcs X,Y) = card { F where F is Function of (X \/ {x}),Y : F . x = y } by A1, Th2; :: thesis: verum