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_{1}(m,IT1 . m)
and

A4: IT2 . 0 = f and

A5: for m being Nat holds IT2 . (m + 1) = H_{1}(m,IT2 . m)
; :: thesis: IT1 = IT2

IT1 = IT2 from NAT_1:sch 16(A2, A3, A4, A5);

hence IT1 = IT2 ; :: thesis: verum

assume that

A2: IT1 . 0 = f and

A3: for m being Nat holds IT1 . (m + 1) = H

A4: IT2 . 0 = f and

A5: for m being Nat holds IT2 . (m + 1) = H

IT1 = IT2 from NAT_1:sch 16(A2, A3, A4, A5);

hence IT1 = IT2 ; :: thesis: verum