theorem Th8: :: MSUALG_6:8

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