:: deftheorem defines OSSym OSAFREE:def 6 :
for S being OrderSortedSign
for X being V2() ManySortedSet of S
for o being OperSymbol of S holds OSSym (o,X) = [o, the carrier of S];