let it1, it2 be sequence of (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 ;
A3: for n being Nat holds it1 . (n + 1) = H₄(n,it1 . n) by A1;
A4: it2 . 0 = root-tree O by A1;
A5: for n being Nat holds it2 . (n + 1) = H₄(n,it2 . n) by A1;
it1 = it2 from NAT_1:sch 16(A2, A3, A4, A5);
hence contradiction by A1; :: thesis: verum