let sn be Real; for K0, B0 being Subset of (TOP-REAL 2)
for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st - 1 < sn & sn < 1 & f = (sn -FanMorphW) | K0 & B0 = { q where q is Point of (TOP-REAL 2) : ( q `1 <= 0 & q <> 0. (TOP-REAL 2) ) } & K0 = { p where p is Point of (TOP-REAL 2) : ( (p `2) / |.p.| <= sn & p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds
f is continuous
let K0, B0 be Subset of (TOP-REAL 2); for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st - 1 < sn & sn < 1 & f = (sn -FanMorphW) | K0 & B0 = { q where q is Point of (TOP-REAL 2) : ( q `1 <= 0 & q <> 0. (TOP-REAL 2) ) } & K0 = { p where p is Point of (TOP-REAL 2) : ( (p `2) / |.p.| <= sn & p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds
f is continuous
let f be Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0); ( - 1 < sn & sn < 1 & f = (sn -FanMorphW) | K0 & B0 = { q where q is Point of (TOP-REAL 2) : ( q `1 <= 0 & q <> 0. (TOP-REAL 2) ) } & K0 = { p where p is Point of (TOP-REAL 2) : ( (p `2) / |.p.| <= sn & p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } implies f is continuous )
set cn = sqrt (1 - (sn ^2));
set p0 = |[(- (sqrt (1 - (sn ^2)))),sn]|;
A1:
|[(- (sqrt (1 - (sn ^2)))),sn]| `1 = - (sqrt (1 - (sn ^2)))
by EUCLID:52;
|[(- (sqrt (1 - (sn ^2)))),sn]| `2 = sn
by EUCLID:52;
then A2: |.|[(- (sqrt (1 - (sn ^2)))),sn]|.| =
sqrt (((- (sqrt (1 - (sn ^2)))) ^2) + (sn ^2))
by A1, JGRAPH_3:1
.=
sqrt (((sqrt (1 - (sn ^2))) ^2) + (sn ^2))
;
assume A3:
( - 1 < sn & sn < 1 & f = (sn -FanMorphW) | K0 & B0 = { q where q is Point of (TOP-REAL 2) : ( q `1 <= 0 & q <> 0. (TOP-REAL 2) ) } & K0 = { p where p is Point of (TOP-REAL 2) : ( (p `2) / |.p.| <= sn & p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } )
; f is continuous
then
sn ^2 < 1 ^2
by SQUARE_1:50;
then A4:
1 - (sn ^2) > 0
by XREAL_1:50;
then A5:
- (- (sqrt (1 - (sn ^2)))) > 0
by SQUARE_1:25;
(sqrt (1 - (sn ^2))) ^2 = 1 - (sn ^2)
by A4, SQUARE_1:def 2;
then
(|[(- (sqrt (1 - (sn ^2)))),sn]| `2) / |.|[(- (sqrt (1 - (sn ^2)))),sn]|.| = sn
by A2, EUCLID:52, SQUARE_1:18;
then A7:
|[(- (sqrt (1 - (sn ^2)))),sn]| in K0
by A3, A1, A6, A5;
then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;
A8:
rng (proj1 * ((sn -FanMorphW) | K1)) c= the carrier of R^1
by TOPMETR:17;
A9:
K0 c= B0
A10:
dom ((sn -FanMorphW) | K1) c= dom (proj2 * ((sn -FanMorphW) | K1))
A13:
rng (proj2 * ((sn -FanMorphW) | K1)) c= the carrier of R^1
by TOPMETR:17;
dom (proj2 * ((sn -FanMorphW) | K1)) c= dom ((sn -FanMorphW) | K1)
by RELAT_1:25;
then dom (proj2 * ((sn -FanMorphW) | K1)) =
dom ((sn -FanMorphW) | K1)
by A10, XBOOLE_0:def 10
.=
(dom (sn -FanMorphW)) /\ K1
by RELAT_1:61
.=
the carrier of (TOP-REAL 2) /\ K1
by FUNCT_2:def 1
.=
K1
by XBOOLE_1:28
.=
the carrier of ((TOP-REAL 2) | K1)
by PRE_TOPC:8
;
then reconsider g2 = proj2 * ((sn -FanMorphW) | K1) as Function of ((TOP-REAL 2) | K1),R^1 by A13, 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.| * ((((p `2) / |.p.|) - sn) / (1 + sn))
proof
let p be
Point of
(TOP-REAL 2);
( p in the carrier of ((TOP-REAL 2) | K1) implies g2 . p = |.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)) )
A14:
dom ((sn -FanMorphW) | K1) =
(dom (sn -FanMorphW)) /\ K1
by RELAT_1:61
.=
the
carrier of
(TOP-REAL 2) /\ K1
by FUNCT_2:def 1
.=
K1
by XBOOLE_1:28
;
A15:
the
carrier of
((TOP-REAL 2) | K1) = K1
by PRE_TOPC:8;
assume A16:
p in the
carrier of
((TOP-REAL 2) | K1)
;
g2 . p = |.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn))
then
ex
p3 being
Point of
(TOP-REAL 2) st
(
p = p3 &
(p3 `2) / |.p3.| <= sn &
p3 `1 <= 0 &
p3 <> 0. (TOP-REAL 2) )
by A3, A15;
then A17:
(sn -FanMorphW) . p = |[(|.p.| * (- (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2))))),(|.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)))]|
by A3, Th18;
((sn -FanMorphW) | K1) . p = (sn -FanMorphW) . p
by A16, A15, FUNCT_1:49;
then g2 . p =
proj2 . |[(|.p.| * (- (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2))))),(|.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)))]|
by A16, A14, A15, A17, FUNCT_1:13
.=
|[(|.p.| * (- (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2))))),(|.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)))]| `2
by PSCOMP_1:def 6
.=
|.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn))
by EUCLID:52
;
hence
g2 . p = |.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn))
;
verum
end;
then consider f2 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
f2 . p = |.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn))
;
A19:
dom ((sn -FanMorphW) | K1) c= dom (proj1 * ((sn -FanMorphW) | K1))
dom (proj1 * ((sn -FanMorphW) | K1)) c= dom ((sn -FanMorphW) | K1)
by RELAT_1:25;
then dom (proj1 * ((sn -FanMorphW) | K1)) =
dom ((sn -FanMorphW) | K1)
by A19, XBOOLE_0:def 10
.=
(dom (sn -FanMorphW)) /\ K1
by RELAT_1:61
.=
the carrier of (TOP-REAL 2) /\ K1
by FUNCT_2:def 1
.=
K1
by XBOOLE_1:28
.=
the carrier of ((TOP-REAL 2) | K1)
by PRE_TOPC:8
;
then reconsider g1 = proj1 * ((sn -FanMorphW) | K1) as Function of ((TOP-REAL 2) | K1),R^1 by A8, 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.| * (- (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2))))
proof
let p be
Point of
(TOP-REAL 2);
( p in the carrier of ((TOP-REAL 2) | K1) implies g1 . p = |.p.| * (- (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2)))) )
A22:
dom ((sn -FanMorphW) | K1) =
(dom (sn -FanMorphW)) /\ K1
by RELAT_1:61
.=
the
carrier of
(TOP-REAL 2) /\ K1
by FUNCT_2:def 1
.=
K1
by XBOOLE_1:28
;
A23:
the
carrier of
((TOP-REAL 2) | K1) = K1
by PRE_TOPC:8;
assume A24:
p in the
carrier of
((TOP-REAL 2) | K1)
;
g1 . p = |.p.| * (- (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2))))
then
ex
p3 being
Point of
(TOP-REAL 2) st
(
p = p3 &
(p3 `2) / |.p3.| <= sn &
p3 `1 <= 0 &
p3 <> 0. (TOP-REAL 2) )
by A3, A23;
then A25:
(sn -FanMorphW) . p = |[(|.p.| * (- (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2))))),(|.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)))]|
by A3, Th18;
((sn -FanMorphW) | K1) . p = (sn -FanMorphW) . p
by A24, A23, FUNCT_1:49;
then g1 . p =
proj1 . |[(|.p.| * (- (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2))))),(|.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)))]|
by A24, A22, A23, A25, FUNCT_1:13
.=
|[(|.p.| * (- (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2))))),(|.p.| * ((((p `2) / |.p.|) - sn) / (1 + sn)))]| `1
by PSCOMP_1:def 5
.=
|.p.| * (- (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2))))
by EUCLID:52
;
hence
g1 . p = |.p.| * (- (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2))))
;
verum
end;
then consider f1 being Function of ((TOP-REAL 2) | K1),R^1 such that
A26:
for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds
f1 . p = |.p.| * (- (sqrt (1 - (((((p `2) / |.p.|) - sn) / (1 + sn)) ^2))))
;
for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
( q `1 <= 0 & (q `2) / |.q.| <= sn & q <> 0. (TOP-REAL 2) )
then A28:
f1 is continuous
by A3, A26, Th22;
A29:
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 A30:
|[x,y]| in K1
and A31:
(
r = f1 . |[x,y]| &
s = f2 . |[x,y]| )
;
f . |[x,y]| = |[r,s]|
set p99 =
|[x,y]|;
A32:
ex
p3 being
Point of
(TOP-REAL 2) st
(
|[x,y]| = p3 &
(p3 `2) / |.p3.| <= sn &
p3 `1 <= 0 &
p3 <> 0. (TOP-REAL 2) )
by A3, A30;
A33:
the
carrier of
((TOP-REAL 2) | K1) = K1
by PRE_TOPC:8;
then A34:
f1 . |[x,y]| = |.|[x,y]|.| * (- (sqrt (1 - (((((|[x,y]| `2) / |.|[x,y]|.|) - sn) / (1 + sn)) ^2))))
by A26, A30;
((sn -FanMorphW) | K0) . |[x,y]| =
(sn -FanMorphW) . |[x,y]|
by A30, FUNCT_1:49
.=
|[(|.|[x,y]|.| * (- (sqrt (1 - (((((|[x,y]| `2) / |.|[x,y]|.|) - sn) / (1 + sn)) ^2))))),(|.|[x,y]|.| * ((((|[x,y]| `2) / |.|[x,y]|.|) - sn) / (1 + sn)))]|
by A3, A32, Th18
.=
|[r,s]|
by A18, A30, A31, A33, A34
;
hence
f . |[x,y]| = |[r,s]|
by A3;
verum
end;
for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
( q `1 <= 0 & q <> 0. (TOP-REAL 2) )
then
f2 is continuous
by A3, A18, Th20;
hence
f is continuous
by A7, A9, A28, A29, JGRAPH_2:35; verum