let x be Element of ; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider a = x as Element of ;
consider b being Element of such that
A1: a + b = 0. K by ALGSTR_0:def 11;
reconsider y = b as Element of ;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. (opp K)
thus x + y = 0. (opp K) by A1; :: thesis: verum