set e = l1 SubstWith l2;
set T = S -termsOfMaxDepth ;
set SS = AllSymbolsOf S;
set IT = (l1,l2) -SymbolSubstIn t;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
reconsider f = (l1 SubstWith l2) | ((S -termsOfMaxDepth) . m) as Function of ((S -termsOfMaxDepth) . m),((S -termsOfMaxDepth) . m) by Lm31;
reconsider tt = t as Element of (S -termsOfMaxDepth) . m by FOMODEL1:def 33;
(f . tt) \+\ ((l1 SubstWith l2) . tt) = {} ;
then f . tt = (l1 SubstWith l2) . tt by FOMODEL0:29;
then (l1 SubstWith l2) . t in (S -termsOfMaxDepth) . mm ;
then (l1,l2) -SymbolSubstIn t in (S -termsOfMaxDepth) . mm by FOMODEL0:def 22;
hence for b₁ being string of S st b₁ = (l1,l2) -SymbolSubstIn t holds
b₁ is m -termal ; :: thesis: verum