let M be MidSp; :: thesis: for a, b, c being Element of M holds (a @ b) @ c = (a @ c) @ (b @ c)
let a, b, c be Element of M; :: thesis: (a @ b) @ c = (a @ c) @ (b @ c)
(a @ b) @ c = (a @ b) @ (c @ c) by Def4
.= (a @ c) @ (b @ c) by Def4 ;
hence (a @ b) @ c = (a @ c) @ (b @ c) ; :: thesis: verum