let F be Function of T,R^1; :: thesis: ( F = f (#) r implies F is continuous )
assume A4: F = f (#) r ; :: thesis: F is continuous
consider g being Function of T,R^1 such that
A5: for p being Point of T
for s being Real st f . p = s holds
g . p = r * s and
A6: g is continuous by JGRAPH_2:23;
F = g
proof
let x be Point of T; :: according to FUNCT_2:def 8 :: thesis: F . x = g . x
thus F . x = (f . x) * r by A4, VALUED_1:6
.= g . x by A5 ; :: thesis: verum
end;
hence F is continuous by A6; :: thesis: verum