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₁(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