for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for x being set
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for a being SortSymbol of S st x in (NForms R) . a holds
nf (x,(R . a)) = x