theorem Th16: :: PRALG_3:16

for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for i being Element of I
for n being set st n in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s