let u, v, w be Element of (RealVS V); :: according to RLVECT_1:def 3 :: thesis: (u + v) + w = u + (v + w)
A1: addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider u1 = u, v1 = v, w1 = w as Element of V ;
thus (u + v) + w = (u1 + v1) + w1 by A1
.= u1 + (v1 + w1) by RLVECT_1:def 3
.= u + (v + w) by A1 ; :: thesis: verum