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

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