let X, Y be RealLinearSpace; :: thesis: 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; :: thesis: ( f is homogeneous implies not f " {(0. Y)} is empty )

assume A1: f is homogeneous ; :: thesis: 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; :: thesis: verum

not f " {(0. Y)} is empty

let f be Function of X,Y; :: thesis: ( f is homogeneous implies not f " {(0. Y)} is empty )

assume A1: f is homogeneous ; :: thesis: 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; :: thesis: verum