consider f being Function of (TS PeanoNat ),((Terminals PeanoNat ) * ) such that
A1: ( TerminalString (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 st nt ==> roots ts holds
f . (nt -tree ts) = FlattenSeq (f * ts) ) ) by Def15;
defpred S₂[ DecoratedTree of ] means TerminalString $1 = <*0 *>;

A2: now

let s be Symbol of PeanoNat ; :: thesis: ( s in Terminals PeanoNat implies S₂[ root-tree s] )
assume s in Terminals PeanoNat ; :: thesis: S₂[ root-tree s]
then s = O by Lm9, TARSKI:def 1;
hence S₂[ root-tree s] by A1; :: thesis: verum

end;

A3: 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 A4: ( nt ==> roots ts & ( for t being DecoratedTree of st t in rng ts holds
S₂[t] ) ) ; :: thesis: S₂[nt -tree ts]
then A5: nt -tree ts in TS PeanoNat by Def4;
( nt = S & ( roots ts = <*O*> or roots ts = <*1*> ) ) by A4, Def5;
then len (roots ts) = 1 by FINSEQ_1:57;
then consider x being Element of FinTrees the carrier of PeanoNat such that
A6: ( ts = <*x*> & x in TS PeanoNat ) by Th5;
reconsider x' = x as Element of TS PeanoNat by A6;
rng ts = {x} by A6, FINSEQ_1:56;
then A7: x in rng ts by TARSKI:def 1;
f . x' is Element of (Terminals PeanoNat ) * ;
then A8: f . x' = TerminalString x by A1, Def15
.= <*O*> by A4, A7 ;
f * ts = <*(f . x)*> by A6, FINSEQ_2:39;
then f . (nt -tree ts) = FlattenSeq <*(f . x')*> by A1, A4
.= <*O*> by A8, Th13 ;
hence S₂[nt -tree ts] by A1, A5, Def15; :: thesis: verum

end;

thus for t being DecoratedTree of st t in TS PeanoNat holds
S₂[t] from DTCONSTR:sch 7(A2, A3); :: thesis: verum