set A = DTConUA (f,D);
A1: NonTerminals (DTConUA (f,D)) = dom f by Th2;
A2: Terminals (DTConUA (f,D)) = D by Th3;
DTConUA (f,D) is with_useful_nonterminals

proof

set d = the Element of D;
let s be Symbol of (DTConUA (f,D)); :: according to DTCONSTR:def 5 :: thesis: ( not s in NonTerminals (DTConUA (f,D)) or ex b₁ being FinSequence of TS (DTConUA (f,D)) st s ==> roots b₁ )
reconsider sd = the Element of D as Symbol of (DTConUA (f,D)) by XBOOLE_0:def 3;
A3: rng f c= NAT by FINSEQ_1:def 4;
assume A4: s in NonTerminals (DTConUA (f,D)) ; :: thesis: ex b₁ being FinSequence of TS (DTConUA (f,D)) st s ==> roots b₁
then f . s in rng f by A1, FUNCT_1:def 3;
then reconsider fs = f . s as Nat by A3;
reconsider sdd = s as Element of (dom f) \/ D ;
set p = fs |-> (root-tree sd);
A5: len (fs |-> (root-tree sd)) = fs by CARD_1:def 7;
A6: root-tree sd in TS (DTConUA (f,D)) by A2, DTCONSTR:def 1;
A7: rng (fs |-> (root-tree sd)) c= TS (DTConUA (f,D))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (fs |-> (root-tree sd)) or y in TS (DTConUA (f,D)) )
assume y in rng (fs |-> (root-tree sd)) ; :: thesis: y in TS (DTConUA (f,D))
then consider n being Nat such that
A8: n in dom (fs |-> (root-tree sd)) and
A9: (fs |-> (root-tree sd)) . n = y by FINSEQ_2:10;
n in Seg (len (fs |-> (root-tree sd))) by A8, FINSEQ_1:def 3;
hence y in TS (DTConUA (f,D)) by A6, A5, A9, FUNCOP_1:7; :: thesis: verum

end;

dom (roots (fs |-> (root-tree sd))) = dom (fs |-> (root-tree sd)) by TREES_3:def 18
.= Seg (len (fs |-> (root-tree sd))) by FINSEQ_1:def 3 ;
then A10: len (roots (fs |-> (root-tree sd))) = fs by A5, FINSEQ_1:def 3;
reconsider p = fs |-> (root-tree sd) as FinSequence of TS (DTConUA (f,D)) by A7, FINSEQ_1:def 4;
take p ; :: thesis: s ==> roots p
reconsider p = p as FinSequence of FinTrees the carrier of (DTConUA (f,D)) ;
reconsider rp = roots p as Element of ((dom f) \/ D) * by FINSEQ_1:def 11;
[sdd,rp] in REL (f,D) by A1, A4, A10, Def7;
hence s ==> roots p by LANG1:def 1; :: thesis: verum

end;

hence ( DTConUA (f,D) is with_terminals & DTConUA (f,D) is with_nonterminals & DTConUA (f,D) is with_useful_nonterminals ) by A2; :: thesis: verum