let x, y, z be Element of (opp K); :: according to RLVECT_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 = (a + b) + c
.= a + (b + c) by RLVECT_1:def 3
.= x + (y + z) ; :: thesis: verum