let K0, B0 be Subset of (TOP-REAL 2); for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st f = Sq_Circ | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } holds
f is continuous
let f be Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0); ( f = Sq_Circ | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } implies f is continuous )
assume A1:
( f = Sq_Circ | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } )
; f is continuous
then
1.REAL 2 in K0
by Lm9, Lm10;
then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;
( dom (proj1 * (Sq_Circ | K1)) = the carrier of ((TOP-REAL 2) | K1) & rng (proj1 * (Sq_Circ | K1)) c= the carrier of R^1 )
by Lm12, TOPMETR:17;
then reconsider g1 = proj1 * (Sq_Circ | K1) as Function of ((TOP-REAL 2) | K1),R^1 by FUNCT_2:2;
for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
g1 . p = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))
proof
let p be
Point of
(TOP-REAL 2);
( p in the carrier of ((TOP-REAL 2) | K1) implies g1 . p = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) )
A2:
dom (Sq_Circ | K1) =
(dom Sq_Circ) /\ K1
by RELAT_1:61
.=
the
carrier of
(TOP-REAL 2) /\ K1
by FUNCT_2:def 1
.=
K1
by XBOOLE_1:28
;
A3:
the
carrier of
((TOP-REAL 2) | K1) = K1
by PRE_TOPC:8;
assume A4:
p in the
carrier of
((TOP-REAL 2) | K1)
;
g1 . p = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))
then
ex
p3 being
Point of
(TOP-REAL 2) st
(
p = p3 & ( (
p3 `2 <= p3 `1 &
- (p3 `1) <= p3 `2 ) or (
p3 `2 >= p3 `1 &
p3 `2 <= - (p3 `1) ) ) &
p3 <> 0. (TOP-REAL 2) )
by A1, A3;
then A5:
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]|
by Def1;
(Sq_Circ | K1) . p = Sq_Circ . p
by A4, A3, FUNCT_1:49;
then g1 . p =
proj1 . |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]|
by A4, A2, A3, A5, FUNCT_1:13
.=
|[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1
by PSCOMP_1:def 5
.=
(p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))
by EUCLID:52
;
hence
g1 . p = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))
;
verum
end;
then consider f1 being Function of ((TOP-REAL 2) | K1),R^1 such that
A6:
for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f1 . p = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))
;
( dom (proj2 * (Sq_Circ | K1)) = the carrier of ((TOP-REAL 2) | K1) & rng (proj2 * (Sq_Circ | K1)) c= the carrier of R^1 )
by Lm11, TOPMETR:17;
then reconsider g2 = proj2 * (Sq_Circ | K1) as Function of ((TOP-REAL 2) | K1),R^1 by 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 `2) / (sqrt (1 + (((p `2) / (p `1)) ^2)))
proof
let p be
Point of
(TOP-REAL 2);
( p in the carrier of ((TOP-REAL 2) | K1) implies g2 . p = (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) )
A7:
dom (Sq_Circ | K1) =
(dom Sq_Circ) /\ K1
by RELAT_1:61
.=
the
carrier of
(TOP-REAL 2) /\ K1
by FUNCT_2:def 1
.=
K1
by XBOOLE_1:28
;
A8:
the
carrier of
((TOP-REAL 2) | K1) = K1
by PRE_TOPC:8;
assume A9:
p in the
carrier of
((TOP-REAL 2) | K1)
;
g2 . p = (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2)))
then
ex
p3 being
Point of
(TOP-REAL 2) st
(
p = p3 & ( (
p3 `2 <= p3 `1 &
- (p3 `1) <= p3 `2 ) or (
p3 `2 >= p3 `1 &
p3 `2 <= - (p3 `1) ) ) &
p3 <> 0. (TOP-REAL 2) )
by A1, A8;
then A10:
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]|
by Def1;
(Sq_Circ | K1) . p = Sq_Circ . p
by A9, A8, FUNCT_1:49;
then g2 . p =
proj2 . |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]|
by A9, A7, A8, A10, FUNCT_1:13
.=
|[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `2
by PSCOMP_1:def 6
.=
(p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2)))
by EUCLID:52
;
hence
g2 . p = (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2)))
;
verum
end;
then consider f2 being Function of ((TOP-REAL 2) | K1),R^1 such that
A11:
for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f2 . p = (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2)))
;
then A16:
f1 is continuous
by A6, Th11;
A17:
for x, y, r, s being Real st |[x,y]| in K1 & r = f1 . |[x,y]| & s = f2 . |[x,y]| holds
f . |[x,y]| = |[r,s]|
proof
let x,
y,
r,
s be
Real;
( |[x,y]| in K1 & r = f1 . |[x,y]| & s = f2 . |[x,y]| implies f . |[x,y]| = |[r,s]| )
assume that A18:
|[x,y]| in K1
and A19:
(
r = f1 . |[x,y]| &
s = f2 . |[x,y]| )
;
f . |[x,y]| = |[r,s]|
set p99 =
|[x,y]|;
A20:
ex
p3 being
Point of
(TOP-REAL 2) st
(
|[x,y]| = p3 & ( (
p3 `2 <= p3 `1 &
- (p3 `1) <= p3 `2 ) or (
p3 `2 >= p3 `1 &
p3 `2 <= - (p3 `1) ) ) &
p3 <> 0. (TOP-REAL 2) )
by A1, A18;
A21:
the
carrier of
((TOP-REAL 2) | K1) = K1
by PRE_TOPC:8;
then A22:
f1 . |[x,y]| = (|[x,y]| `1) / (sqrt (1 + (((|[x,y]| `2) / (|[x,y]| `1)) ^2)))
by A6, A18;
(Sq_Circ | K0) . |[x,y]| =
Sq_Circ . |[x,y]|
by A18, FUNCT_1:49
.=
|[((|[x,y]| `1) / (sqrt (1 + (((|[x,y]| `2) / (|[x,y]| `1)) ^2)))),((|[x,y]| `2) / (sqrt (1 + (((|[x,y]| `2) / (|[x,y]| `1)) ^2))))]|
by A20, Def1
.=
|[r,s]|
by A11, A18, A19, A21, A22
;
hence
f . |[x,y]| = |[r,s]|
by A1;
verum
end;
f2 is continuous
by A12, A11, Th12;
hence
f is continuous
by A1, A16, A17, Lm13, JGRAPH_2:35; verum