set FF = AllFormulasOf S;
set D = Funcs ((AllFormulasOf S),(AllFormulasOf S));
reconsider d = Depth phi as Element of NAT by ORDINAL1:def 12;
reconsider F = (l,t) Subst4 (l Subst1 t) as sequence of (Funcs ((AllFormulasOf S),(AllFormulasOf S))) ;
F . d is Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) ;
then reconsider f = F . d as Function of (AllFormulasOf S),(AllFormulasOf S) ;
reconsider phii = phi as Element of AllFormulasOf S by FOMODEL2:16;
f . phii is wff string of S by TARSKI:def 3;
hence (((l,t) Subst4 (l Subst1 t)) . (Depth phi)) . phi is wff string of S ; :: thesis: verum