:: deftheorem Def8 defines ParsedTerms OSAFREE:def 8 :
for S being OrderSortedSign
for X being V2() ManySortedSet of S
for b₃ being OrderSortedSet of S holds
( b₃ = ParsedTerms X iff for s being Element of S holds b₃ . s = ParsedTerms (X,s) );