let x, y, z be Element of (opp K); :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)
reconsider a = x, b = y, c = z as Element of K ;
thus (x * y) * z = c * (b * a) by Lm4
.= (c * b) * a by GROUP_1:def 3
.= x * (y * z) by Lm4 ; :: thesis: verum