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

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