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

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

hence
ExtendInt r is continuous
by A2, FUNCT_2:63; :: thesis: verum
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;thus g . x = r * (f1 . x) by A1

.= r * x

.= (ExtendInt r) . x by Def1 ; :: thesis: verum