let v, w be Element of (RealVS V); :: according to RLVECT_1:def 2 :: thesis: v + w = w + v
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 v1 = v, w1 = w as Element of V ;
thus v + w = v1 + w1 by A1
.= w1 + v1
.= w + v by A1 ; :: thesis: verum