:: deftheorem HDef8 defines homogeneous ZMODLAT1:def 22 :
for V being non empty ModuleStr over INT.Ring
for F being FrFunctional of V holds
( F is homogeneous iff for x being Vector of V
for r being Scalar of holds F . (r * x) = r * (F . x) );