let x be Vector of V; :: according to HAHNBAN1:def 18 :: thesis: for r being Real holds (RtoC l) . ([**r,0 **] * x) = r * ((RtoC l) . x)
let r be Real; :: thesis: (RtoC l) . ([**r,0 **] * x) = r * ((RtoC l) . x)
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 as VECTOR of (RealVS V) ;
[**r,0 **] * x = r * x1 by Def22;
hence (RtoC l) . ([**r,0 **] * x) = r * ((RtoC l) . x) by HAHNBAN:def 5; :: thesis: verum