thus Terminals PeanoNat <> {} by Lm8; :: according to DTCONSTR:def 6 :: thesis: ( PeanoNat is with_nonterminals & PeanoNat is with_useful_nonterminals )
thus NonTerminals PeanoNat <> {} by Lm11; :: according to DTCONSTR:def 7 :: thesis: PeanoNat is with_useful_nonterminals
reconsider rO = root-tree O as Element of TSPN by Def4, Lm8;
reconsider p = <*rO*> as FinSequence of TSPN ;
reconsider p = p as FinSequence of TS PeanoNat ;
let nt be Symbol of PeanoNat ; :: according to DTCONSTR:def 8 :: thesis: ( nt in NonTerminals PeanoNat implies ex p being FinSequence of TS PeanoNat st nt ==> roots p )
assume nt in NonTerminals PeanoNat ; :: thesis: ex p being FinSequence of TS PeanoNat st nt ==> roots p
then A1: nt = S by Lm13, TARSKI:def 1;
take p ; :: thesis: nt ==> roots p
A2: ( dom <*rO*> = Seg 1 & dom <*O*> = Seg 1 ) by FINSEQ_1:55;

now

let i be Element of NAT ; :: thesis: ( i in dom p implies ex rO being DecoratedTree st
( rO = p . i & <*O*> . i = rO . {} ) )
assume A3: i in dom p ; :: thesis: ex rO being DecoratedTree st
( rO = p . i & <*O*> . i = rO . {} )
reconsider rO = rO as DecoratedTree ;
take rO = rO; :: thesis: ( rO = p . i & <*O*> . i = rO . {} )
( i = 1 & <*O*> . 1 = O ) by A2, A3, FINSEQ_1:4, FINSEQ_1:57, TARSKI:def 1;
hence ( rO = p . i & <*O*> . i = rO . {} ) by FINSEQ_1:57, TREES_4:3; :: thesis: verum

end;

hence nt ==> roots p by A1, A2, Lm4, TREES_3:def 18; :: thesis: verum