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)
A1: (TOP-REAL n) --> (0. (TOP-REAL n)) = the carrier of (TOP-REAL n) --> (0. (TOP-REAL n)) ;
hence ((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 A1, FUNCOP_1:13 ;
:: thesis: verum

end;

let x, y be Point of (TOP-REAL n); :: according to TOPREAL9:def 5 :: thesis: ((TOP-REAL n) --> (0. (TOP-REAL n))) . (x + y) = (((TOP-REAL n) --> (0. (TOP-REAL n))) . x) + (((TOP-REAL n) --> (0. (TOP-REAL n))) . y)
A2: (TOP-REAL n) --> (0. (TOP-REAL n)) = the carrier of (TOP-REAL n) --> (0. (TOP-REAL n)) ;
hence ((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 A2, FUNCOP_1:13
.= (((TOP-REAL n) --> (0. (TOP-REAL n))) . x) + (((TOP-REAL n) --> (0. (TOP-REAL n))) . y) by A2, FUNCOP_1:13 ;
:: thesis: verum