ex f being sequence of (TS PeanoNat) st
( f . 0 = root-tree O & ( for n being Nat holds f . (n + 1) = H₄(n,f . n) ) ) from NAT_1:sch 12();
hence ex b₁ being sequence of (TS PeanoNat) st
( b₁ . 0 = root-tree 0 & ( for n being Nat holds b₁ . (n + 1) = PNsucc (b₁ . n) ) ) ; :: thesis: verum