let X be functional set ; :: thesis: ( X is finite & X is finite-membered implies SymbolsOf X is finite )
set Y = X \/ {{}};
set F = { (rng y) where y is Element of X \/ {{}} : y in X } ;
assume A1: X is finite ; :: thesis: ( not X is finite-membered or SymbolsOf X is finite )
{ (rng y) where y is Element of X \/ {{}} : y in X } is finite from FRAENKEL:sch 21(A1);
then reconsider FF = { (rng y) where y is Element of X \/ {{}} : y in X } as finite set ;
assume X is finite-membered ; :: thesis: SymbolsOf X is finite
then reconsider YY = X \/ {{}} as finite-membered set ;

now :: thesis: for y being set st y in { (rng y) where y is Element of X \/ {{}} : y in X } holds
y is finite

let y be set ; :: thesis: ( y in { (rng y) where y is Element of X \/ {{}} : y in X } implies y is finite )
assume y in { (rng y) where y is Element of X \/ {{}} : y in X } ; :: thesis: y is finite
then consider x being Element of X \/ {{}} such that
A2: ( y = rng x & x in X ) ;
reconsider xx = x as Element of YY ;
xx is finite ;
hence y is finite by A2; :: thesis: verum

end;

then reconsider FFF = FF as finite finite-membered set by FINSET_1:def 6;
union FFF is finite ;
hence SymbolsOf X is finite ; :: thesis: verum