:: deftheorem defines product PRALG_2:def 14 :
for I being set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S holds product A = MSAlgebra(# (SORTS A),(OPS A) #);