let f be non empty FinSequence of NAT ; :: thesis:
let X be set ; :: thesis:
set A = DTConUA (f,X);
set D = (dom f) \/ X;
A1: the carrier of (DTConUA (f,X)) = (Terminals (DTConUA (f,X))) \/ (NonTerminals (DTConUA (f,X))) by LANG1:1;
Terminals (DTConUA (f,X)) misses NonTerminals (DTConUA (f,X)) by DTCONSTR:8;
then A2: (Terminals (DTConUA (f,X))) /\ (NonTerminals (DTConUA (f,X))) = {} ;
thus Terminals (DTConUA (f,X)) c= X :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A3: x in Terminals (DTConUA (f,X)) ; :: thesis:
then reconsider xd = x as Element of (dom f) \/ X by A1, XBOOLE_0:def 3;
reconsider xa = x as Element of the carrier of (DTConUA (f,X)) by A1, A3, XBOOLE_0:def 3;

A4: now :: thesis:

A5: rng f c= NAT by FINSEQ_1:def 4;
assume A6: x in dom f ; :: thesis:
then f . x in rng f by FUNCT_1:def 3;
then reconsider fx = f . x as Nat by A5;
reconsider a = fx |-> xd as FinSequence of (dom f) \/ X ;
reconsider a = a as Element of ((dom f) \/ X) * by FINSEQ_1:def 11;
len a = f . xd by CARD_1:def 7;
then [xd,a] in REL (f,X) by A6, Def7;
then xa ==> a by LANG1:def 1;
then xa in { t where t is Symbol of (DTConUA (f,X)) : ex n being FinSequence st t ==> n } ;
then x in NonTerminals (DTConUA (f,X)) by LANG1:def 3;
hence contradiction by A2, A3, XBOOLE_0:def 4; :: thesis:

end;

x in (dom f) \/ X by A1, A3, XBOOLE_0:def 3;
hence x in X by A4, XBOOLE_0:def 3; :: thesis:

end;

thus NonTerminals (DTConUA (f,X)) c= dom f :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in NonTerminals (DTConUA (f,X)) ; :: thesis:
then x in { t where t is Symbol of (DTConUA (f,X)) : ex n being FinSequence st t ==> n } by LANG1:def 3;
then consider t being Symbol of (DTConUA (f,X)) such that
A7: x = t and
A8: ex n being FinSequence st t ==> n ;
consider n being FinSequence such that
A9: t ==> n by A8;
[t,n] in the Rules of (DTConUA (f,X)) by A9, LANG1:def 1;
then reconsider n = n as Element of ((dom f) \/ X) * by ZFMISC_1:87;
reconsider t = t as Element of (dom f) \/ X ;
[t,n] in REL (f,X) by A9, LANG1:def 1;
hence x in dom f by A7, Def7; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
A10: rng f c= NAT by FINSEQ_1:def 4;
assume A11: x in dom f ; :: thesis:
then reconsider xa = x as Symbol of (DTConUA (f,X)) by XBOOLE_0:def 3;
f . x in rng f by A11, FUNCT_1:def 3;
then reconsider fx = f . x as Nat by A10;
reconsider xd = x as Element of (dom f) \/ X by A11, XBOOLE_0:def 3;
reconsider a = fx |-> xd as FinSequence of (dom f) \/ X ;
reconsider a = a as Element of ((dom f) \/ X) * by FINSEQ_1:def 11;
len a = f . xd by CARD_1:def 7;
then [xd,a] in REL (f,X) by A11, Def7;
then xa ==> a by LANG1:def 1;
then xa in { t where t is Symbol of (DTConUA (f,X)) : ex n being FinSequence st t ==> n } ;
hence x in NonTerminals (DTConUA (f,X)) by LANG1:def 3; :: thesis: