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