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