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

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