:: deftheorem defines ./. ALGSTR_4:def 5 :
for M being multMagma
for R being compatible Equivalence_Relation of M holds M ./. R = multMagma(# (Class R),(ClassOp R) #);