thus Terminals PeanoNat <> {} by Lm9; :: according to DTCONSTR:def 3 :: thesis: ( PeanoNat is with_nonterminals & PeanoNat is with_useful_nonterminals )
thus NonTerminals PeanoNat <> {} by Lm12; :: according to DTCONSTR:def 4 :: thesis: PeanoNat is with_useful_nonterminals
reconsider rO = root-tree O as Element of TSPN by Def1, Lm9;
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 5 :: 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 Lm14, TARSKI:def 1;
take p ; :: thesis: nt ==> roots p
A2: dom <*rO*> = Seg 1 by FINSEQ_1:38;
A3: dom <*O*> = Seg 1 by FINSEQ_1:38;

now :: thesis: for i being Element of NAT st i in dom p holds
ex rO being DecoratedTree st
( rO = p . i & <*O*> . i = rO . {} )

let i be Element of NAT ; :: thesis: ( i in dom p implies ex rO being DecoratedTree st
( rO = p . i & <*O*> . i = rO . {} ) )
assume A4: 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 . {} )
A5: i = 1 by A2, A4, FINSEQ_1:2, TARSKI:def 1;
thus ( rO = p . i & <*O*> . i = rO . {} ) by A5, TREES_4:3; :: thesis: verum

end;

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