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 )
defpred S1[ set , set ] means for r1, r2 being real number st f1 . $1 = r1 & f2 . $1 = r2 holds
$2 = r1 - r2;
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 r2 = f2 . x as Real by TOPMETR:24;
set r3 = r1 - r2;
for r1, r2 being real number st f1 . x = r1 & f2 . x = r2 holds
r1 - r2 = r1 - r2 ;
hence ex y being Element of REAL st
for r1, r2 being real number st f1 . x = r1 & f2 . x = r2 holds
y = r1 - r2 ; :: 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, r2 being real number st f1 . x = r1 & f2 . x = r2 holds
f . x = r1 - r2 ;
reconsider g0 = f as Function of X,R^1 by TOPMETR:24;
A4: for p being Point of X
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g0 . p = r1 - r2 by A3;
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 A5: ( 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
A6: ( r0 > 0 & ].(r - r0),(r + r0).[ c= V ) by A5, FRECHET:8;
reconsider r1 = f1 . p as Real by TOPMETR:24;
reconsider G1 = ].(r1 - (r0 / 2)),(r1 + (r0 / 2)).[ as Subset of R^1 by TOPMETR:24;
r0 / 2 > 0 by A6, XREAL_1:217;
then A7: r1 < r1 + (r0 / 2) by XREAL_1:31;
then r1 - (r0 / 2) < r1 by XREAL_1:21;
then A8: f1 . p in G1 by A7, XXREAL_1:4;
G1 is open by JORDAN6:46;
then consider W1 being Subset of X such that
A9: ( p in W1 & W1 is open & f1 .: W1 c= G1 ) by A1, A8, Th20;
reconsider r2 = f2 . p as Real by TOPMETR:24;
reconsider G2 = ].(r2 - (r0 / 2)),(r2 + (r0 / 2)).[ as Subset of R^1 by TOPMETR:24;
r0 / 2 > 0 by A6, XREAL_1:217;
then A10: r2 < r2 + (r0 / 2) by XREAL_1:31;
then r2 - (r0 / 2) < r2 by XREAL_1:21;
then A11: f2 . p in G2 by A10, XXREAL_1:4;
G2 is open by JORDAN6:46;
then consider W2 being Subset of X such that
A12: ( p in W2 & W2 is open & f2 .: W2 c= G2 ) by A1, A11, Th20;
set W = W1 /\ W2;
A13: W1 /\ W2 is open by A9, A12, TOPS_1:38;
A14: p in W1 /\ W2 by A9, A12, XBOOLE_0:def 4;
g0 .: (W1 /\ W2) c= ].(r - r0),(r + r0).[
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in g0 .: (W1 /\ W2) or x in ].(r - r0),(r + r0).[ )
assume x in g0 .: (W1 /\ W2) ; :: thesis: x in ].(r - r0),(r + r0).[
then consider z being set such that
A15: ( z in dom g0 & z in W1 /\ W2 & g0 . z = x ) by FUNCT_1:def 12;
A16: z in W1 by A15, XBOOLE_0:def 4;
reconsider pz = z as Point of X by A15;
A17: pz in the carrier of X ;
then pz in dom f1 by FUNCT_2:def 1;
then A18: f1 . pz in f1 .: W1 by A16, FUNCT_1:def 12;
reconsider aa1 = f1 . pz as Real by TOPMETR:24;
A19: z in W2 by A15, XBOOLE_0:def 4;
pz in dom f2 by A17, FUNCT_2:def 1;
then A20: f2 . pz in f2 .: W2 by A19, FUNCT_1:def 12;
reconsider aa2 = f2 . pz as Real by TOPMETR:24;
A21: x = aa1 - aa2 by A3, A15;
then reconsider rx = x as Real ;
A22: ( r1 - (r0 / 2) < aa1 & aa1 < r1 + (r0 / 2) ) by A9, A18, XXREAL_1:4;
A23: ( r2 - (r0 / 2) < aa2 & aa2 < r2 + (r0 / 2) ) by A12, A20, XXREAL_1:4;
then aa1 - aa2 < (r1 + (r0 / 2)) - (r2 - (r0 / 2)) by A22, XREAL_1:16;
then aa1 - aa2 < (r1 - r2) + ((r0 / 2) + (r0 / 2)) ;
then A24: rx < r + r0 by A3, A21;
(r1 - (r0 / 2)) - (r2 + (r0 / 2)) < aa1 - aa2 by A22, A23, XREAL_1:16;
then (r1 - r2) - ((r0 / 2) + (r0 / 2)) < aa1 - aa2 ;
then r - r0 < aa1 - aa2 by A3;
hence x in ].(r - r0),(r + r0).[ by A21, A24, 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, A14, XBOOLE_1:1; :: 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, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 - r2 ) & g is continuous ) by A4; :: thesis: verum