let nt be Symbol of PeanoNat; :: thesis: ( ( nt = 0 implies PostTraversalLanguage nt = {<*0*>} ) & ( nt = 1 implies PostTraversalLanguage nt = { (<*0*> ^ (n |-> 1)) 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 PostTraversal rtO = <*0*> ^ (0 |-> 1) by Th17;
then A1: PostTraversal rtO = <*O*> ^ {}
.= <*O*> by FINSEQ_1:34 ;
thus ( nt = 0 implies PostTraversalLanguage nt = {<*0*>} ) :: thesis: ( nt = 1 implies PostTraversalLanguage nt = { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } )

proof

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

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

let x be object ; :: thesis: ( x in PostTraversalLanguage nt implies x in {<*0*>} )
assume x in PostTraversalLanguage nt ; :: thesis: x in {<*0*>}
then consider tsg being Element of FinTrees the carrier of PeanoNat such that
A3: x = PostTraversal 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 PostTraversalLanguage nt )
assume x in {<*0*>} ; :: thesis: x in PostTraversalLanguage nt
then A6: x = <*O*> by TARSKI:def 1;
rtO . {} = O by TREES_4:3;
hence x in PostTraversalLanguage nt by A1, A2, A6; :: thesis: verum

end;

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

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

let x be object ; :: thesis: ( x in PostTraversalLanguage nt implies x in { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } )
assume x in PostTraversalLanguage nt ; :: thesis: x in { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 }
then consider tsg being Element of FinTrees the carrier of PeanoNat such that
A8: x = PostTraversal 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 = <*0*> ^ ((height (dom tsg)) |-> 1) by A8, A9, Th17;
hence x in { (<*0*> ^ (n |-> 1)) 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 { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } or x in PostTraversalLanguage nt )
assume x in { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } ; :: thesis: x in PostTraversalLanguage nt
then consider n being Element of NAT such that
A15: x = <*0*> ^ (n |-> 1) and
A16: n <> 0 ;
defpred S₂[ Nat] means ( $1 <> 0 implies ex tsg being Element of TS PeanoNat st
( tsg . {} = S & PostTraversal tsg = <*0*> ^ ($1 |-> 1) ) );
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 & PostTraversal tsg = <*0*> ^ ((n + 1) |-> 1) )

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

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

then consider tsg being Element of TS PeanoNat such that
tsg . {} = S and
A20: PostTraversal tsg = <*0*> ^ (n |-> 1) by A19;
PostTraversal tsg = <*0*> ^ ((height (dom tsg)) |-> 1) by Th17;
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 & PostTraversal tsg9 = <*0*> ^ ((n + 1) |-> 1) )
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 & PostTraversal tsg9 = <*0*> ^ ((n + 1) |-> 1) ) by A23, Th17, TREES_4:def 4; :: thesis: verum

end;

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

take tsg9 = S -tree rtO; :: thesis: ( tsg9 . {} = S & PostTraversal tsg9 = <*0*> ^ ((n + 1) |-> 1) )
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 & PostTraversal tsg9 = <*0*> ^ ((n + 1) |-> 1) ) by A25, Th17, 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 & PostTraversal tsg = <*0*> ^ (n |-> 1) ) by A16;
hence x in PostTraversalLanguage nt by A7, A15; :: thesis: verum