set T = S -termsOfMaxDepth ;
set n = |.(ar s).|;
consider mm being Element of NAT such that
A1: V is Element of ((S -termsOfMaxDepth) . mm) * by Lm3;
reconsider VV = V as |.(ar s).| -element Element of ((S -termsOfMaxDepth) . mm) * by A1;
s -compound VV is mm + 1 -termal string of S ;
hence for b₁ being string of S st b₁ = s -compound V holds
b₁ is termal ; :: thesis: verum