let x be Element of (opp K); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable

reconsider a = x as Element of K ;

consider b being Element of K such that

A1: a + b = 0. K by ALGSTR_0:def 11;

reconsider y = b as Element of (opp K) ;

take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. (opp K)

thus x + y = 0. (opp K) by A1; :: thesis: verum

reconsider a = x as Element of K ;

consider b being Element of K such that

A1: a + b = 0. K by ALGSTR_0:def 11;

reconsider y = b as Element of (opp K) ;

take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. (opp K)

thus x + y = 0. (opp K) by A1; :: thesis: verum