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

b_{1} is m -wff
; :: thesis: verum

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

b