theorem Th58: :: ALGSPEC1:58

for S being non void Signature
for E being non empty Signature
for A being MSAlgebra over E st A is Algebra of S holds
for o being OperSymbol of S holds the Charact of A . o is Function of (( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o))