theorem Th10: :: MSUALG_6:10

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for i being Element of NAT
for A being feasible MSAlgebra over S
for a being Function st a in Args (o,A) holds
transl (o,i,a,A) is Function of ( the Sorts of A . ((the_arity_of o) /. i)),( the Sorts of A . (the_result_sort_of o))