let M be 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)) )
let R be Equivalence_Relation of M; ( 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 ( ( 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
;
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,(b5 * b7)) = Class (R,(b6 * b8))let v,
v9,
w,
w9 be
Element of
M;
( Class (R,v) = Class (R,v9) & Class (R,w) = Class (R,w9) implies Class (R,(b1 * b3)) = Class (R,(b2 * b4)) )assume A2:
(
Class (
R,
v)
= Class (
R,
v9) &
Class (
R,
w)
= Class (
R,
w9) )
;
Class (R,(b1 * b3)) = Class (R,(b2 * b4))
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))
; 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))
hence
R is compatible
; verum