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_{1} being string of S st b_{1} = (l1,l2) -SymbolSubstIn t holds

b_{1} is termal
; :: thesis: verum

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

b