theorem Th3: :: PRALG_2:3

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for o being OperSymbol of S holds
( Args (o,U0) = product ( the Sorts of U0 * (the_arity_of o)) & dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) )