theorem Th24: :: AOFA_A01:24

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