for S being non empty non void ManySortedSign
for a, b being SortSymbol of S
for o being OperSymbol of S st the_arity_of o = <*a,b*> holds
for A being MSAlgebra over S holds Args (o,A) = product <*( the Sorts of A . a),( the Sorts of A . b)*>