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