set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;
now :: thesis: for y being object st y in rng (S -termsOfMaxDepth) holds
y in bool (((AllSymbolsOf S) *) \ {{}})
let y be object ; :: 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 object such that
A1: ( x in dom (S -termsOfMaxDepth) & (S -termsOfMaxDepth) . x = y ) by FUNCT_1:def 3;
reconsider mm = x as Element of NAT by A1;
(S -termsOfMaxDepth) . mm misses {{}}
proof
assume (S -termsOfMaxDepth) . mm meets {{}} ; :: thesis: contradiction
then ((S -termsOfMaxDepth) . mm) /\ {{}} <> {} ;
then consider z being object such that
A2: z in ((S -termsOfMaxDepth) . mm) /\ {{}} by XBOOLE_0:def 1;
thus contradiction by A2; :: thesis: verum
end;
then (S -termsOfMaxDepth) . mm c= ((AllSymbolsOf S) *) \ {{}} by XBOOLE_1:86;
hence y in bool (((AllSymbolsOf S) *) \ {{}}) by A1; :: thesis: verum
end;
then rng (S -termsOfMaxDepth) c= bool (((AllSymbolsOf S) *) \ {{}}) by TARSKI:def 3;
hence S -termsOfMaxDepth is sequence of (bool (((AllSymbolsOf S) *) \ {{}})) by FUNCT_2:6; :: thesis: verum