set T = S -termsOfMaxDepth ;
set F = S -firstChar ;
set C = S -multiCat ;
set A = AllTermsOf S;
set SS = AllSymbolsOf S;
consider TT being Element of ((S -termsOfMaxDepth) . mm) * such that
A1: ( TT is |.(ar t).| -element & t = <*((S -firstChar) . t)*> ^ ((S -multiCat) . TT) ) by Th3;
reconsider X = (S -termsOfMaxDepth) . mm as Subset of (AllTermsOf S) by Th2;
reconsider Y = X * as non empty Subset of ((AllTermsOf S) *) ;
reconsider TTTT = TT as Element of Y ;
reconsider TTT = TTTT as Element of (AllTermsOf S) * ;
TTT = SubTerms t by Def37, A1;
hence for b₁ being Element of (AllTermsOf S) * st b₁ = SubTerms t holds
b₁ is (S -termsOfMaxDepth) . mm -valued ; :: thesis: verum