set C = S -multiCat ;
set t = s -compound V;
set T = S -termsOfMaxDepth ;
set L = LettersOf S;
set SS = AllSymbolsOf S;
set n = |.(ar s).|;
set A = AtomicTermsOf S;
set fam = { (Compound (u,((S -termsOfMaxDepth) . mm))) where u is ofAtomicFormula Element of S : u is operational } ;
A1: V is FinSequence of (S -termsOfMaxDepth) . mm by FINSEQ_1:def 11;
reconsider Ss = ((AllSymbolsOf S) *) \ {{}} as Subset of ((AllSymbolsOf S) *) ;
V in Ss * ;
then reconsider VV = V as Element of ((AllSymbolsOf S) *) * ;
( s -compound V = <*s*> ^ ((S -multiCat) . VV) & rng VV c= (S -termsOfMaxDepth) . mm ) by A1, FINSEQ_1:def 4;
then A2: s -compound V in Compound (s,((S -termsOfMaxDepth) . mm)) ;

per cases ;

suppose s is literal ; :: thesis:

then reconsider v = s as literal Element of S ;
reconsider vv = v as Element of LettersOf S by FOMODEL1:def 14;
ar v = 0 ;
then |.(ar s).| = 0 ;
then reconsider VVV = V as 0 -element FinSequence ;
s -compound V = <*s*> ^ VVV
.= <*vv*> ;
then s -compound V in AtomicTermsOf S by FINSEQ_2:98;
then ( (S -termsOfMaxDepth) . 0 c= (S -termsOfMaxDepth) . (0 + (mm + 1)) & s -compound V in (S -termsOfMaxDepth) . 0 ) by FOMODEL1:def 30, FOMODEL1:4;
hence for b₁ being string of S st b₁ = s -compound V holds
b₁ is mm + 1 -termal ; :: thesis:

end;

suppose not s is literal ; :: thesis:

then Compound (s,((S -termsOfMaxDepth) . mm)) in { (Compound (u,((S -termsOfMaxDepth) . mm))) where u is ofAtomicFormula Element of S : u is operational } ;
then s -compound V in union { (Compound (u,((S -termsOfMaxDepth) . mm))) where u is ofAtomicFormula Element of S : u is operational } by A2, TARSKI:def 4;
then s -compound V in (union { (Compound (u,((S -termsOfMaxDepth) . mm))) where u is ofAtomicFormula Element of S : u is operational } ) \/ ((S -termsOfMaxDepth) . mm) by XBOOLE_0:def 3;
then s -compound V in (S -termsOfMaxDepth) . (mm + 1) by FOMODEL1:def 30;
hence for b₁ being string of S st b₁ = s -compound V holds
b₁ is mm + 1 -termal ; :: thesis:

end;

end;