set TR = TOP-REAL n;

_{1} being Function of (TOP-REAL n),(TOP-REAL n) st b_{1} = f * g holds

b_{1} is homogeneous
; :: thesis: verum

now :: thesis: for r being Real

for p being Point of (TOP-REAL n) holds (f * g) . (r * p) = r * ((f * g) . p)

hence
for bfor p being Point of (TOP-REAL n) holds (f * g) . (r * p) = r * ((f * g) . p)

let r be Real; :: thesis: for p being Point of (TOP-REAL n) holds (f * g) . (r * p) = r * ((f * g) . p)

let p be Point of (TOP-REAL n); :: thesis: (f * g) . (r * p) = r * ((f * g) . p)

reconsider gp = g . p as Point of (TOP-REAL n) ;

A1: dom (f * g) = the carrier of (TOP-REAL n) by FUNCT_2:52;

hence (f * g) . (r * p) = f . (g . (r * p)) by FUNCT_1:12

.= f . (r * gp) by TOPREAL9:def 4

.= r * (f . gp) by TOPREAL9:def 4

.= r * ((f * g) . p) by A1, FUNCT_1:12 ;

:: thesis: verum

end;let p be Point of (TOP-REAL n); :: thesis: (f * g) . (r * p) = r * ((f * g) . p)

reconsider gp = g . p as Point of (TOP-REAL n) ;

A1: dom (f * g) = the carrier of (TOP-REAL n) by FUNCT_2:52;

hence (f * g) . (r * p) = f . (g . (r * p)) by FUNCT_1:12

.= f . (r * gp) by TOPREAL9:def 4

.= r * (f . gp) by TOPREAL9:def 4

.= r * ((f * g) . p) by A1, FUNCT_1:12 ;

:: thesis: verum

b