let X be RealUnitarySpace; :: thesis: for f being Function of X,REAL st f is homogeneous holds
not f " {0} is empty
let f be Function of X,REAL; :: thesis: ( f is homogeneous implies not f " {0} is empty )
assume A1: f is homogeneous ; :: thesis: not f " {0} is empty
f . (0. X) = f . (0 * (0. X))
.= 0 * (f . (0. X)) by A1, HAHNBAN:def 3
.= 0 ;
then f . (0. X) in {0} by TARSKI:def 1;
hence not f " {0} is empty by FUNCT_2:38; :: thesis: verum