set SS = AllSymbolsOf S;
set T = S -termsOfMaxDepth ;
A1: dom (S -termsOfMaxDepth) = NAT by Def30;
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) *) )
reconsider yy = y as set by TARSKI:1;
assume y in rng (S -termsOfMaxDepth) ; :: thesis: y in bool ((AllSymbolsOf S) *)
then consider x being object such that
A2: ( x in dom (S -termsOfMaxDepth) & y = (S -termsOfMaxDepth) . x ) by FUNCT_1:def 3;
reconsider m = x as Element of NAT by Def30, A2;
y = (S -termsOfMaxDepth) . m by A2;
then ( yy c= ((AllSymbolsOf S) *) \ {{}} & ((AllSymbolsOf S) *) \ {{}} c= (AllSymbolsOf S) * ) by Lm4;
then yy 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 sequence of (bool ((AllSymbolsOf S) *)) by A1, RELSET_1:4, FUNCT_2:67; :: thesis: verum