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