theorem Th2: :: FREEALG:2

for f being non empty FinSequence of NAT
for X being set holds
( Terminals (DTConUA (f,X)) c= X & NonTerminals (DTConUA (f,X)) = dom f )