let X be non empty TopSpace; :: thesis: for f1 being Function of X,R^1
for a being real number st f1 is continuous holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being real number 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 number st f1 is continuous holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being real number st f1 . p = r1 holds
g . p = a * r1 ) & g is continuous )
let a be real number ; :: thesis: ( f1 is continuous implies ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being real number st f1 . p = r1 holds
g . p = a * r1 ) & g is continuous ) )
assume A1: f1 is continuous ; :: thesis: ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being real number st f1 . p = r1 holds
g . p = a * r1 ) & g is continuous )
defpred S1[ set , set ] means for r1 being Real st f1 . $1 = r1 holds
$2 = a * r1;
A2: for x being Element of X ex y being Element of REAL st S1[x,y]
proof
let x be Element of X; :: thesis: ex y being Element of REAL st S1[x,y]
reconsider r1 = f1 . x as Real by TOPMETR:24;
reconsider r3 = a * r1 as Element of REAL ;
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 S1[x,f . x] from FUNCT_2:sch 3(A2);
 then consider f being Function of the carrier of X, REAL such that
A3: 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:24;
A4: for p being Point of X
for r1 being real number st f1 . p = r1 holds
g0 . p = a * r1
proof
let p be Point of X; :: thesis: for r1 being real number st f1 . p = r1 holds
g0 . p = a * r1
let r1 be real number ; :: thesis: ( f1 . p = r1 implies g0 . p = a * r1 )
assume A5: f1 . p = r1 ; :: thesis: g0 . p = a * r1
reconsider r1 = r1 as Element of REAL by XREAL_0:def 1;
g0 . p = a * r1 by A3, A5;
hence g0 . p = a * r1 ; :: thesis: verum
end;
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 ) )
assume A6: ( 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 )
reconsider r = g0 . p as Real by TOPMETR:24;
consider r0 being Real such that
A7: ( r0 > 0 & ].(r - r0),(r + r0).[ c= V ) by A6, FRECHET:8;
reconsider r1 = f1 . p as Real by TOPMETR:24;
A8: r = a * r1 by A3;
A9: r = a * r1 by A3;
now
per cases ( a >= 0 or a < 0 ) ;
case A10: a >= 0 ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
now
per cases ( a > 0 or a = 0 ) by A10;
case A11: a > 0 ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
set r4 = r0 / a;
A12: r0 / a > 0 by A7, A11, XREAL_1:141;
reconsider G1 = ].(r1 - (r0 / a)),(r1 + (r0 / a)).[ as Subset of R^1 by TOPMETR:24;
A13: r1 < r1 + (r0 / a) by A12, XREAL_1:31;
then r1 - (r0 / a) < r1 by XREAL_1:21;
then A14: f1 . p in G1 by A13, XXREAL_1:4;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A15: ( p in W1 & W1 is open & f1 .: W1 c= G1 ) by A1, A14, Th20;
set W = W1;
g0 .: W1 c= ].(r - r0),(r + r0).[
proof
let x be set ; :: 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 set such that
A16: ( z in dom g0 & z in W1 & g0 . z = x ) by FUNCT_1:def 12;
reconsider pz = z as Point of X by A16;
pz in the carrier of X ;
then pz in dom f1 by FUNCT_2:def 1;
then A17: f1 . pz in f1 .: W1 by A16, FUNCT_1:def 12;
reconsider aa1 = f1 . pz as Real by TOPMETR:24;
A18: x = a * aa1 by A3, A16;
reconsider rx = x as Real by A16, XREAL_0:def 1;
A19: ( r1 - (r0 / a) < aa1 & aa1 < r1 + (r0 / a) ) by A15, A17, XXREAL_1:4;
a * (r1 + (r0 / a)) = (a * r1) + (a * (r0 / a))
.= r + r0 by A8, A11, XCMPLX_1:88 ;
then A20: rx < r + r0 by A11, A18, A19, XREAL_1:70;
A21: a * (r1 - (r0 / a)) < a * aa1 by A11, A19, XREAL_1:70;
a * (r1 - (r0 / a)) = (a * r1) - (a * (r0 / a))
.= r - r0 by A8, A11, XCMPLX_1:88 ;
hence x in ].(r - r0),(r + r0).[ by A18, A20, A21, 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 A7, A15, XBOOLE_1:1; :: thesis: verum
end;
case A22: 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:24;
A23: r1 < r1 + r0 by A7, XREAL_1:31;
then r1 - r0 < r1 by XREAL_1:21;
then A24: f1 . p in G1 by A23, XXREAL_1:4;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A25: ( p in W1 & W1 is open & f1 .: W1 c= G1 ) by A1, A24, Th20;
set W = W1;
g0 .: W1 c= ].(r - r0),(r + r0).[
proof
let x be set ; :: 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 set such that
A26: ( z in dom g0 & z in W1 & g0 . z = x ) by FUNCT_1:def 12;
reconsider pz = z as Point of X by A26;
reconsider aa1 = f1 . pz as Real by TOPMETR:24;
x = a * aa1 by A3, A26
.= 0 by A22 ;
hence x in ].(r - r0),(r + r0).[ by A7, A9, 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 A7, A25, 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 A28: a < 0 ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
then A29: - a > 0 by XREAL_1:60;
A30: - a <> 0 by A28;
set r4 = r0 / (- a);
A31: r0 / (- a) > 0 by A7, A29, XREAL_1:141;
A32: (- a) * (r0 / (- a)) = r0 by A30, XCMPLX_1:88;
reconsider G1 = ].(r1 - (r0 / (- a))),(r1 + (r0 / (- a))).[ as Subset of R^1 by TOPMETR:24;
A33: r1 < r1 + (r0 / (- a)) by A31, XREAL_1:31;
then r1 - (r0 / (- a)) < r1 by XREAL_1:21;
then A34: f1 . p in G1 by A33, XXREAL_1:4;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A35: ( p in W1 & W1 is open & f1 .: W1 c= G1 ) by A1, A34, Th20;
set W = W1;
g0 .: W1 c= ].(r - r0),(r + r0).[
proof
let x be set ; :: 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 set such that
A36: ( z in dom g0 & z in W1 & g0 . z = x ) by FUNCT_1:def 12;
reconsider pz = z as Point of X by A36;
pz in the carrier of X ;
then pz in dom f1 by FUNCT_2:def 1;
then A37: f1 . pz in f1 .: W1 by A36, FUNCT_1:def 12;
reconsider aa1 = f1 . pz as Real by TOPMETR:24;
A38: x = a * aa1 by A3, A36;
A39: ( r1 - (r0 / (- a)) < aa1 & aa1 < r1 + (r0 / (- a)) ) by A35, A37, XXREAL_1:4;
then A40: a * aa1 < a * (r1 - (r0 / (- a))) by A28, XREAL_1:71;
A41: a * (r1 - (r0 / (- a))) = (a * r1) + (- (a * (r0 / (- a))))
.= r + r0 by A4, A32 ;
a * (r1 + (r0 / (- a))) = (a * r1) - (- (a * (r0 / (- a))))
.= r - r0 by A4, A32 ;
then r - r0 < a * aa1 by A28, A39, XREAL_1:71;
hence x in ].(r - r0),(r + r0).[ by A38, A40, A41, 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 A7, A35, 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 Th20;
hence ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being real number st f1 . p = r1 holds
g . p = a * r1 ) & g is continuous ) by A4; :: thesis: verum