let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over 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 16
.= r * (F . (i_FC * v)) by A1 ; :: thesis: verum