theorem Th9: :: PRALG_3:9

for I being non empty set
for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
(const (o,(product A))) . i = const (o,(A . i))