let nt be Symbol of PeanoNat; :: thesis: ( ( nt = 0 implies PreTraversalLanguage nt = {<*0*>} ) & ( nt = 1 implies PreTraversalLanguage nt = { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } ) )
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: ( nt = 1 implies PreTraversalLanguage nt = { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } )

proof

assume A2: nt = 0 ; :: thesis: PreTraversalLanguage nt = {<*0*>}

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {<*0*>} c= PreTraversalLanguage nt

let x be object ; :: thesis: ( x in PreTraversalLanguage nt implies x in {<*0*>} )
assume x in PreTraversalLanguage nt ; :: thesis: x in {<*0*>}
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: verum

end;

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

end;

assume A7: nt = 1 ; :: thesis: PreTraversalLanguage nt = { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 }

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } c= PreTraversalLanguage nt

let x be object ; :: thesis: ( x in PreTraversalLanguage nt implies x in { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } )
assume x in PreTraversalLanguage nt ; :: thesis: x in { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 }
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: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } or x in PreTraversalLanguage nt )
assume x in { ((n |-> 1) ^ <*0*>) where n is Element of NAT : n <> 0 } ; :: thesis: x in PreTraversalLanguage nt
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: for n being Nat st S₂[n] holds
S₂[n + 1]

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

proof

assume n + 1 <> 0 ; :: thesis: ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PreTraversal tsg = ((n + 1) |-> 1) ^ <*0*> )

per cases ( n <> 0 or n = 0 ) ;

suppose n <> 0 ; :: thesis: ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PreTraversal tsg = ((n + 1) |-> 1) ^ <*0*> )

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: ( tsg9 . {} = S & PreTraversal tsg9 = ((n + 1) |-> 1) ^ <*0*> )
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: verum

end;

suppose A24: n = 0 ; :: thesis: ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PreTraversal tsg = ((n + 1) |-> 1) ^ <*0*> )

take tsg9 = S -tree rtO; :: thesis: ( tsg9 . {} = S & PreTraversal tsg9 = ((n + 1) |-> 1) ^ <*0*> )
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: verum

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: verum