theorem Th10: :: PRALG_2:10

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 f being Function st f in dom (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) )