reconsider f1 = id I[01] as Function of I[01] ,R^1 by BORSUK_1:83, FUNCT_2:9, TOPMETR:24;
f1 is continuous by PRE_TOPC:56;
then consider g being Function of I[01] ,R^1 such that
A1: for p being Point of I[01]
for r1 being real number st f1 . p = r1 holds
g . p = r * r1 and
A2: g is continuous by JGRAPH_2:33;
for x being Point of I[01] holds g . x = (ExtendInt r) . x
proof
let x be Point of I[01] ; :: thesis: g . x = (ExtendInt r) . x
thus g . x = r * (f1 . x) by A1
.= r * x by FUNCT_1:35
.= (ExtendInt r) . x by Def1 ; :: thesis: verum
end;
hence ExtendInt r is continuous by A2, FUNCT_2:113; :: thesis: verum