reconsider A = [.0,1.] as non empty Subset of R^1 by TOPMETR:17, XXREAL_1:1;
set X = [:I[01],I[01]:];
let f1, f2 be Function of [:I[01],I[01]:],I[01]; :: thesis:
assume that
A1: ( f1 is continuous & f2 is continuous ) and
A2: for p being Point of [:I[01],I[01]:] holds (f1 . p) + (f2 . p) is Point of I[01] ; :: thesis:
reconsider f19 = f1, f29 = f2 as Function of [:I[01],I[01]:],R^1 by BORSUK_1:40, FUNCT_2:7, TOPMETR:17;
( f19 is continuous & f29 is continuous ) by A1, PRE_TOPC:26;
then consider g being Function of [:I[01],I[01]:],R^1 such that
A3: for p being Point of [:I[01],I[01]:]
for r1, r2 being Real st f19 . p = r1 & f29 . p = r2 holds
g . p = r1 + r2 and
A4: g is continuous by JGRAPH_2:19;
A5: rng g c= [.0,1.]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng g ; :: thesis:
then consider y being object such that
A6: y in dom g and
A7: x = g . y by FUNCT_1:def 3;
reconsider y = y as Point of [:I[01],I[01]:] by A6;
g . y = (f1 . y) + (f2 . y) by A3;
then g . y is Point of I[01] by A2;
hence x in [.0,1.] by A7, BORSUK_1:40; :: thesis:

end;

( [.0,1.] = the carrier of (R^1 | A) & dom g = the carrier of [:I[01],I[01]:] ) by FUNCT_2:def 1, PRE_TOPC:8;
then reconsider g = g as Function of [:I[01],I[01]:],(R^1 | A) by A5, FUNCT_2:2;
R^1 | A = I[01] by BORSUK_1:def 13, TOPMETR:def 6;
then reconsider g = g as continuous Function of [:I[01],I[01]:],I[01] by A4, JGRAPH_1:45;
take g ; :: thesis:
thus ( ( for p being Point of [:I[01],I[01]:]
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 + r2 ) & g is continuous ) by A3; :: thesis: