let IT1, IT2 be Function of NAT,(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
B1: IT1 . 0 = f and
B2: for m being Nat holds IT1 . (m + 1) = H₁(m,IT1 . m) and
B3: IT2 . 0 = f and
B4: for m being Nat holds IT2 . (m + 1) = H₁(m,IT2 . m) ; :: thesis: IT1 = IT2
IT1 = IT2 from NAT_1:sch 16(B1, B2, B3, B4);
hence IT1 = IT2 ; :: thesis: verum