let M be multMagma ; :: thesis: for R being Equivalence_Relation of holds
( R is compatible iff for v, v', w, w' being Element of st Class R,v = Class R,v' & Class R,w = Class R,w' holds
Class R,(v * w) = Class R,(v' * w') )
let R be Equivalence_Relation of ; :: thesis: ( R is compatible iff for v, v', w, w' being Element of st Class R,v = Class R,v' & Class R,w = Class R,w' holds
Class R,(v * w) = Class R,(v' * w') )

hereby :: thesis: ( ( for v, v', w, w' being Element of st Class R,v = Class R,v' & Class R,w = Class R,w' holds
Class R,(v * w) = Class R,(v' * w') ) implies R is compatible )

assume A1: R is compatible ; :: thesis: for v, v', w, w' being Element of st Class R,v = Class R,v' & Class R,w = Class R,w' holds
Class R,(b₅ * b₇) = Class R,(b₆ * b₈)
let v, v', w, w' be Element of ; :: thesis: ( Class R,v = Class R,v' & Class R,w = Class R,w' implies Class R,(b₁ * b₃) = Class R,(b₂ * b₄) )
assume A2: ( Class R,v = Class R,v' & Class R,w = Class R,w' ) ; :: 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,(v' * w') by A3 ; :: thesis: verum

end;

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

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

end;

end;

end;

assume A4: for v, v', w, w' being Element of st Class R,v = Class R,v' & Class R,w = Class R,w' holds
Class R,(v * w) = Class R,(v' * w') ; :: thesis: R is compatible
for v, v', w, w' being Element of st v in Class R,v' & w in Class R,w' holds
v * w in Class R,(v' * w')

proof

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

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

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

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

end;

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

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

end;

end;

end;

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