let nt be Symbol of PeanoNat; :: thesis:
reconsider rtO = root-tree O as Element of TS PeanoNat ;
height (dom (root-tree 0)) = 0 by TREES_1:42, TREES_4:3;
then PreTraversal rtO = (0 |-> 1) ^ <*O*> by Th15;
then A1: PreTraversal rtO = {} ^ <*O*>
.= <*O*> by FINSEQ_1:34 ;
thus ( nt = 0 implies PreTraversalLanguage nt = {<*0*>} ) :: thesis:

proof

assume A2: nt = 0 ; :: thesis:

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

let x be object ; :: thesis:
assume x in PreTraversalLanguage nt ; :: thesis:
then consider tsg being Element of FinTrees the carrier of PeanoNat such that
A3: x = PreTraversal tsg and
A4: tsg in TS PeanoNat and
A5: tsg . {} = O by A2;
tsg = root-tree O by A4, A5, Th9;
hence x in {<*0*>} by A1, A3, TARSKI:def 1; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in {<*0*>} ; :: thesis:
then A6: x = <*O*> by TARSKI:def 1;
rtO . {} = O by TREES_4:3;
hence x in PreTraversalLanguage nt by A1, A2, A6; :: thesis:

end;

assume A7: nt = 1 ; :: thesis:

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

let x be object ; :: thesis:
assume x in PreTraversalLanguage nt ; :: thesis:
then consider tsg being Element of FinTrees the carrier of PeanoNat such that
A8: x = PreTraversal tsg and
A9: tsg in TS PeanoNat and
A10: tsg . {} = S by A7;
consider ts being FinSequence of TS PeanoNat such that
A11: tsg = S -tree ts and
A12: S ==> roots ts by A9, A10, Th10;
( roots ts = <*0*> or roots ts = <*1*> ) by A12, Def2;
then len (roots ts) = 1 by FINSEQ_1:40;
then consider t being Element of FinTrees the carrier of PeanoNat such that
A13: ts = <*t*> and
t in TS PeanoNat by Th5;
tsg = S -tree t by A11, A13, TREES_4:def 5;
then dom tsg = ^ (dom t) by TREES_4:13;
then A14: height (dom tsg) = (height (dom t)) + 1 by TREES_3:80;
x = ((height (dom tsg)) |-> 1) ^ <*0*> by A8, A9, Th15;
hence x in { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } by A14; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } ; :: thesis:
then consider n being Element of NAT such that
A15: x = (n |-> 1) ^ <*0*> and
A16: n <> 0 ;
defpred S₂[ Nat] means ( $1 <> 0 implies ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PreTraversal tsg = ($1 |-> 1) ^ <*0*> ) );
A17: S₂[ 0 ] ;

A18: now :: thesis:

let n be Nat; :: thesis:
assume A19: S₂[n] ; :: thesis:
thus S₂[n + 1] :: thesis:

proof

assume n + 1 <> 0 ; :: thesis:

per cases ;

suppose n <> 0 ; :: thesis:

then consider tsg being Element of TS PeanoNat such that
tsg . {} = S and
A20: PreTraversal tsg = (n |-> 1) ^ <*0*> by A19;
PreTraversal tsg = ((height (dom tsg)) |-> 1) ^ <*0*> by Th15;
then A21: n |-> 1 = (height (dom tsg)) |-> 1 by A20, FINSEQ_1:33;
len (n |-> 1) = n by CARD_1:def 7;
then A22: height (dom tsg) = n by A21, CARD_1:def 7;
take tsg9 = S -tree tsg; :: thesis:
A23: tsg9 = S -tree <*tsg*> by TREES_4:def 5;
height (dom tsg9) = height (^ (dom tsg)) by TREES_4:13
.= n + 1 by A22, TREES_3:80 ;
hence ( tsg9 . {} = S & PreTraversal tsg9 = ((n + 1) |-> 1) ^ <*0*> ) by A23, Th15, TREES_4:def 4; :: thesis:

end;

suppose A24: n = 0 ; :: thesis:

take tsg9 = S -tree rtO; :: thesis:
A25: tsg9 = S -tree <*rtO*> by TREES_4:def 5;
height (dom tsg9) = height (^ (dom rtO)) by TREES_4:13
.= (height (dom rtO)) + 1 by TREES_3:80
.= n + 1 by A24, TREES_1:42, TREES_4:3 ;
hence ( tsg9 . {} = S & PreTraversal tsg9 = ((n + 1) |-> 1) ^ <*0*> ) by A25, Th15, TREES_4:def 4; :: thesis:

end;

end;

end;

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(A17, A18);
then ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PreTraversal tsg = (n |-> 1) ^ <*0*> ) by A16;
hence x in PreTraversalLanguage nt by A7, A15; :: thesis: