let IT1, IT2 be sequence of (Funcs ((AllFormulasOf S),(AllFormulasOf S))); ( IT1 . 0 = f & ( for m being Nat holds IT1 . (m + 1) = (l,t,m,(IT1 . m)) Subst3 ) & IT2 . 0 = f & ( for m being Nat holds IT2 . (m + 1) = (l,t,m,(IT2 . m)) Subst3 ) implies IT1 = IT2 )
assume that
A2:
IT1 . 0 = f
and
A3:
for m being Nat holds IT1 . (m + 1) = H1(m,IT1 . m)
and
A4:
IT2 . 0 = f
and
A5:
for m being Nat holds IT2 . (m + 1) = H1(m,IT2 . m)
; IT1 = IT2
IT1 = IT2
from NAT_1:sch 16(A2, A3, A4, A5);
hence
IT1 = IT2
; verum