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 that
A1: not x in X and
A2: y in Y ; :: thesis: card (Funcs (X,Y)) = card { F where F is Function of (X \/ {x}),Y : F . x = y }
set F2 = { 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 ) } ;
{y} c= Y by A2, ZFMISC_1:31;
then A3: Y = Y \/ {y} by XBOOLE_1:12;
A4: { 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 object ; :: 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 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 ) }
then consider F being Function of (X \/ {x}),Y such that
A5: ( f = F & F . x = y ) ;
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 A3, A5; :: thesis: verum

end;

{ 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 object ; :: 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 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 }
then ex F being Function of (X \/ {x}),(Y \/ {y}) st
( f = F & rng (F | X) c= Y & F . x = y ) ;
hence f in { F where F is Function of (X \/ {x}),Y : F . x = y } by A3; :: 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 A4;
hence card (Funcs (X,Y)) = card { F where F is Function of (X \/ {x}),Y : F . x = y } by A1, A2, Th1; :: thesis: verum