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