let x be Element of (V *' ); :: according to RLVECT_1:def 7 :: thesis: x + (0. (V *' )) = x
reconsider f = x as linear-Functional of V by Def14;
thus x + (0. (V *' )) = the addF of (V *' ) . x,(0Functional V) by Def14
.= f + (0Functional V) by Def14
.= x by Th23 ; :: thesis: verum