for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for a being set
for r being SortSymbol of S st o is_of_type a,r holds
( Den (o,A) is Function of (( the Sorts of A #) . a),( the Sorts of A . r) & Args (o,A) = ( the Sorts of A #) . a & Result (o,A) = the Sorts of A . r )