reconsider nn = n as Element of NAT by ORDINAL1:def 12;
deffunc H₁( Element of AllFormulasOf S) -> Element of AllFormulasOf S = (l,t,nn,f) Subst2 $1;
consider g being Function of (AllFormulasOf S),(AllFormulasOf S) such that
A1: for x being Element of AllFormulasOf S holds g . x = H₁(x) from FUNCT_2:sch 4();
reconsider gg = g as Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) by FUNCT_2:8;
take gg ; :: thesis: for phi being wff string of S holds gg . phi = (l,t,n,f) Subst2 phi

now :: thesis: for phi being wff string of S holds gg . phi = (l,t,nn,f) Subst2 phi

let phi be wff string of S; :: thesis: gg . phi = (l,t,nn,f) Subst2 phi
reconsider phii = phi as Element of AllFormulasOf S by FOMODEL2:16;
g . phii = H₁(phii) by A1;
hence gg . phi = (l,t,nn,f) Subst2 phi ; :: thesis: verum

end;

hence for phi being wff string of S holds gg . phi = (l,t,n,f) Subst2 phi ; :: thesis: verum