let x, y be Vector of V; :: according to HAHNBAN1:def 17 :: thesis: (RtoC l) . (x + y) = ((RtoC l) . x) + ((RtoC l) . y)
A1: addLoopStr(# the carrier of V,the addF of V,the U2 of V #) = addLoopStr(# the carrier of (RealVS V),the addF of (RealVS V),the U2 of (RealVS V) #) by Def22;
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 4; :: thesis: verum