let A be non empty set ; :: thesis: RAlgebra A is right_complementable
let x be Element of (RAlgebra A); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider f = x as Element of Funcs A,REAL ;
set h = (RealFuncExtMult A) . [(- 1),f];
reconsider t = (RealFuncExtMult A) . [(- 1),f] as Element of (RAlgebra A) ;
take t ; :: according to ALGSTR_0:def 11 :: thesis: x + t = 0. (RAlgebra A)
thus x + t = 0. (RAlgebra A) by Th22; :: thesis: verum