defpred S1[ set , set , set ] means 1 = 1;
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 ) } )
set F2 = { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S1[f,X \/ {x},Y \/ {y}] & rng (f | X) c= Y & f . x = y ) } ;
A2: for f being Function of (X \/ {x}),(Y \/ {y}) st f . x = y holds
( S1[f,X \/ {x},Y \/ {y}] iff S1[f | X,X,Y] ) ;
set F1 = { f where f is Function of X,Y : S1[f,X,Y] } ;
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 ) }
set F3 = { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) } ;
A4: Funcs (X,Y) c= { f where f is Function of X,Y : S1[f,X,Y] }
proof
let F be object ; :: according to TARSKI:def 3 :: thesis: ( not F in Funcs (X,Y) or F in { f where f is Function of X,Y : S1[f,X,Y] } )
assume F in Funcs (X,Y) ; :: thesis: F in { f where f is Function of X,Y : S1[f,X,Y] }
then F is Function of X,Y by FUNCT_2:66;
hence F in { f where f is Function of X,Y : S1[f,X,Y] } ; :: thesis: verum
end;
A5: { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S1[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 object ; :: according to TARSKI:def 3 :: thesis: ( not F in { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S1[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 F in { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S1[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 ) }
then ex f being Function of (X \/ {x}),(Y \/ {y}) st
( f = F & S1[f,X \/ {x},Y \/ {y}] & rng (f | X) c= Y & f . x = y ) ;
hence F in { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) } ; :: thesis: verum
end;
A6: ( Y is empty implies X is empty ) by A1;
A7: card { f where f is Function of X,Y : S1[f,X,Y] } = card { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S1[f,X \/ {x},Y \/ {y}] & rng (f | X) c= Y & f . x = y ) } from STIRL2_1:sch 4(A6, A3, A2);
 A8: { 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}) : ( S1[f,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 \/ {y}) : ( rng (F | X) c= Y & F . x = y ) } or F in { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S1[f,X \/ {x},Y \/ {y}] & rng (f | X) c= 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 \/ {y}) : ( S1[f,X \/ {x},Y \/ {y}] & rng (f | X) c= 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 \/ {y}) : ( S1[f,X \/ {x},Y \/ {y}] & rng (f | X) c= Y & f . x = y ) } ; :: thesis: verum
end;
{ f where f is Function of X,Y : S1[f,X,Y] } c= Funcs (X,Y)
proof
let F be object ; :: according to TARSKI:def 3 :: thesis: ( not F in { f where f is Function of X,Y : S1[f,X,Y] } or F in Funcs (X,Y) )
assume F in { f where f is Function of X,Y : S1[f,X,Y] } ; :: thesis: F in Funcs (X,Y)
then ex f being Function of X,Y st
( f = F & S1[f,X,Y] ) ;
hence F in Funcs (X,Y) by A1, FUNCT_2:8; :: thesis: verum
end;
then Funcs (X,Y) = { f where f is Function of X,Y : S1[f,X,Y] } by 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 A5, A8, A7, XBOOLE_0:def 10; :: thesis: verum