consider g being sequence of (Funcs ((AllFormulasOf S),(AllFormulasOf S))) such that

A1: ( g . 0 = f & ( for m being Nat holds g . (m + 1) = H_{1}(m,g . m) ) )
from NAT_1:sch 12();

take g ; :: thesis: ( g . 0 = f & ( for m being Nat holds g . (m + 1) = (l,t,m,(g . m)) Subst3 ) )

thus ( g . 0 = f & ( for m being Nat holds g . (m + 1) = (l,t,m,(g . m)) Subst3 ) ) by A1; :: thesis: verum

A1: ( g . 0 = f & ( for m being Nat holds g . (m + 1) = H

take g ; :: thesis: ( g . 0 = f & ( for m being Nat holds g . (m + 1) = (l,t,m,(g . m)) Subst3 ) )

thus ( g . 0 = f & ( for m being Nat holds g . (m + 1) = (l,t,m,(g . m)) Subst3 ) ) by A1; :: thesis: verum