thus for x, y, z being Element of (opp K) holds x + (y + z) = (x + y) + z by Lm2; :: according to RLVECT_1:def 3 :: thesis: ( opp K is right_zeroed & opp K is right_complementable )
thus for x being Element of (opp K) holds x + (0. (opp K)) = x by Lm2; :: according to RLVECT_1:def 4 :: thesis: opp K is right_complementable
let a be Element of (opp K); :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
reconsider x = a as Element of K ;
reconsider y = - x as Element of (opp K) ;
take y ; :: according to ALGSTR_0:def 11 :: thesis: a + y = 0. (opp K)
thus a + y = x + (- x)
.= 0. (opp K) by RLVECT_1:5 ; :: thesis: verum