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