let x be Element of (opp K); :: according to RLVECT_1:def 4 :: 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 4 ; :: thesis: verum

reconsider a = x as Element of K ;

thus x + (0. (opp K)) = a + (0. K)

.= x by RLVECT_1:def 4 ; :: thesis: verum