let x, y be Vector of V; :: according to HAHNBAN1:def 12 :: thesis: (RtoC l) . (x + y) = ((RtoC l) . x) + ((RtoC l) . y)
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 x1 = x, y1 = y as VECTOR of (RealVS V) ;
x + y = x1 + y1 by A1;
hence (RtoC l) . (x + y) = ((RtoC l) . x) + ((RtoC l) . y) by HAHNBAN:def 2; :: thesis: verum