let X be non empty TopSpace; :: thesis: for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 * r2 ) & g is continuous )
let f1, f2 be Function of X,R^1 ; :: thesis: ( f1 is continuous & f2 is continuous implies ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 * r2 ) & g is continuous ) )
assume A1: ( f1 is continuous & f2 is continuous ) ; :: thesis: ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 * r2 ) & g is continuous )
then consider g1 being Function of X,R^1 such that
A2: ( ( for p being Point of X
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g1 . p = r1 + r2 ) & g1 is continuous ) by Th29;
consider g2 being Function of X,R^1 such that
A3: ( ( for p being Point of X
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g2 . p = r1 - r2 ) & g2 is continuous ) by A1, Th31;
consider g3 being Function of X,R^1 such that
A4: ( ( for p being Point of X
for r1 being real number st g1 . p = r1 holds
g3 . p = r1 * r1 ) & g3 is continuous ) by A2, Th32;
consider g4 being Function of X,R^1 such that
A5: ( ( for p being Point of X
for r1 being real number st g2 . p = r1 holds
g4 . p = r1 * r1 ) & g4 is continuous ) by A3, Th32;
consider g5 being Function of X,R^1 such that
A6: ( ( for p being Point of X
for r1, r2 being real number st g3 . p = r1 & g4 . p = r2 holds
g5 . p = r1 - r2 ) & g5 is continuous ) by A4, A5, Th31;
consider g6 being Function of X,R^1 such that
A7: ( ( for p being Point of X
for r1 being real number st g5 . p = r1 holds
g6 . p = (1 / 4) * r1 ) & g6 is continuous ) by A6, Th33;
for p being Point of X
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g6 . p = r1 * r2

proof

let p be Point of X; :: thesis: for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g6 . p = r1 * r2
let r1, r2 be real number ; :: thesis: ( f1 . p = r1 & f2 . p = r2 implies g6 . p = r1 * r2 )
assume A8: ( f1 . p = r1 & f2 . p = r2 ) ; :: thesis: g6 . p = r1 * r2
then A9: g1 . p = r1 + r2 by A2;
A10: g2 . p = r1 - r2 by A3, A8;
A11: g3 . p = (r1 + r2) ^2 by A4, A9;
g4 . p = (r1 - r2) ^2 by A5, A10;
then g5 . p = ((r1 + r2) ^2 ) - ((r1 - r2) ^2 ) by A6, A11;
then g6 . p = (1 / 4) * ((((r1 ^2 ) + ((2 * r1) * r2)) + (r2 ^2 )) - ((r1 - r2) ^2 )) by A7
.= r1 * r2 ;
hence g6 . p = r1 * r2 ; :: thesis: verum

end;

hence ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 * r2 ) & g is continuous ) by A7; :: thesis: verum