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 Def10;
reconsider b = - f as Element of (V *') by Def10;
take b ; :: according to ALGSTR_0:def 11 :: thesis: x + b = 0. (V *')
thus x + b = f - f by Def10
.= 0Functional V by Th14
.= 0. (V *') by Def10 ; :: thesis: verum