theorem Th23: :: AOFA_A01:23

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)*>