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 5 :: 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 3;
then reconsider fs = f . s as 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 object such that
A3: x in dom f and
A4: f . x = 0 by FUNCT_1:def 3;
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 CARD_1:def 7;
len re = 0 by DTCONSTR:3;
then [s0,(roots (<*> (TS (DTConUA (f,X)))))] in the Rules of (DTConUA (f,X)) by A3, A4, Def7;
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 1;
A8: rng (fs |-> (s0 -tree (<*> (TS (DTConUA (f,X)))))) c= TS (DTConUA (f,X))

proof

let y be object ; :: 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:10;
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:7; :: 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, Def7;
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