:: deftheorem Def5 defines product PRALG_3:def 5 :
for I being non empty set
for S being non empty non void ManySortedSign
for J being V8() ManySortedSet of I
for C being MSAlgebra-Class of S,J
for b₅ being MSAlgebra-Family of I,S holds
( b₅ = product C iff for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & b₅ . i = product Cs ) );