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

suppose A1: not M is empty ; :: thesis: M ./. R is associative

now :: thesis: for X, Y, Z being Element of (M ./. R) holds (X * Y) * Z = X * (Y * Z)

let X, Y, Z be Element of (M ./. R); :: thesis: (X * Y) * Z = X * (Y * Z)
consider x being Element of M such that
A2: X = Class (R,x) by A1, EQREL_1:36;
consider y being Element of M such that
A3: Y = Class (R,y) by A1, EQREL_1:36;
consider z being Element of M such that
A4: Z = Class (R,z) by A1, EQREL_1:36;
A5: ( Class (R,(x * y)) in Class R & Class (R,(y * z)) in Class R ) by A1, EQREL_1:def 3;
thus (X * Y) * Z = (ClassOp R) . ((Class (R,(x * y))),Z) by A1, A2, A3, Def4
.= Class (R,((x * y) * z)) by A1, A4, A5, Def4
.= Class (R,(x * (y * z))) by GROUP_1:def 3
.= (ClassOp R) . (X,(Class (R,(y * z)))) by A1, A2, A5, Def4
.= X * (Y * Z) by A1, A3, A4, Def4 ; :: thesis: verum

end;

hence M ./. R is associative by GROUP_1:def 3; :: thesis: verum

end;

suppose M is empty ; :: thesis: M ./. R is associative

hence M ./. R is associative ; :: thesis: verum

end;

end;