:: deftheorem defines ParsedTermsOSA OSAFREE:def 11 :
for S being OrderSortedSign
for X being V2() ManySortedSet of S holds ParsedTermsOSA X = MSAlgebra(# (ParsedTerms X),(PTOper X) #);