:: deftheorem Def3 defines homogeneous HAHNBAN:def 3 :
for V being RealLinearSpace
for IT being Functional of V holds
( IT is homogeneous iff for x being VECTOR of V
for r being Real holds IT . (r * x) = r * (IT . x) );