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 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 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 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 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 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, Th11;
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;
reconsider r3 =
f1 . r,
r4 =
f2 . r as
Real ;
A14: 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) ;
A15:
r = |[(pr `1),(pr `2)]|
by EUCLID:53;
then A16:
f0 . |[(pr `1),(pr `2)]| = |[r3,r4]|
by A5, A14;
A17:
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 A17, XXREAL_1:4;
then
(
G2 is
open &
f2 . r in G2 )
by A15, A16, EUCLID:52, JORDAN6:35;
then consider W2 being
Subset of
X such that A18:
r in W2
and A19:
W2 is
open
and A20:
f2 .: W2 c= G2
by A2, Th10;
A21:
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 A21, XXREAL_1:4;
then
f1 . r in ].((p `1) - r2),((p `1) + r2).[
by A15, A16, EUCLID:52;
then consider W1 being
Subset of
X such that A22:
r in W1
and A23:
W1 is
open
and A24:
f1 .: W1 c= G1
by A1, A13, Th10;
reconsider W5 =
W1 /\ W2 as
Subset of
X ;
f2 .: W5 c= f2 .: W2
by RELAT_1:123, XBOOLE_1:17;
then A25:
f2 .: W5 c= G2
by A20;
f1 .: W5 c= f1 .: W1
by RELAT_1:123, XBOOLE_1:17;
then A26:
f1 .: W5 c= G1
by A24;
A27:
f0 .: W5 c= V
proof
let v be
object ;
TARSKI:def 3 ( not v in f0 .: W5 or v in V )
assume A28:
v in f0 .: W5
;
v in V
then reconsider q2 =
v as
Point of
Y ;
consider k being
object such that A29:
k in dom f0
and A30:
k in W5
and A31:
q2 = f0 . k
by A28, FUNCT_1:def 6;
the
carrier of
X =
[#] X
.=
K0
by PRE_TOPC:def 5
;
then
k in K0
by A29;
then reconsider r8 =
k as
Point of
(TOP-REAL 2) ;
A32:
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 A33:
|[(r8 `1),(r8 `2)]| in K0
by A29, EUCLID:53;
A34:
dom f2 =
the
carrier of
((TOP-REAL 2) | K0)
by FUNCT_2:def 1
.=
[#] ((TOP-REAL 2) | K0)
.=
K0
by PRE_TOPC:def 5
;
A35:
dom f1 =
the
carrier of
((TOP-REAL 2) | K0)
by FUNCT_2:def 1
.=
[#] ((TOP-REAL 2) | K0)
.=
K0
by PRE_TOPC:def 5
;
reconsider r7 =
f1 . |[(r8 `1),(r8 `2)]|,
s7 =
f2 . |[(r8 `1),(r8 `2)]| as
Real ;
A36:
|[(r8 `1),(r8 `2)]| in W5
by A30, EUCLID:53;
then
f1 . |[(r8 `1),(r8 `2)]| in f1 .: W5
by A33, A35, FUNCT_1:def 6;
then A37:
(
(p `1) - r2 < r7 &
r7 < (p `1) + r2 )
by A26, XXREAL_1:4;
f2 . |[(r8 `1),(r8 `2)]| in f2 .: W5
by A33, A34, A36, FUNCT_1:def 6;
then A38:
(
(p `2) - r2 < s7 &
s7 < (p `2) + r2 )
by A25, XXREAL_1:4;
k = |[(r8 `1),(r8 `2)]|
by EUCLID:53;
then A39:
v = |[r7,s7]|
by A5, A29, A31, A32;
(
|[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 A39, A37, A38;
hence
v in V
by A9, A12, XBOOLE_0:def 4;
verum
end;
r in W5
by A22, A18, XBOOLE_0:def 4;
hence
ex
W being
Subset of
X st
(
r in W &
W is
open &
f0 .: W c= V )
by A23, A19, A27;
verum
end;
hence
f is continuous
by Th10; verum