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