:: deftheorem Def4 defines ClassOp ALGSTR_4:def 4 :
for M being multMagma
for R being compatible Equivalence_Relation of M
for b₃ being BinOp of (Class R) holds
( ( not M is empty implies ( b₃ = ClassOp R iff for x, y being Element of Class R
for v, w being Element of M st x = Class (R,v) & y = Class (R,w) holds
b₃ . (x,y) = Class (R,(v * w)) ) ) & ( M is empty implies ( b₃ = ClassOp R iff b₃ = {} ) ) );