let f1, f2 be Function of [:I[01] ,I[01] :],I[01] ; :: thesis:
assume A1: ( f1 is continuous & f2 is continuous & ( for p being Point of [:I[01] ,I[01] :] holds (f1 . p) * (f2 . p) is Point of I[01] ) ) ; :: thesis:
set X = [:I[01] ,I[01] :];
reconsider f1' = f1, f2' = f2 as Function of [:I[01] ,I[01] :],R^1 by BORSUK_1:83, FUNCT_2:9, TOPMETR:24;
( f1' is continuous & f2' is continuous ) by A1, PRE_TOPC:56;
then consider g being Function of [:I[01] ,I[01] :],R^1 such that
A2: ( ( for p being Point of [:I[01] ,I[01] :]
for r1, r2 being real number st f1' . p = r1 & f2' . p = r2 holds
g . p = r1 * r2 ) & g is continuous ) by JGRAPH_2:35;
reconsider A = [.0 ,1.] as non empty Subset of R^1 by TOPMETR:24, XXREAL_1:1;
A3: [.0 ,1.] = the carrier of (R^1 | A) by PRE_TOPC:29;
A4: rng g c= [.0 ,1.]

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng g ; :: thesis:
then consider y being set such that
A5: ( y in dom g & x = g . y ) by FUNCT_1:def 5;
reconsider y = y as Point of [:I[01] ,I[01] :] by A5;
g . y = (f1 . y) * (f2 . y) by A2;
then g . y is Point of I[01] by A1;
hence x in [.0 ,1.] by A5, BORSUK_1:83; :: thesis:

end;

dom g = the carrier of [:I[01] ,I[01] :] by FUNCT_2:def 1;
then reconsider g = g as Function of [:I[01] ,I[01] :],(R^1 | A) by A3, A4, FUNCT_2:4;
R^1 | A = I[01] by BORSUK_1:def 16, TOPMETR:def 7;
then reconsider g = g as continuous Function of [:I[01] ,I[01] :],I[01] by A2, JGRAPH_1:63;
take g ; :: thesis:
thus ( ( for p being Point of [:I[01] ,I[01] :]
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 * r2 ) & g is continuous ) by A2; :: thesis: