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) ;
reconsider g1 = proj1 * ((Sq_Circ ") | K1) as Function of ((TOP-REAL 2) | K1),R^1 by Lm18;
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
A2:
dom ((Sq_Circ ") | K1) =
(dom (Sq_Circ ")) /\ K1
by RELAT_1:61
.=
the
carrier of
(TOP-REAL 2) /\ K1
by Th29, FUNCT_2:def 1
.=
K1
by XBOOLE_1:28
;
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))) )
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 Th28;
((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)))
;
reconsider g2 = proj2 * ((Sq_Circ ") | K1) as Function of ((TOP-REAL 2) | K1),R^1 by Lm17;
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
A7:
dom ((Sq_Circ ") | K1) =
(dom (Sq_Circ ")) /\ K1
by RELAT_1:61
.=
the
carrier of
(TOP-REAL 2) /\ K1
by Th29, FUNCT_2:def 1
.=
K1
by XBOOLE_1:28
;
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))) )
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 Th28;
((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)))
;
A12:
for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
q `1 <> 0
then A16:
f1 is continuous
by A6, Th33;
A17:
now 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]|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, Th28
.=
|[r,s]|
by A11, A18, A19, A21, A22
;
hence
f . |[x,y]| = |[r,s]|
by A1;
verum end;
f2 is continuous
by A12, A11, Th34;
hence
f is continuous
by A1, A16, A17, Lm13, JGRAPH_2:35; verum