set SS = AllSymbolsOf S;
set T = S -termsOfMaxDepth ;
B1: dom (S -termsOfMaxDepth) = NAT by DefTerm;

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) & y = (S -termsOfMaxDepth) . x ) by FUNCT_1:def 3;
reconsider m = x as Element of NAT by DefTerm, C1;
y = (S -termsOfMaxDepth) . m by C1;
then ( y c= ((AllSymbolsOf S) *) \ {{}} & ((AllSymbolsOf S) *) \ {{}} c= (AllSymbolsOf S) * ) by Lm9;
then y c= (AllSymbolsOf S) * by XBOOLE_1:1;
hence y in bool ((AllSymbolsOf S) *) ; :: 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 B1, FUNCT_2:67, RELSET_1:4; :: thesis: verum