theorem Th3: :: MSUALG_6:3

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being MSAlgebra over S holds
( Args (o,A) <> {} iff for i being Element of NAT st i in dom (the_arity_of o) holds
the Sorts of A . ((the_arity_of o) /. i) <> {} )