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₄))

hence Class (R,(v * w)) = {}
.= 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:23;
then v * w in Class (R,(v9 * w9)) by A1;
hence Class (R,(v * w)) = Class (R,(v9 * w9)) by EQREL_1:23; :: 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:23;
then Class (R,(v * w)) = Class (R,(v9 * w9)) by A4;
hence v * w in Class (R,(v9 * w9)) by A6, EQREL_1:23; :: thesis: verum

end;

end;

end;

hence R is compatible ; :: thesis: verum