let IT1, IT2 be sequence of (Funcs ((AllFormulasOf S),(AllFormulasOf S))); :: thesis: ( 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) = H₁(m,IT1 . m) and
A4: IT2 . 0 = f and
A5: for m being Nat holds IT2 . (m + 1) = H₁(m,IT2 . m) ; :: thesis: IT1 = IT2
IT1 = IT2 from NAT_1:sch 16(A2, A3, A4, A5);
hence IT1 = IT2 ; :: thesis: verum