let X be non empty TopSpace; :: thesis: for f1 being Function of X,R^1
for a being Real st f1 is continuous holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being Real st f1 . p = r1 holds
g . p = a * r1 ) & g is continuous )
let f1 be Function of X,R^1; :: thesis: for a being Real st f1 is continuous holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being Real st f1 . p = r1 holds
g . p = a * r1 ) & g is continuous )
let a be Real; :: thesis: ( f1 is continuous implies ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being Real st f1 . p = r1 holds
g . p = a * r1 ) & g is continuous ) )
defpred S₁[ set , set ] means for r1 being Real st f1 . $1 = r1 holds
$2 = a * r1;
A1: for x being Element of X ex y being Element of REAL st S₁[x,y]

proof

let x be Element of X; :: thesis: ex y being Element of REAL st S₁[x,y]
reconsider r1 = f1 . x as Real ;
reconsider r3 = a * r1 as Element of REAL by XREAL_0:def 1;
for r1 being Real st f1 . x = r1 holds
r3 = a * r1 ;
hence ex y being Element of REAL st
for r1 being Real st f1 . x = r1 holds
y = a * r1 ; :: thesis: verum

end;

ex f being Function of the carrier of X,REAL st
for x being Element of X holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
then consider f being Function of the carrier of X,REAL such that
A2: for x being Element of X
for r1 being Real st f1 . x = r1 holds
f . x = a * r1 ;
reconsider g0 = f as Function of X,R^1 by TOPMETR:17;
A3: for p being Point of X
for r1 being Real st f1 . p = r1 holds
g0 . p = a * r1 by A2;
assume A4: f1 is continuous ; :: thesis: ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being Real st f1 . p = r1 holds
g . p = a * r1 ) & g is continuous )
for p being Point of X
for V being Subset of R^1 st g0 . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )

proof

let p be Point of X; :: thesis: for V being Subset of R^1 st g0 . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
let V be Subset of R^1; :: thesis: ( g0 . p in V & V is open implies ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) )
reconsider r = g0 . p as Real ;
reconsider r1 = f1 . p as Real ;
assume ( g0 . p in V & V is open ) ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
then consider r0 being Real such that
A5: r0 > 0 and
A6: ].(r - r0),(r + r0).[ c= V by FRECHET:8;
A7: r = a * r1 by A2;
A8: r = a * r1 by A2;

now :: thesis: ( ( a >= 0 & ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) ) or ( a < 0 & ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) ) )

per cases ( a >= 0 or a < 0 ) ;

case A9: a >= 0 ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )

now :: thesis: ( ( a > 0 & ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) ) or ( a = 0 & ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) ) )

per cases ( a > 0 or a = 0 ) by A9;

case A10: a > 0 ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )

set r4 = r0 / a;
reconsider G1 = ].(r1 - (r0 / a)),(r1 + (r0 / a)).[ as Subset of R^1 by TOPMETR:17;
A11: r1 < r1 + (r0 / a) by A5, A10, XREAL_1:29, XREAL_1:139;
then r1 - (r0 / a) < r1 by XREAL_1:19;
then A12: f1 . p in G1 by A11, XXREAL_1:4;
G1 is open by JORDAN6:35;
then consider W1 being Subset of X such that
A13: ( p in W1 & W1 is open ) and
A14: f1 .: W1 c= G1 by A4, A12, Th10;
set W = W1;
g0 .: W1 c= ].(r - r0),(r + r0).[

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g0 .: W1 or x in ].(r - r0),(r + r0).[ )
assume x in g0 .: W1 ; :: thesis: x in ].(r - r0),(r + r0).[
then consider z being object such that
A15: z in dom g0 and
A16: z in W1 and
A17: g0 . z = x by FUNCT_1:def 6;
reconsider pz = z as Point of X by A15;
reconsider aa1 = f1 . pz as Real ;
A18: x = a * aa1 by A2, A17;
pz in the carrier of X ;
then pz in dom f1 by FUNCT_2:def 1;
then A19: f1 . pz in f1 .: W1 by A16, FUNCT_1:def 6;
then r1 - (r0 / a) < aa1 by A14, XXREAL_1:4;
then A20: a * (r1 - (r0 / a)) < a * aa1 by A10, XREAL_1:68;
reconsider rx = x as Real by A17;
A21: a * (r1 + (r0 / a)) = (a * r1) + (a * (r0 / a))
.= r + r0 by A7, A10, XCMPLX_1:87 ;
A22: a * (r1 - (r0 / a)) = (a * r1) - (a * (r0 / a))
.= r - r0 by A7, A10, XCMPLX_1:87 ;
aa1 < r1 + (r0 / a) by A14, A19, XXREAL_1:4;
then rx < r + r0 by A10, A18, A21, XREAL_1:68;
hence x in ].(r - r0),(r + r0).[ by A18, A20, A22, XXREAL_1:4; :: thesis: verum

end;

hence ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) by A6, A13, XBOOLE_1:1; :: thesis: verum

end;

case A23: a = 0 ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )

set r4 = r0;
reconsider G1 = ].(r1 - r0),(r1 + r0).[ as Subset of R^1 by TOPMETR:17;
A24: r1 < r1 + r0 by A5, XREAL_1:29;
then r1 - r0 < r1 by XREAL_1:19;
then A25: f1 . p in G1 by A24, XXREAL_1:4;
G1 is open by JORDAN6:35;
then consider W1 being Subset of X such that
A26: ( p in W1 & W1 is open ) and
f1 .: W1 c= G1 by A4, A25, Th10;
set W = W1;
g0 .: W1 c= ].(r - r0),(r + r0).[

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g0 .: W1 or x in ].(r - r0),(r + r0).[ )
assume x in g0 .: W1 ; :: thesis: x in ].(r - r0),(r + r0).[
then consider z being object such that
A27: z in dom g0 and
z in W1 and
A28: g0 . z = x by FUNCT_1:def 6;
reconsider pz = z as Point of X by A27;
reconsider aa1 = f1 . pz as Real ;
x = a * aa1 by A2, A28
.= 0 by A23 ;
hence x in ].(r - r0),(r + r0).[ by A5, A8, A23, XXREAL_1:4; :: thesis: verum

end;

hence ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) by A6, A26, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

hence ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) ; :: thesis: verum

end;

case A29: a < 0 ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )

set r4 = r0 / (- a);
reconsider G1 = ].(r1 - (r0 / (- a))),(r1 + (r0 / (- a))).[ as Subset of R^1 by TOPMETR:17;
- a > 0 by A29, XREAL_1:58;
then A30: r1 < r1 + (r0 / (- a)) by A5, XREAL_1:29, XREAL_1:139;
then r1 - (r0 / (- a)) < r1 by XREAL_1:19;
then A31: f1 . p in G1 by A30, XXREAL_1:4;
G1 is open by JORDAN6:35;
then consider W1 being Subset of X such that
A32: ( p in W1 & W1 is open ) and
A33: f1 .: W1 c= G1 by A4, A31, Th10;
set W = W1;
- a <> 0 by A29;
then A34: (- a) * (r0 / (- a)) = r0 by XCMPLX_1:87;
g0 .: W1 c= ].(r - r0),(r + r0).[

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g0 .: W1 or x in ].(r - r0),(r + r0).[ )
assume x in g0 .: W1 ; :: thesis: x in ].(r - r0),(r + r0).[
then consider z being object such that
A35: z in dom g0 and
A36: z in W1 and
A37: g0 . z = x by FUNCT_1:def 6;
reconsider pz = z as Point of X by A35;
reconsider aa1 = f1 . pz as Real ;
pz in the carrier of X ;
then pz in dom f1 by FUNCT_2:def 1;
then A38: f1 . pz in f1 .: W1 by A36, FUNCT_1:def 6;
then r1 - (r0 / (- a)) < aa1 by A33, XXREAL_1:4;
then A39: a * aa1 < a * (r1 - (r0 / (- a))) by A29, XREAL_1:69;
A40: a * (r1 + (r0 / (- a))) = (a * r1) - (- (a * (r0 / (- a))))
.= r - r0 by A3, A34 ;
A41: a * (r1 - (r0 / (- a))) = (a * r1) + (- (a * (r0 / (- a))))
.= r + r0 by A3, A34 ;
aa1 < r1 + (r0 / (- a)) by A33, A38, XXREAL_1:4;
then A42: r - r0 < a * aa1 by A29, A40, XREAL_1:69;
x = a * aa1 by A2, A37;
hence x in ].(r - r0),(r + r0).[ by A39, A41, A42, XXREAL_1:4; :: thesis: verum

end;

hence ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) by A6, A32, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

hence ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) ; :: thesis: verum

end;

then g0 is continuous by Th10;
hence ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being Real st f1 . p = r1 holds
g . p = a * r1 ) & g is continuous ) by A3; :: thesis: verum