theorem Th15: :: PRALG_3:15

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 x being Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
x . n in product (Carrier (A,((the_arity_of o) /. n)))