:: deftheorem Def15 defines @ FREEALG:def 15 :
for f being non empty FinSequence of NAT
for D being set
for s being Symbol of (DTConUA (f,D)) st ex p being FinSequence st s ==> p holds
@ s = s;