:: deftheorem Def3 defines MSAlgebra-Class PRALG_3:def 3 :
for I being non empty set
for J being ManySortedSet of I
for S being non empty non void ManySortedSign
for b₄ being ManySortedSet of I holds
( b₄ is MSAlgebra-Class of S,J iff for i being set st i in I holds
b₄ . i is MSAlgebra-Family of J . i,S );