let x be Element of (V *' ); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider f = x as linear-Functional of V by Def14;
reconsider b = - f as Element of (V *' ) by Def14;
take b ; :: according to ALGSTR_0:def 11 :: thesis: x + b = 0. (V *' )
thus x + b = f - f by Def14
.= 0Functional V by Th24
.= 0. (V *' ) by Def14 ; :: thesis: verum