let X, Y be RealLinearSpace; for f being Function of X,Y st f is homogeneous holds
not f " {(0. Y)} is empty
let f be Function of X,Y; ( f is homogeneous implies not f " {(0. Y)} is empty )
assume A1:
f is homogeneous
; not f " {(0. Y)} is empty
f . (0. X) =
f . (0 * (0. X))
by RLVECT_1:10
.=
0 * (f . (0. X))
by A1, LOPBAN_1:def 5
.=
0. Y
by RLVECT_1:10
;
then
f . (0. X) in {(0. Y)}
by TARSKI:def 1;
hence
not f " {(0. Y)} is empty
by FUNCT_2:38; verum