for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over F_Complex
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))