:: deftheorem Def4 defines / PRALG_3:def 4 :
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for EqR being Equivalence_Relation of I
for b₅ being MSAlgebra-Class of S, id (Class EqR) holds
( b₅ = A / EqR iff for c being set st c in Class EqR holds
b₅ . c = A | c );