let K0, B0 be Subset of (TOP-REAL 2); for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } holds
f is continuous
let f be Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0); ( f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } implies f is continuous )
A1:
1.REAL 2 <> 0. (TOP-REAL 2)
by Lm1, REVROT_1:19;
assume A2:
( f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } )
; f is continuous
A3:
K0 c= B0
( ( (1.REAL 2) `1 <= (1.REAL 2) `2 & - ((1.REAL 2) `2) <= (1.REAL 2) `1 ) or ( (1.REAL 2) `1 >= (1.REAL 2) `2 & (1.REAL 2) `1 <= - ((1.REAL 2) `2) ) )
by Th5;
then A5:
1.REAL 2 in K0
by A2, A1;
then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;
A6:
K1 c= NonZero (TOP-REAL 2)
A8:
dom (Out_In_Sq | K1) c= dom (proj1 * (Out_In_Sq | K1))
A11:
rng (proj1 * (Out_In_Sq | K1)) c= the carrier of R^1
by TOPMETR:17;
A12:
NonZero (TOP-REAL 2) <> {}
by Th9;
A13:
dom (Out_In_Sq | K1) c= dom (proj2 * (Out_In_Sq | K1))
A16:
rng (proj2 * (Out_In_Sq | K1)) c= the carrier of R^1
by TOPMETR:17;
dom (proj2 * (Out_In_Sq | K1)) c= dom (Out_In_Sq | K1)
by RELAT_1:25;
then dom (proj2 * (Out_In_Sq | K1)) =
dom (Out_In_Sq | K1)
by A13
.=
(dom Out_In_Sq) /\ K1
by RELAT_1:61
.=
(NonZero (TOP-REAL 2)) /\ K1
by A12, FUNCT_2:def 1
.=
K1
by A6, XBOOLE_1:28
.=
[#] ((TOP-REAL 2) | K1)
by PRE_TOPC:def 5
.=
the carrier of ((TOP-REAL 2) | K1)
;
then reconsider g1 = proj2 * (Out_In_Sq | K1) as Function of ((TOP-REAL 2) | K1),R^1 by A16, FUNCT_2:2;
for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
g1 . p = 1 / (p `2)
proof
A17:
K1 c= NonZero (TOP-REAL 2)
A19:
NonZero (TOP-REAL 2) <> {}
by Th9;
A20:
dom (Out_In_Sq | K1) =
(dom Out_In_Sq) /\ K1
by RELAT_1:61
.=
(NonZero (TOP-REAL 2)) /\ K1
by A19, FUNCT_2:def 1
.=
K1
by A17, XBOOLE_1:28
;
let p be
Point of
(TOP-REAL 2);
( p in the carrier of ((TOP-REAL 2) | K1) implies g1 . p = 1 / (p `2) )
A21: the
carrier of
((TOP-REAL 2) | K1) =
[#] ((TOP-REAL 2) | K1)
.=
K1
by PRE_TOPC:def 5
;
assume A22:
p in the
carrier of
((TOP-REAL 2) | K1)
;
g1 . p = 1 / (p `2)
then
ex
p3 being
Point of
(TOP-REAL 2) st
(
p = p3 & ( (
p3 `1 <= p3 `2 &
- (p3 `2) <= p3 `1 ) or (
p3 `1 >= p3 `2 &
p3 `1 <= - (p3 `2) ) ) &
p3 <> 0. (TOP-REAL 2) )
by A2, A21;
then A23:
Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]|
by Th14;
(Out_In_Sq | K1) . p = Out_In_Sq . p
by A22, A21, FUNCT_1:49;
then g1 . p =
proj2 . |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]|
by A22, A20, A21, A23, FUNCT_1:13
.=
|[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| `2
by PSCOMP_1:def 6
.=
1
/ (p `2)
by EUCLID:52
;
hence
g1 . p = 1
/ (p `2)
;
verum
end;
then consider f1 being Function of ((TOP-REAL 2) | K1),R^1 such that
A24:
for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f1 . p = 1 / (p `2)
;
dom (proj1 * (Out_In_Sq | K1)) c= dom (Out_In_Sq | K1)
by RELAT_1:25;
then dom (proj1 * (Out_In_Sq | K1)) =
dom (Out_In_Sq | K1)
by A8
.=
(dom Out_In_Sq) /\ K1
by RELAT_1:61
.=
(NonZero (TOP-REAL 2)) /\ K1
by A12, FUNCT_2:def 1
.=
K1
by A6, XBOOLE_1:28
.=
[#] ((TOP-REAL 2) | K1)
by PRE_TOPC:def 5
.=
the carrier of ((TOP-REAL 2) | K1)
;
then reconsider g2 = proj1 * (Out_In_Sq | K1) as Function of ((TOP-REAL 2) | K1),R^1 by A11, FUNCT_2:2;
for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
g2 . p = ((p `1) / (p `2)) / (p `2)
proof
A25:
NonZero (TOP-REAL 2) <> {}
by Th9;
A26:
dom (Out_In_Sq | K1) =
(dom Out_In_Sq) /\ K1
by RELAT_1:61
.=
(NonZero (TOP-REAL 2)) /\ K1
by A25, FUNCT_2:def 1
.=
K1
by A6, XBOOLE_1:28
;
let p be
Point of
(TOP-REAL 2);
( p in the carrier of ((TOP-REAL 2) | K1) implies g2 . p = ((p `1) / (p `2)) / (p `2) )
A27: the
carrier of
((TOP-REAL 2) | K1) =
[#] ((TOP-REAL 2) | K1)
.=
K1
by PRE_TOPC:def 5
;
assume A28:
p in the
carrier of
((TOP-REAL 2) | K1)
;
g2 . p = ((p `1) / (p `2)) / (p `2)
then
ex
p3 being
Point of
(TOP-REAL 2) st
(
p = p3 & ( (
p3 `1 <= p3 `2 &
- (p3 `2) <= p3 `1 ) or (
p3 `1 >= p3 `2 &
p3 `1 <= - (p3 `2) ) ) &
p3 <> 0. (TOP-REAL 2) )
by A2, A27;
then A29:
Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]|
by Th14;
(Out_In_Sq | K1) . p = Out_In_Sq . p
by A28, A27, FUNCT_1:49;
then g2 . p =
proj1 . |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]|
by A28, A26, A27, A29, FUNCT_1:13
.=
|[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| `1
by PSCOMP_1:def 5
.=
((p `1) / (p `2)) / (p `2)
by EUCLID:52
;
hence
g2 . p = ((p `1) / (p `2)) / (p `2)
;
verum
end;
then consider f2 being Function of ((TOP-REAL 2) | K1),R^1 such that
A30:
for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f2 . p = ((p `1) / (p `2)) / (p `2)
;
A31:
for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
q `2 <> 0
then A35:
f1 is continuous
by A24, Th32;
A36:
for x, y, s, r being Real st |[x,y]| in K1 & s = f2 . |[x,y]| & r = f1 . |[x,y]| holds
f . |[x,y]| = |[s,r]|
proof
let x,
y,
s,
r be
Real;
( |[x,y]| in K1 & s = f2 . |[x,y]| & r = f1 . |[x,y]| implies f . |[x,y]| = |[s,r]| )
assume that A37:
|[x,y]| in K1
and A38:
(
s = f2 . |[x,y]| &
r = f1 . |[x,y]| )
;
f . |[x,y]| = |[s,r]|
set p99 =
|[x,y]|;
A39:
ex
p3 being
Point of
(TOP-REAL 2) st
(
|[x,y]| = p3 & ( (
p3 `1 <= p3 `2 &
- (p3 `2) <= p3 `1 ) or (
p3 `1 >= p3 `2 &
p3 `1 <= - (p3 `2) ) ) &
p3 <> 0. (TOP-REAL 2) )
by A2, A37;
A40: the
carrier of
((TOP-REAL 2) | K1) =
[#] ((TOP-REAL 2) | K1)
.=
K1
by PRE_TOPC:def 5
;
then A41:
f1 . |[x,y]| = 1
/ (|[x,y]| `2)
by A24, A37;
(Out_In_Sq | K0) . |[x,y]| =
Out_In_Sq . |[x,y]|
by A37, FUNCT_1:49
.=
|[(((|[x,y]| `1) / (|[x,y]| `2)) / (|[x,y]| `2)),(1 / (|[x,y]| `2))]|
by A39, Th14
.=
|[s,r]|
by A30, A37, A38, A40, A41
;
hence
f . |[x,y]| = |[s,r]|
by A2;
verum
end;
f2 is continuous
by A31, A30, Th34;
hence
f is continuous
by A5, A3, A35, A36, Th35; verum