let K0, B0 be Subset of (TOP-REAL 2); :: thesis: 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 `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); :: thesis: ( f = Sq_Circ | 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 )
assume A1:
( f = Sq_Circ | 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) ) } )
; :: thesis: f is continuous
then
1.REAL 2 in K0
by Lm11;
then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;
A2:
dom (proj1 * (Sq_Circ | K1)) = the carrier of ((TOP-REAL 2) | K1)
by Lm9;
rng (proj1 * (Sq_Circ | K1)) c= the carrier of R^1
by TOPMETR:24;
then reconsider g2 = proj1 * (Sq_Circ | K1) as Function of ((TOP-REAL 2) | K1),R^1 by A2, FUNCT_2:4;
A3:
dom (proj2 * (Sq_Circ | K1)) = the carrier of ((TOP-REAL 2) | K1)
by Lm8;
rng (proj2 * (Sq_Circ | K1)) c= the carrier of R^1
by TOPMETR:24;
then reconsider g1 = proj2 * (Sq_Circ | K1) as Function of ((TOP-REAL 2) | K1),R^1 by A3, FUNCT_2:4;
A4:
for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
q `2 <> 0
for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
g2 . p = (p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))
proof
let p be
Point of
(TOP-REAL 2);
:: thesis: ( p in the carrier of ((TOP-REAL 2) | K1) implies g2 . p = (p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))) )
assume A8:
p in the
carrier of
((TOP-REAL 2) | K1)
;
:: thesis: g2 . p = (p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))
A9:
dom (Sq_Circ | K1) =
(dom Sq_Circ ) /\ K1
by RELAT_1:90
.=
the
carrier of
(TOP-REAL 2) /\ K1
by FUNCT_2:def 1
.=
K1
by XBOOLE_1:28
;
A10:
the
carrier of
((TOP-REAL 2) | K1) = K1
by PRE_TOPC:29;
then consider p3 being
Point of
(TOP-REAL 2) such that A11:
(
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 A1, A8;
A12:
Sq_Circ . p = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]|
by A11, Th14;
(Sq_Circ | K1) . p = Sq_Circ . p
by A8, A10, FUNCT_1:72;
then g2 . p =
proj1 . |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]|
by A8, A9, A10, A12, FUNCT_1:23
.=
|[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| `1
by PSCOMP_1:def 28
.=
(p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))
by EUCLID:56
;
hence
g2 . p = (p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))
;
:: thesis: verum
end;
then consider f2 being Function of ((TOP-REAL 2) | K1),R^1 such that
A13:
for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f2 . p = (p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))
;
A14:
f2 is continuous
by A4, A13, Th24;
for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
g1 . p = (p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))
proof
let p be
Point of
(TOP-REAL 2);
:: thesis: ( p in the carrier of ((TOP-REAL 2) | K1) implies g1 . p = (p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))) )
assume A15:
p in the
carrier of
((TOP-REAL 2) | K1)
;
:: thesis: g1 . p = (p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))
A16:
dom (Sq_Circ | K1) =
(dom Sq_Circ ) /\ K1
by RELAT_1:90
.=
the
carrier of
(TOP-REAL 2) /\ K1
by FUNCT_2:def 1
.=
K1
by XBOOLE_1:28
;
A17:
the
carrier of
((TOP-REAL 2) | K1) = K1
by PRE_TOPC:29;
then consider p3 being
Point of
(TOP-REAL 2) such that A18:
(
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 A1, A15;
A19:
Sq_Circ . p = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]|
by A18, Th14;
(Sq_Circ | K1) . p = Sq_Circ . p
by A15, A17, FUNCT_1:72;
then g1 . p =
proj2 . |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]|
by A15, A16, A17, A19, FUNCT_1:23
.=
|[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| `2
by PSCOMP_1:def 29
.=
(p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))
by EUCLID:56
;
hence
g1 . p = (p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))
;
:: thesis: verum
end;
then consider f1 being Function of ((TOP-REAL 2) | K1),R^1 such that
A20:
for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f1 . p = (p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))
;
A21:
f1 is continuous
by A4, A20, Th23;
now let x,
y,
s,
r be
real number ;
:: thesis: ( |[x,y]| in K1 & s = f2 . |[x,y]| & r = f1 . |[x,y]| implies f . |[x,y]| = |[s,r]| )assume A22:
(
|[x,y]| in K1 &
s = f2 . |[x,y]| &
r = f1 . |[x,y]| )
;
:: thesis: f . |[x,y]| = |[s,r]|set p99 =
|[x,y]|;
A23:
the
carrier of
((TOP-REAL 2) | K1) = K1
by PRE_TOPC:29;
consider p3 being
Point of
(TOP-REAL 2) such that A24:
(
|[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 A1, A22;
A25:
f1 . |[x,y]| = (|[x,y]| `2 ) / (sqrt (1 + (((|[x,y]| `1 ) / (|[x,y]| `2 )) ^2 )))
by A20, A22, A23;
(Sq_Circ | K0) . |[x,y]| =
Sq_Circ . |[x,y]|
by A22, FUNCT_1:72
.=
|[((|[x,y]| `1 ) / (sqrt (1 + (((|[x,y]| `1 ) / (|[x,y]| `2 )) ^2 )))),((|[x,y]| `2 ) / (sqrt (1 + (((|[x,y]| `1 ) / (|[x,y]| `2 )) ^2 ))))]|
by A24, Th14
.=
|[s,r]|
by A13, A22, A23, A25
;
hence
f . |[x,y]| = |[s,r]|
by A1;
:: thesis: verum end;
hence
f is continuous
by A1, A14, A21, Lm10, JGRAPH_2:45; :: thesis: verum