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