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

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