let X, Y be finite set ; :: thesis: for x, y being set st ( Y = {} implies X = {} ) & not x in X holds
card (Funcs X,Y) = card { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) }
let x, y be set ; :: thesis: ( ( Y = {} implies X = {} ) & not x in X implies card (Funcs X,Y) = card { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) } )
assume A1: ( Y = {} implies X = {} ) ; :: thesis: ( x in X or card (Funcs X,Y) = card { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) } )
then A2: ( Y is empty implies X is empty ) ;
assume A3: not x in X ; :: thesis: card (Funcs X,Y) = card { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) }
defpred S₁[ set , set , set ] means 1 = 1;
A4: for f being Function of (X \/ {x}),(Y \/ {y}) st f . x = y holds
( S₁[f,X \/ {x},Y \/ {y}] iff S₁[f | X,X,Y] ) ;
set F1 = { f where f is Function of X,Y : S₁[f,X,Y] } ;
set F2 = { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S₁[f,X \/ {x},Y \/ {y}] & rng (f | X) c= Y & f . x = y ) } ;
set F3 = { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) } ;
A5: { f where f is Function of X,Y : S₁[f,X,Y] } c= Funcs X,Y

proof

let F be set ; :: according to TARSKI:def 3 :: thesis: ( not F in { f where f is Function of X,Y : S₁[f,X,Y] } or F in Funcs X,Y )
assume A6: F in { f where f is Function of X,Y : S₁[f,X,Y] } ; :: thesis: F in Funcs X,Y
ex f being Function of X,Y st
( f = F & S₁[f,X,Y] ) by A6;
hence F in Funcs X,Y by A1, FUNCT_2:11; :: thesis: verum

end;

Funcs X,Y c= { f where f is Function of X,Y : S₁[f,X,Y] }

proof

let F be set ; :: according to TARSKI:def 3 :: thesis: ( not F in Funcs X,Y or F in { f where f is Function of X,Y : S₁[f,X,Y] } )
assume A7: F in Funcs X,Y ; :: thesis: F in { f where f is Function of X,Y : S₁[f,X,Y] }
F is Function of X,Y by A7, FUNCT_2:121;
hence F in { f where f is Function of X,Y : S₁[f,X,Y] } ; :: thesis: verum

end;

then A8: Funcs X,Y = { f where f is Function of X,Y : S₁[f,X,Y] } by A5, XBOOLE_0:def 10;
A9: { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S₁[f,X \/ {x},Y \/ {y}] & rng (f | X) c= 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 \/ {y}) : ( S₁[f,X \/ {x},Y \/ {y}] & rng (f | X) c= 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 A10: F in { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S₁[f,X \/ {x},Y \/ {y}] & rng (f | X) c= 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 ) }
ex f being Function of (X \/ {x}),(Y \/ {y}) st
( f = F & S₁[f,X \/ {x},Y \/ {y}] & rng (f | X) c= Y & f . x = y ) by A10;
hence F in { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) } ; :: thesis: verum

end;

A11: { 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 \/ {y}) : ( S₁[f,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 \/ {y}) : ( rng (F | X) c= Y & F . x = y ) } or F in { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S₁[f,X \/ {x},Y \/ {y}] & rng (f | X) c= Y & f . x = y ) } )
assume A12: 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 \/ {y}) : ( S₁[f,X \/ {x},Y \/ {y}] & rng (f | X) c= 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 A12;
hence F in { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S₁[f,X \/ {x},Y \/ {y}] & rng (f | X) c= Y & f . x = y ) } ; :: thesis: verum

end;

card { f where f is Function of X,Y : S₁[f,X,Y] } = card { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S₁[f,X \/ {x},Y \/ {y}] & rng (f | X) c= Y & f . x = y ) } from STIRL2_1:sch 4(A2, A3, A4);
hence card (Funcs X,Y) = card { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) } by A8, A9, A11, XBOOLE_0:def 10; :: thesis: verum