set f = (TOP-REAL n) --> (0.REAL n);
thus (TOP-REAL n) --> (0.REAL n) is homogeneous :: thesis: (TOP-REAL n) --> (0.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.REAL n)) . (r * x) = r * (((TOP-REAL n) --> (0.REAL n)) . x)
let x be Point of (TOP-REAL n); :: thesis: ((TOP-REAL n) --> (0.REAL n)) . (r * x) = r * (((TOP-REAL n) --> (0.REAL n)) . x)
A1: (TOP-REAL n) --> (0.REAL n) = the carrier of (TOP-REAL n) --> (0.REAL n) by BORSUK_1:def 2;
hence ((TOP-REAL n) --> (0.REAL n)) . (r * x) = 0.REAL n by FUNCOP_1:13
.= r * (0.REAL n) by EUCLID:32
.= r * (((TOP-REAL n) --> (0.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.REAL n)) . (x + y) = (((TOP-REAL n) --> (0.REAL n)) . x) + (((TOP-REAL n) --> (0.REAL n)) . y)
A2: (TOP-REAL n) --> (0.REAL n) = the carrier of (TOP-REAL n) --> (0.REAL n) by BORSUK_1:def 2;
hence ((TOP-REAL n) --> (0.REAL n)) . (x + y) = 0.REAL n by FUNCOP_1:13
.= (0.REAL n) + (0.REAL n) by EUCLID:31
.= (((TOP-REAL n) --> (0.REAL n)) . x) + (0.REAL n) by A2, FUNCOP_1:13
.= (((TOP-REAL n) --> (0.REAL n)) . x) + (((TOP-REAL n) --> (0.REAL n)) . y) by A2, FUNCOP_1:13 ;
:: thesis: verum