:: deftheorem defines NHReverse OSAFREE:def 30 :
for S being locally_directed OrderSortedSign
for X being V2() ManySortedSet of S
for b₃ being ManySortedFunction of OSFreeGen X, PTVars X holds
( b₃ = NHReverse X iff for s being Element of S holds b₃ . s = NHReverse (s,X) );