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