let it1, it2 be Function of NAT ,(TS PeanoNat ); :: thesis: ( it1 . 0 = root-tree 0 & ( for n being Nat holds it1 . (n + 1) = PNsucc (it1 . n) ) & it2 . 0 = root-tree 0 & ( for n being Nat holds it2 . (n + 1) = PNsucc (it2 . n) ) implies it1 = it2 )
assume A1: ( it1 . 0 = root-tree 0 & ( for n being Nat holds it1 . (n + 1) = PNsucc (it1 . n) ) & it2 . 0 = root-tree 0 & ( for n being Nat holds it2 . (n + 1) = PNsucc (it2 . n) ) & not it1 = it2 ) ; :: thesis: contradiction
then A2: it1 . 0 = root-tree O ;
B2: for n being Nat holds it1 . (n + 1) = H₄(n,it1 . n) by A1;
A3: it2 . 0 = root-tree O by A1;
B3: for n being Nat holds it2 . (n + 1) = H₄(n,it2 . n) by A1;
it1 = it2 from NAT_1:sch 16(A2, B2, A3, B3);
hence contradiction by A1; :: thesis: verum