let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr of F_Complex ; :: thesis: for F being RFunctional of V st F is Real_homogeneous holds
for v being Vector of V
for r being Real holds F . ([**0 ,r**] * v) = r * (F . (i_FC * v))
let F be RFunctional of V; :: thesis: ( F is Real_homogeneous implies for v being Vector of V
for r being Real holds F . ([**0 ,r**] * v) = r * (F . (i_FC * v)) )
assume A1: F is Real_homogeneous ; :: thesis: for v being Vector of V
for r being Real holds F . ([**0 ,r**] * v) = r * (F . (i_FC * v))
let v be Vector of V; :: thesis: for r being Real holds F . ([**0 ,r**] * v) = r * (F . (i_FC * v))
let r be Real; :: thesis: F . ([**0 ,r**] * v) = r * (F . (i_FC * v))
thus F . ([**0 ,r**] * v) = F . (([**r,0 **] * i_FC ) * v)
.= F . ([**r,0 **] * (i_FC * v)) by VECTSP_1:def 28, VECTSP_1:def 29
.= r * (F . (i_FC * v)) by A1, Def18 ; :: thesis: verum