set T = S -termsOfMaxDepth ;
set n = abs (ar s);
consider mm being Element of NAT such that
B1: V is Element of ((S -termsOfMaxDepth) . mm) * by Lm1;
reconsider VV = V as abs (ar s) -element Element of ((S -termsOfMaxDepth) . mm) * by B1;
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