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