let M be multMagma ; :: thesis: 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) )
let R be Equivalence_Relation of M; :: thesis: ( 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) )

hereby :: thesis: ( ( 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) ) implies R is compatible )

assume A1: R is compatible ; :: thesis: 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,(b₅ * b₇) = Class R,(b₆ * b₈)
let v, v9, w, w9 be Element of M; :: thesis: ( Class R,v = Class R,v9 & Class R,w = Class R,w9 implies Class R,(b₁ * b₃) = Class R,(b₂ * b₄) )
assume A2: ( Class R,v = Class R,v9 & Class R,w = Class R,w9 ) ; :: thesis: Class R,(b₁ * b₃) = Class R,(b₂ * b₄)

per cases ( M is empty or not M is empty ) ;

suppose A3: M is empty ; :: thesis: Class R,(b₁ * b₃) = Class R,(b₂ * b₄)

thus Class R,(v * w) = {} by A3
.= Class R,(v9 * w9) by A3 ; :: thesis: verum

end;

suppose not M is empty ; :: thesis: Class R,(b₁ * b₃) = Class R,(b₂ * b₄)

then ( v in Class R,v9 & w in Class R,w9 ) by A2, EQREL_1:31;
then v * w in Class R,(v9 * w9) by A1, Def4;
hence Class R,(v * w) = Class R,(v9 * w9) by EQREL_1:31; :: thesis: verum

end;

end;

end;

assume A4: 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) ; :: thesis: R is compatible
for v, v9, w, w9 being Element of M st v in Class R,v9 & w in Class R,w9 holds
v * w in Class R,(v9 * w9)

proof

let v, v9, w, w9 be Element of M; :: thesis: ( v in Class R,v9 & w in Class R,w9 implies v * w in Class R,(v9 * w9) )
assume A5: ( v in Class R,v9 & w in Class R,w9 ) ; :: thesis: v * w in Class R,(v9 * w9)

per cases ( M is empty or not M is empty ) ;

suppose M is empty ; :: thesis: v * w in Class R,(v9 * w9)

hence v * w in Class R,(v9 * w9) by A5; :: thesis: verum

end;

suppose A6: not M is empty ; :: thesis: v * w in Class R,(v9 * w9)

( Class R,v9 = Class R,v & Class R,w9 = Class R,w ) by A5, EQREL_1:31;
then Class R,(v * w) = Class R,(v9 * w9) by A4;
hence v * w in Class R,(v9 * w9) by A6, EQREL_1:31; :: thesis: verum

end;

end;

end;

hence R is compatible by Def4; :: thesis: verum