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