let f be Function; :: thesis: SymbolsOf {f} = rng f
set P = f;
set X = {f};
set F = { (rng x) where x is Element of {f} \/ {{}} : x in {f} } ;
set LH = union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } ;
set RH = rng f;
{f} null {{}} c= {f} \/ {{}} ;
then reconsider XX = {f} as Subset of ({f} \/ {{}}) ;
reconsider PP = f as Element of XX by TARSKI:def 1;
reconsider PPP = PP as Element of {f} \/ {{}} by TARSKI:def 3;

now

let y be set ; :: thesis: ( y in union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } implies y in rng f )
assume y in union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } ; :: thesis: y in rng f
then consider z being set such that
C0: ( y in z & z in { (rng x) where x is Element of {f} \/ {{}} : x in {f} } ) by TARSKI:def 4;
consider x being Element of {f} \/ {{}} such that
C1: ( z = rng x & x in {f} ) by C0;
thus y in rng f by C0, C1, TARSKI:def 1; :: thesis: verum

end;

then B0: union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } c= rng f by TARSKI:def 3;

now

let y be set ; :: thesis: ( y in rng f implies y in union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } )
assume y in rng f ; :: thesis: y in union { (rng x) where x is Element of {f} \/ {{}} : x in {f} }
then ( y in rng PP & rng PPP in { (rng x) where x is Element of {f} \/ {{}} : x in {f} } ) ;
hence y in union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } by TARSKI:def 4; :: thesis: verum

end;

then rng f c= union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } by TARSKI:def 3;
hence SymbolsOf {f} = rng f by B0, XBOOLE_0:def 10; :: thesis: verum