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)) & Terminals (DTConUA f,X) misses NonTerminals (DTConUA f,X) ) by DTCONSTR:8, LANG1:1;
then A2: (Terminals (DTConUA f,X)) /\ (NonTerminals (DTConUA f,X)) = {} by XBOOLE_0:def 7;
thus Terminals (DTConUA f,X) c= X :: thesis: NonTerminals (DTConUA f,X) = dom f

proof

let x be set ; :: 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 A4: x in (dom f) \/ X by A1, XBOOLE_0:def 3;
reconsider xd = x as Element of (dom f) \/ X by A1, A3, XBOOLE_0:def 3;
reconsider xa = x as Element of the carrier of (DTConUA f,X) by A1, A3, XBOOLE_0:def 3;

now

assume A5: x in dom f ; :: thesis: contradiction
then ( f . x in rng f & rng f c= NAT ) by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider fx = f . x as Element of NAT ;
reconsider a = fx |-> xd as FinSequence of (dom f) \/ X by FINSEQ_2:77;
reconsider a = a as Element of ((dom f) \/ X) * by FINSEQ_1:def 11;
len a = f . xd by FINSEQ_2:69;
then ( [xd,a] in REL f,X & xd = xa ) by A5, Def8;
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) & xa = x ) by LANG1:def 3;
hence contradiction by A2, A3, XBOOLE_0:def 4; :: thesis: verum

end;

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 set ; :: 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
A6: ( x = t & ex n being FinSequence st t ==> n ) ;
consider n being FinSequence such that
A7: t ==> n by A6;
A8: [t,n] in the Rules of (DTConUA f,X) by A7, LANG1:def 1;
reconsider t = t as Element of (dom f) \/ X ;
reconsider n = n as Element of ((dom f) \/ X) * by A8, ZFMISC_1:106;
[t,n] in REL f,X by A7, LANG1:def 1;
hence x in dom f by A6, Def8; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in NonTerminals (DTConUA f,X) )
assume A9: 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;
reconsider xd = x as Element of (dom f) \/ X by A9, XBOOLE_0:def 3;
( f . x in rng f & rng f c= NAT ) by A9, FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider fx = f . x as Element of NAT ;
reconsider a = fx |-> xd as FinSequence of (dom f) \/ X by FINSEQ_2:77;
reconsider a = a as Element of ((dom f) \/ X) * by FINSEQ_1:def 11;
len a = f . xd by FINSEQ_2:69;
then ( [xd,a] in REL f,X & xd = xa ) by A9, Def8;
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