theorem Th6: :: MSUALG_3:6

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1 being MSAlgebra over S
for x being Function st x in Args (o,U1) holds
( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds
x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) )