let f be Function; :: thesis:
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;

let y be object ; :: thesis:
assume y in union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } ; :: thesis:
then consider z being set such that
A1: ( 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
A2: ( z = rng x & x in {f} ) by A1;
thus y in rng f by A1, A2, TARSKI:def 1; :: thesis:

end;

then A3: union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } c= rng f ;

let y be object ; :: thesis:
assume y in rng f ; :: thesis:
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:

end;

then rng f c= union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } ;
hence SymbolsOf {f} = rng f by A3; :: thesis: