:: deftheorem defines DTConUA FREEALG:def 8 :
for f being non empty FinSequence of NAT
for X being set holds DTConUA (f,X) = DTConstrStr(# ((dom f) \/ X),(REL (f,X)) #);