let M be multMagma ; :: thesis: ( M is empty implies M is associative )
assume M is empty ; :: thesis: M is associative
then AA: the carrier of M is empty ;

now :: thesis: for x, y, z being Element of M holds (x * y) * z = x * (y * z)

let x, y, z be Element of M; :: thesis: (x * y) * z = x * (y * z)
thus (x * y) * z = {} by AA
.= the multF of M . [x,(y * z)] by AA
.= x * (y * z) ; :: thesis: verum

end;

hence M is associative ; :: thesis: verum