set IT = (l1,l2) -SymbolSubstIn t;
set TT = AllTermsOf S;
set T = S -termsOfMaxDepth ;
reconsider TF = S -termsOfMaxDepth as Function ;
t in AllTermsOf S by FOMODEL1:def 32;
then consider mm being Element of NAT such that
A1: t in TF . mm by FOMODEL1:5;
reconsider tm = t as mm -termal string of S by A1, FOMODEL1:def 33;
(l1,l2) -SymbolSubstIn tm is mm -termal ;
hence for b₁ being string of S st b₁ = (l1,l2) -SymbolSubstIn t holds
b₁ is termal ; :: thesis: verum