set d = Depth phi;
set TT = AllTermsOf S;
reconsider tt = t as Element of AllTermsOf S by FOMODEL1:def 32;
set psi = (l,tt) SubstIn phi;
reconsider k = m - (Depth phi) as Nat ;
Depth ((l,tt) SubstIn phi) = Depth phi by Th10;
then reconsider psii = (l,tt) SubstIn phi as Depth phi -wff string of S by FOMODEL2:def 31;
psii is (Depth phi) + (0 * k) -wff ;
then psii is (Depth phi) + k -wff ;
hence for b₁ being string of S st b₁ = (l,t) SubstIn phi holds
b₁ is m -wff ; :: thesis: verum