reconsider f1 = id I[01] as Function of I[01],R^1 by BORSUK_1:40, FUNCT_2:7, TOPMETR:17;
f1 is continuous by PRE_TOPC:26;
then consider g being Function of I[01],R^1 such that
A1: for p being Point of I[01]
for r1 being Real st f1 . p = r1 holds
g . p = r * r1 and
A2: g is continuous by JGRAPH_2:23;
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
.= (ExtendInt r) . x by Def1 ; :: thesis: verum
end;
hence ExtendInt r is continuous by A2, FUNCT_2:63; :: thesis: verum