reconsider nn = n as Element of NAT by ORDINAL1:def 12;

deffunc H_{1}( 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_{1}(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

deffunc H

consider g being Function of (AllFormulasOf S),(AllFormulasOf S) such that

A1: for x being Element of AllFormulasOf S holds g . x = H

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

hence
for phi being wff string of S holds gg . phi = (l,t,n,f) Subst2 phi
; :: thesis: verumlet 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_{1}(phii)
by A1;

hence gg . phi = (l,t,nn,f) Subst2 phi ; :: thesis: verum

end;reconsider phii = phi as Element of AllFormulasOf S by FOMODEL2:16;

g . phii = H

hence gg . phi = (l,t,nn,f) Subst2 phi ; :: thesis: verum