let K0, B0 be Subset of (TOP-REAL 2); for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0)
for f1, f2 being Function of ((TOP-REAL 2) | K0),R^1 st f1 is continuous & f2 is continuous & K0 <> {} & B0 <> {} & ( for x, y, r, s being real number st |[x,y]| in K0 & r = f1 . |[x,y]| & s = f2 . |[x,y]| holds
f . |[x,y]| = |[r,s]| ) holds
f is continuous
let f be Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0); for f1, f2 being Function of ((TOP-REAL 2) | K0),R^1 st f1 is continuous & f2 is continuous & K0 <> {} & B0 <> {} & ( for x, y, r, s being real number st |[x,y]| in K0 & r = f1 . |[x,y]| & s = f2 . |[x,y]| holds
f . |[x,y]| = |[r,s]| ) holds
f is continuous
let f1, f2 be Function of ((TOP-REAL 2) | K0),R^1; ( f1 is continuous & f2 is continuous & K0 <> {} & B0 <> {} & ( for x, y, r, s being real number st |[x,y]| in K0 & r = f1 . |[x,y]| & s = f2 . |[x,y]| holds
f . |[x,y]| = |[r,s]| ) implies f is continuous )
assume that
A1:
f1 is continuous
and
A2:
f2 is continuous
and
A3:
K0 <> {}
and
A4:
B0 <> {}
and
A5:
for x, y, r, s being real number st |[x,y]| in K0 & r = f1 . |[x,y]| & s = f2 . |[x,y]| holds
f . |[x,y]| = |[r,s]|
; f is continuous
reconsider B1 = B0 as non empty Subset of (TOP-REAL 2) by A4;
reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) by A3;
reconsider X = (TOP-REAL 2) | K1, Y = (TOP-REAL 2) | B1 as non empty TopSpace ;
reconsider f0 = f as Function of X,Y ;
for r being Point of X
for V being Subset of Y st f0 . r in V & V is open holds
ex W being Subset of X st
( r in W & W is open & f0 .: W c= V )
proof
let r be
Point of
X;
for V being Subset of Y st f0 . r in V & V is open holds
ex W being Subset of X st
( r in W & W is open & f0 .: W c= V )let V be
Subset of
Y;
( f0 . r in V & V is open implies ex W being Subset of X st
( r in W & W is open & f0 .: W c= V ) )
assume that A6:
f0 . r in V
and A7:
V is
open
;
ex W being Subset of X st
( r in W & W is open & f0 .: W c= V )
consider V2 being
Subset of
(TOP-REAL 2) such that A8:
V2 is
open
and A9:
V = V2 /\ ([#] Y)
by A7, TOPS_2:24;
A10:
V2 /\ ([#] Y) c= V2
by XBOOLE_1:17;
then
f0 . r in V2
by A6, A9;
then reconsider p =
f0 . r as
Point of
(TOP-REAL 2) ;
consider r2 being
real number such that A11:
r2 > 0
and A12:
{ q where q is Point of (TOP-REAL 2) : ( (p `1) - r2 < q `1 & q `1 < (p `1) + r2 & (p `2) - r2 < q `2 & q `2 < (p `2) + r2 ) } c= V2
by A6, A8, A9, A10, Th21;
reconsider G1 =
].((p `1) - r2),((p `1) + r2).[,
G2 =
].((p `2) - r2),((p `2) + r2).[ as
Subset of
R^1 by TOPMETR:17;
A13:
G1 is
open
by JORDAN6:35;
A14:
r in the
carrier of
X
;
then
r in dom f2
by FUNCT_2:def 1;
then A15:
f2 . r in rng f2
by FUNCT_1:3;
r in dom f1
by A14, FUNCT_2:def 1;
then
f1 . r in rng f1
by FUNCT_1:3;
then reconsider r3 =
f1 . r,
r4 =
f2 . r as
Real by A15, TOPMETR:17;
A16: the
carrier of
X =
[#] X
.=
K0
by PRE_TOPC:def 5
;
then
r in K0
;
then reconsider pr =
r as
Point of
(TOP-REAL 2) ;
A17:
r = |[(pr `1),(pr `2)]|
by EUCLID:53;
then A18:
f0 . |[(pr `1),(pr `2)]| = |[r3,r4]|
by A5, A16;
A19:
p `2 < (p `2) + r2
by A11, XREAL_1:29;
then
(p `2) - r2 < p `2
by XREAL_1:19;
then
p `2 in ].((p `2) - r2),((p `2) + r2).[
by A19, XXREAL_1:4;
then
(
G2 is
open &
f2 . r in G2 )
by A17, A18, EUCLID:52, JORDAN6:35;
then consider W2 being
Subset of
X such that A20:
r in W2
and A21:
W2 is
open
and A22:
f2 .: W2 c= G2
by A2, Th20;
A23:
p `1 < (p `1) + r2
by A11, XREAL_1:29;
then
(p `1) - r2 < p `1
by XREAL_1:19;
then
p `1 in ].((p `1) - r2),((p `1) + r2).[
by A23, XXREAL_1:4;
then
f1 . r in ].((p `1) - r2),((p `1) + r2).[
by A17, A18, EUCLID:52;
then consider W1 being
Subset of
X such that A24:
r in W1
and A25:
W1 is
open
and A26:
f1 .: W1 c= G1
by A1, A13, Th20;
reconsider W5 =
W1 /\ W2 as
Subset of
X ;
f2 .: W5 c= f2 .: W2
by RELAT_1:123, XBOOLE_1:17;
then A27:
f2 .: W5 c= G2
by A22, XBOOLE_1:1;
f1 .: W5 c= f1 .: W1
by RELAT_1:123, XBOOLE_1:17;
then A28:
f1 .: W5 c= G1
by A26, XBOOLE_1:1;
A29:
f0 .: W5 c= V
proof
let v be
set ;
TARSKI:def 3 ( not v in f0 .: W5 or v in V )
assume A30:
v in f0 .: W5
;
v in V
then reconsider q2 =
v as
Point of
Y ;
consider k being
set such that A31:
k in dom f0
and A32:
k in W5
and A33:
q2 = f0 . k
by A30, FUNCT_1:def 6;
the
carrier of
X =
[#] X
.=
K0
by PRE_TOPC:def 5
;
then
k in K0
by A31;
then reconsider r8 =
k as
Point of
(TOP-REAL 2) ;
A34:
dom f0 =
the
carrier of
((TOP-REAL 2) | K1)
by FUNCT_2:def 1
.=
[#] ((TOP-REAL 2) | K1)
.=
K0
by PRE_TOPC:def 5
;
then A35:
|[(r8 `1),(r8 `2)]| in K0
by A31, EUCLID:53;
A36:
dom f2 =
the
carrier of
((TOP-REAL 2) | K0)
by FUNCT_2:def 1
.=
[#] ((TOP-REAL 2) | K0)
.=
K0
by PRE_TOPC:def 5
;
then A37:
f2 . |[(r8 `1),(r8 `2)]| in rng f2
by A35, FUNCT_1:def 3;
A38:
dom f1 =
the
carrier of
((TOP-REAL 2) | K0)
by FUNCT_2:def 1
.=
[#] ((TOP-REAL 2) | K0)
.=
K0
by PRE_TOPC:def 5
;
then
f1 . |[(r8 `1),(r8 `2)]| in rng f1
by A35, FUNCT_1:def 3;
then reconsider r7 =
f1 . |[(r8 `1),(r8 `2)]|,
s7 =
f2 . |[(r8 `1),(r8 `2)]| as
Real by A37, TOPMETR:17;
A39:
|[(r8 `1),(r8 `2)]| in W5
by A32, EUCLID:53;
then
f1 . |[(r8 `1),(r8 `2)]| in f1 .: W5
by A35, A38, FUNCT_1:def 6;
then A40:
(
(p `1) - r2 < r7 &
r7 < (p `1) + r2 )
by A28, XXREAL_1:4;
f2 . |[(r8 `1),(r8 `2)]| in f2 .: W5
by A35, A36, A39, FUNCT_1:def 6;
then A41:
(
(p `2) - r2 < s7 &
s7 < (p `2) + r2 )
by A27, XXREAL_1:4;
k = |[(r8 `1),(r8 `2)]|
by EUCLID:53;
then A42:
v = |[r7,s7]|
by A5, A31, A33, A34;
(
|[r7,s7]| `1 = r7 &
|[r7,s7]| `2 = s7 )
by EUCLID:52;
then
(
q2 in [#] Y &
v in { q3 where q3 is Point of (TOP-REAL 2) : ( (p `1) - r2 < q3 `1 & q3 `1 < (p `1) + r2 & (p `2) - r2 < q3 `2 & q3 `2 < (p `2) + r2 ) } )
by A42, A40, A41;
hence
v in V
by A9, A12, XBOOLE_0:def 4;
verum
end;
r in W5
by A24, A20, XBOOLE_0:def 4;
hence
ex
W being
Subset of
X st
(
r in W &
W is
open &
f0 .: W c= V )
by A25, A21, A29;
verum
end;
hence
f is continuous
by Th20; verum