let x be Element of (opp K); :: according to RLVECT_1:def 7 :: thesis: x + (0. (opp K)) = x
reconsider a = x as Element of K ;
thus x + (0. (opp K)) = a + (0. K)
.= x by RLVECT_1:def 7 ; :: thesis: verum