theorem :: PRALG_3: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 the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const (o,(A . i)) ) holds
f = const (o,(product A))