let v, w be Element of (RealVS V); :: according to RLVECT_1:def 5 :: thesis: v + w = w + v
A1: addLoopStr(# the carrier of V,the addF of V,the U2 of V #) = addLoopStr(# the carrier of (RealVS V),the addF of (RealVS V),the U2 of (RealVS V) #) by Def22;
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