set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;

now

let y be set ; :: thesis: ( y in rng (S -termsOfMaxDepth) implies y in bool (((AllSymbolsOf S) *) \ {{}}) )
assume y in rng (S -termsOfMaxDepth) ; :: thesis: y in bool (((AllSymbolsOf S) *) \ {{}})
then consider x being set such that
C1: ( x in dom (S -termsOfMaxDepth) & (S -termsOfMaxDepth) . x = y ) by FUNCT_1:def 3;
reconsider mm = x as Element of NAT by C1;
(S -termsOfMaxDepth) . mm misses {{}}

proof

assume (S -termsOfMaxDepth) . mm meets {{}} ; :: thesis: contradiction
then ((S -termsOfMaxDepth) . mm) /\ {{}} <> {} by XBOOLE_0:def 7;
then consider z being set such that
D1: z in ((S -termsOfMaxDepth) . mm) /\ {{}} by XBOOLE_0:def 1;
thus contradiction by D1; :: thesis: verum

end;

then (S -termsOfMaxDepth) . mm c= ((AllSymbolsOf S) *) \ {{}} by XBOOLE_1:86;
hence y in bool (((AllSymbolsOf S) *) \ {{}}) by C1; :: thesis: verum

end;

then rng (S -termsOfMaxDepth) c= bool (((AllSymbolsOf S) *) \ {{}}) by TARSKI:def 3;
hence S -termsOfMaxDepth is Function of NAT,(bool (((AllSymbolsOf S) *) \ {{}})) by FUNCT_2:6; :: thesis: verum