let v be Element of (RealVS V); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
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 ;
consider w1 being Element of V such that
A2: v1 + w1 = 0. V by ALGSTR_0:def 11;
reconsider w = w1 as Element of (RealVS V) by A1;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. (RealVS V)
thus v + w = 0. (RealVS V) by A1, A2; :: thesis: verum