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