:: deftheorem Def18 defines Reverse MSAFREE:def 18 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for b₃ being ManySortedFunction of FreeGen X,X holds
( b₃ = Reverse X iff for s being SortSymbol of S holds b₃ . s = Reverse (s,X) );