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