theorem Th2: :: ALGSTR_4:2

for M being multMagma
for R being Equivalence_Relation of M holds
( R is compatible iff for v, v9, w, w9 being Element of M st Class (R,v) = Class (R,v9) & Class (R,w) = Class (R,w9) holds
Class (R,(v * w)) = Class (R,(v9 * w9)) )