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)) = {} 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 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

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 5;
then reconsider fx = f . x as Element of 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 FINSEQ_1:def 18;
then [xd,a] in REL f,X by A6, 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) 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 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
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:106;
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, 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) )
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 5;
then reconsider fx = f . x as Element of 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 FINSEQ_1:def 18;
then [xd,a] in REL f,X by A11, 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