let v, w be Element of (V *'); :: according to RLVECT_1:def 2 :: thesis: v + w = w + v
reconsider f = v, g = w as linear-Functional of V by Def10;
thus v + w = f + g by Def10
.= g + f by Th10
.= w + v by Def10 ; :: thesis: verum