set f = (TOP-REAL n) --> (0. (TOP-REAL n));
thus (TOP-REAL n) --> (0. (TOP-REAL n)) is homogeneous :: thesis: (TOP-REAL n) --> (0. (TOP-REAL n)) is additive

proof

let r be real number ; :: according to TOPREAL9:def 4 :: thesis: for x being Point of (TOP-REAL n) holds ((TOP-REAL n) --> (0. (TOP-REAL n))) . (r * x) = r * (((TOP-REAL n) --> (0. (TOP-REAL n))) . x)
let x be Point of (TOP-REAL n); :: thesis: ((TOP-REAL n) --> (0. (TOP-REAL n))) . (r * x) = r * (((TOP-REAL n) --> (0. (TOP-REAL n))) . x)
thus ((TOP-REAL n) --> (0. (TOP-REAL n))) . (r * x) = 0. (TOP-REAL n) by FUNCOP_1:13
.= r * (0. (TOP-REAL n)) by EUCLID:32
.= r * (((TOP-REAL n) --> (0. (TOP-REAL n))) . x) by FUNCOP_1:13 ; :: thesis: verum

end;

let x, y be Point of (TOP-REAL n); :: according to GRCAT_1:def 13 :: thesis: ((TOP-REAL n) --> (0. (TOP-REAL n))) . K375((TOP-REAL n),x,y) = K375((TOP-REAL n),(((TOP-REAL n) --> (0. (TOP-REAL n))) . x),(((TOP-REAL n) --> (0. (TOP-REAL n))) . y))
thus ((TOP-REAL n) --> (0. (TOP-REAL n))) . (x + y) = 0. (TOP-REAL n) by FUNCOP_1:13
.= (0. (TOP-REAL n)) + (0. (TOP-REAL n)) by EUCLID:31
.= (((TOP-REAL n) --> (0. (TOP-REAL n))) . x) + (0. (TOP-REAL n)) by FUNCOP_1:13
.= (((TOP-REAL n) --> (0. (TOP-REAL n))) . x) + (((TOP-REAL n) --> (0. (TOP-REAL n))) . y) by FUNCOP_1:13 ; :: thesis: verum