theorem Th12: :: PRALG_3:12

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1) holds x in product (doms (F * (the_arity_of o)))