let x be VECTOR of (RealVS V); :: according to HAHNBAN:def 3 :: thesis: for b₁ being object holds (CtoR l) . (b₁ * x) = b₁ * ((CtoR l) . x)
let r be Real; :: thesis: (CtoR l) . (r * x) = r * ((CtoR l) . x)
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 x1 = x as Vector of V ;
reconsider r = r as Real ;
[**r,0**] * x1 = r * x by Def17;
hence (CtoR l) . (r * x) = r * ((CtoR l) . x) by Def13; :: thesis: verum