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