let x, y be Element of (opp K); :: according to RLVECT_1:def 2 :: thesis: x + y = y + x

reconsider a = x, b = y as Element of K ;

thus x + y = a + b

.= b + a

.= y + x ; :: thesis: verum

reconsider a = x, b = y as Element of K ;

thus x + y = a + b

.= b + a

.= y + x ; :: thesis: verum