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