theorem Th2: :: MSUALG_6:2

for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for o being OperSymbol of S
for a being Function st a in Args (o,A) holds
( dom a = dom (the_arity_of o) & ( for i being set st i in dom (the_arity_of o) holds
a . i in the Sorts of A . ((the_arity_of o) /. i) ) )