set A = DTConUA f,X;
set D = (dom f) \/ X;
DTConUA f,X is with_useful_nonterminals

proof

set e = <*> (TS (DTConUA f,X));
let s be Symbol of (DTConUA f,X); :: according to DTCONSTR:def 8 :: thesis: ( not s in NonTerminals (DTConUA f,X) or ex b₁ being FinSequence of TS (DTConUA f,X) st s ==> roots b₁ )
assume A1: s in NonTerminals (DTConUA f,X) ; :: thesis: ex b₁ being FinSequence of TS (DTConUA f,X) st s ==> roots b₁
A2: rng f c= NAT by FINSEQ_1:def 4;
NonTerminals (DTConUA f,X) = dom f by Th2;
then f . s in rng f by A1, FUNCT_1:def 5;
then reconsider fs = f . s as Element of NAT by A2;
reconsider sd = s as Element of (dom f) \/ X ;
roots (<*> (TS (DTConUA f,X))) = <*> ((dom f) \/ X) by DTCONSTR:3;
then reconsider re = roots (<*> (TS (DTConUA f,X))) as Element of ((dom f) \/ X) * ;
0 in rng f by Def2;
then consider x being set such that
A3: x in dom f and
A4: f . x = 0 by FUNCT_1:def 5;
A5: NonTerminals (DTConUA f,X) = dom f by Th2;
then reconsider s0 = x as Symbol of (DTConUA f,X) by A3;
set p = fs |-> (s0 -tree (<*> (TS (DTConUA f,X))));
A6: len (fs |-> (s0 -tree (<*> (TS (DTConUA f,X))))) = fs by FINSEQ_1:def 18;
len re = 0 by DTCONSTR:3;
then [s0,(roots (<*> (TS (DTConUA f,X))))] in the Rules of (DTConUA f,X) by A3, A4, Def8;
then s0 ==> roots (<*> (TS (DTConUA f,X))) by LANG1:def 1;
then A7: s0 -tree (<*> (TS (DTConUA f,X))) in TS (DTConUA f,X) by DTCONSTR:def 4;
A8: rng (fs |-> (s0 -tree (<*> (TS (DTConUA f,X))))) c= TS (DTConUA f,X)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (fs |-> (s0 -tree (<*> (TS (DTConUA f,X))))) or y in TS (DTConUA f,X) )
assume y in rng (fs |-> (s0 -tree (<*> (TS (DTConUA f,X))))) ; :: thesis: y in TS (DTConUA f,X)
then A9: ex n being Nat st
( n in dom (fs |-> (s0 -tree (<*> (TS (DTConUA f,X))))) & (fs |-> (s0 -tree (<*> (TS (DTConUA f,X))))) . n = y ) by FINSEQ_2:11;
dom (fs |-> (s0 -tree (<*> (TS (DTConUA f,X))))) = Seg (len (fs |-> (s0 -tree (<*> (TS (DTConUA f,X)))))) by FINSEQ_1:def 3;
hence y in TS (DTConUA f,X) by A7, A6, A9, FUNCOP_1:13; :: thesis: verum

end;

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

end;

hence ( DTConUA f,X is with_nonterminals & DTConUA f,X is with_useful_nonterminals ) ; :: thesis: verum