let f be non empty FinSequence of NAT ; :: thesis: for X being set holds
( Terminals (DTConUA (f,X)) c= X & NonTerminals (DTConUA (f,X)) = dom f )
let X be set ; :: thesis: ( Terminals (DTConUA (f,X)) c= X & NonTerminals (DTConUA (f,X)) = dom f )
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: NonTerminals (DTConUA (f,X)) = dom f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Terminals (DTConUA (f,X)) or x in X )
assume A3: x in Terminals (DTConUA (f,X)) ; :: thesis: x in X
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: not x in dom f

A5: rng f c= NAT by FINSEQ_1:def 4;
assume A6: x in dom f ; :: thesis: contradiction
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: verum

end;

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

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NonTerminals (DTConUA (f,X)) or x in dom f )
assume x in NonTerminals (DTConUA (f,X)) ; :: thesis: x in dom f
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: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in NonTerminals (DTConUA (f,X)) )
A10: rng f c= NAT by FINSEQ_1:def 4;
assume A11: x in dom f ; :: thesis: x in NonTerminals (DTConUA (f,X))
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: verum