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