theorem Th7: :: MSUALG_6:7

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being MSAlgebra over S
for a being Function st a in Args (o,A) holds
for i being Nat
for x being Element of A,((the_arity_of o) /. i) holds a +* (i,x) in Args (o,A)