consider f being Function of (TS PeanoNat ),(the carrier of PeanoNat * ) such that
A1: ( PreTraversal (root-tree O) = f . (root-tree O) & ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
f . (root-tree t) = <*t*> ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat
for rts being FinSequence st rts = roots ts & nt ==> rts holds
for x being FinSequence of the carrier of PeanoNat * st x = f * ts holds
f . (nt -tree ts) = <*nt*> ^ (FlattenSeq x) ) ) by Def16;
reconsider rtO = root-tree O as Element of TS PeanoNat ;
defpred S₂[ DecoratedTree of ] means ex t being Element of TS PeanoNat st
( $1 = t & PreTraversal t = ((height (dom t)) |-> 1) ^ <*0 *> );

A2: now

let s be Symbol of PeanoNat ; :: thesis: ( s in Terminals PeanoNat implies S₂[ root-tree s] )
assume A3: s in Terminals PeanoNat ; :: thesis: S₂[ root-tree s]
thus S₂[ root-tree s] :: thesis: verum

proof

take t = rtO; :: thesis: ( root-tree s = t & PreTraversal t = ((height (dom t)) |-> 1) ^ <*0 *> )
thus root-tree s = t by A3, Lm9, TARSKI:def 1; :: thesis: PreTraversal t = ((height (dom t)) |-> 1) ^ <*0 *>
thus PreTraversal t = <*O*> by A1
.= {} ^ <*O*> by FINSEQ_1:47
.= (0 |-> 1) ^ <*0 *> by FINSEQ_2:72
.= ((height (dom t)) |-> 1) ^ <*0 *> by TREES_1:79, TREES_4:3 ; :: thesis: verum

end;

end;

A4: now

let nt be Symbol of PeanoNat ; :: thesis: for ts being FinSequence of TS PeanoNat st nt ==> roots ts & ( for t being DecoratedTree of st t in rng ts holds
S₂[t] ) holds
S₂[nt -tree ts]
let ts be FinSequence of TS PeanoNat ; :: thesis: ( nt ==> roots ts & ( for t being DecoratedTree of st t in rng ts holds
S₂[t] ) implies S₂[nt -tree ts] )
assume A5: ( nt ==> roots ts & ( for t being DecoratedTree of st t in rng ts holds
S₂[t] ) ) ; :: thesis: S₂[nt -tree ts]
then reconsider t' = nt -tree ts as Element of TS PeanoNat by Def4;
A6: ( nt = S & ( roots ts = <*O*> or roots ts = <*1*> ) ) by A5, Def5;
then len (roots ts) = 1 by FINSEQ_1:57;
then consider x being Element of FinTrees the carrier of PeanoNat such that
A7: ( ts = <*x*> & x in TS PeanoNat ) by Th5;
reconsider x' = x as Element of TS PeanoNat by A7;
rng ts = {x} by A7, FINSEQ_1:56;
then x in rng ts by TARSKI:def 1;
then A8: ex t' being Element of TS PeanoNat st
( x = t' & PreTraversal t' = ((height (dom t')) |-> 1) ^ <*0 *> ) by A5;
f . x' is Element of the carrier of PeanoNat * ;
then A9: f . x' = ((height (dom x')) |-> 1) ^ <*0 *> by A1, A8, Def16;
f * ts = <*(f . x)*> by A7, FINSEQ_2:39;
then A10: f . (nt -tree ts) = <*nt*> ^ (FlattenSeq <*(f . x')*>) by A1, A5
.= <*nt*> ^ (((height (dom x')) |-> 1) ^ <*0 *>) by A9, Th13
.= (<*nt*> ^ ((height (dom x')) |-> 1)) ^ <*0 *> by FINSEQ_1:45
.= ((1 |-> 1) ^ ((height (dom x')) |-> 1)) ^ <*0 *> by A6, FINSEQ_2:73
.= (((height (dom x')) + 1) |-> 1) ^ <*0 *> by FINSEQ_2:143
.= ((height (^ (dom x'))) |-> 1) ^ <*0 *> by TREES_3:83 ;
A11: ( dom (nt -tree x') = ^ (dom x') & t' = nt -tree x' ) by A7, TREES_4:13, TREES_4:def 5;
f . t' is Element of the carrier of PeanoNat * ;
then PreTraversal (nt -tree ts) = f . (nt -tree ts) by A1, Def16;
hence S₂[nt -tree ts] by A10, A11; :: thesis: verum

end;

A12: for t being DecoratedTree of st t in TS PeanoNat holds
S₂[t] from DTCONSTR:sch 7(A2, A4);
let t be Element of TS PeanoNat ; :: thesis: PreTraversal t = ((height (dom t)) |-> 1) ^ <*0 *>
S₂[t] by A12;
hence PreTraversal t = ((height (dom t)) |-> 1) ^ <*0 *> ; :: thesis: verum