:: deftheorem Def13 defines Real_homogeneous HAHNBAN1:def 13 :
for V being non empty ModuleStr over F_Complex
for F being RFunctional of V holds
( F is Real_homogeneous iff for v being Vector of V
for r being Real holds F . ([**r,0**] * v) = r * (F . v) );