let sn be Real; :: thesis: 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); :: thesis: 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); :: thesis: ( - 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:56;
|[(- (sqrt (1 - (sn ^2 )))),sn]| `2 = sn by EUCLID:56;
then A2: |.|[(- (sqrt (1 - (sn ^2 )))),sn]|.| = sqrt (((- (sqrt (1 - (sn ^2 )))) ^2 ) + (sn ^2 )) by A1, JGRAPH_3:10
.= 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) ) } ) ; :: thesis: f is continuous
then sn ^2 < 1 ^2 by SQUARE_1:120;
then A4: 1 - (sn ^2 ) > 0 by XREAL_1:52;
then A5: - (- (sqrt (1 - (sn ^2 )))) > 0 by SQUARE_1:93;

A6: now

assume |[(- (sqrt (1 - (sn ^2 )))),sn]| = 0. (TOP-REAL 2) ; :: thesis: contradiction
then - (- (sqrt (1 - (sn ^2 )))) = - 0 by EUCLID:56, JGRAPH_2:11;
hence contradiction by A4, SQUARE_1:93; :: thesis: verum

end;

(sqrt (1 - (sn ^2 ))) ^2 = 1 - (sn ^2 ) by A4, SQUARE_1:def 4;
then (|[(- (sqrt (1 - (sn ^2 )))),sn]| `2 ) / |.|[(- (sqrt (1 - (sn ^2 )))),sn]|.| = sn by A2, EUCLID:56, SQUARE_1:83;
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:24;
A9: K0 c= B0

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in K0 or x in B0 )
assume x in K0 ; :: thesis: x in B0
then ex p8 being Point of (TOP-REAL 2) st
( x = p8 & (p8 `2 ) / |.p8.| >= sn & p8 `1 <= 0 & p8 <> 0. (TOP-REAL 2) ) by A3;
hence x in B0 by A3; :: thesis: verum

end;

A10: dom ((sn -FanMorphW ) | K1) c= dom (proj2 * ((sn -FanMorphW ) | K1))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((sn -FanMorphW ) | K1) or x in dom (proj2 * ((sn -FanMorphW ) | K1)) )
assume A11: x in dom ((sn -FanMorphW ) | K1) ; :: thesis: x in dom (proj2 * ((sn -FanMorphW ) | K1))
then x in (dom (sn -FanMorphW )) /\ K1 by RELAT_1:90;
then x in dom (sn -FanMorphW ) by XBOOLE_0:def 4;
then A12: ( dom proj2 = the carrier of (TOP-REAL 2) & (sn -FanMorphW ) . x in rng (sn -FanMorphW ) ) by FUNCT_1:12, FUNCT_2:def 1;
((sn -FanMorphW ) | K1) . x = (sn -FanMorphW ) . x by A11, FUNCT_1:70;
hence x in dom (proj2 * ((sn -FanMorphW ) | K1)) by A11, A12, FUNCT_1:21; :: thesis: verum

end;

A13: rng (proj2 * ((sn -FanMorphW ) | K1)) c= the carrier of R^1 by TOPMETR:24;
dom (proj2 * ((sn -FanMorphW ) | K1)) c= dom ((sn -FanMorphW ) | K1) by RELAT_1:44;
then dom (proj2 * ((sn -FanMorphW ) | K1)) = dom ((sn -FanMorphW ) | K1) by A10, XBOOLE_0:def 10
.= (dom (sn -FanMorphW )) /\ K1 by RELAT_1:90
.= 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:29 ;
then reconsider g2 = proj2 * ((sn -FanMorphW ) | K1) as Function of ((TOP-REAL 2) | K1),R^1 by A13, FUNCT_2:4;
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); :: thesis: ( 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:90
.= 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:29;
assume A16: p in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: 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, Th25;
((sn -FanMorphW ) | K1) . p = (sn -FanMorphW ) . p by A16, A15, FUNCT_1:72;
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:23
.= |[(|.p.| * (- (sqrt (1 - (((((p `2 ) / |.p.|) - sn) / (1 - sn)) ^2 ))))),(|.p.| * ((((p `2 ) / |.p.|) - sn) / (1 - sn)))]| `2 by PSCOMP_1:def 29
.= |.p.| * ((((p `2 ) / |.p.|) - sn) / (1 - sn)) by EUCLID:56 ;
hence g2 . p = |.p.| * ((((p `2 ) / |.p.|) - sn) / (1 - sn)) ; :: thesis: 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))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((sn -FanMorphW ) | K1) or x in dom (proj1 * ((sn -FanMorphW ) | K1)) )
assume A20: x in dom ((sn -FanMorphW ) | K1) ; :: thesis: x in dom (proj1 * ((sn -FanMorphW ) | K1))
then x in (dom (sn -FanMorphW )) /\ K1 by RELAT_1:90;
then x in dom (sn -FanMorphW ) by XBOOLE_0:def 4;
then A21: ( dom proj1 = the carrier of (TOP-REAL 2) & (sn -FanMorphW ) . x in rng (sn -FanMorphW ) ) by FUNCT_1:12, FUNCT_2:def 1;
((sn -FanMorphW ) | K1) . x = (sn -FanMorphW ) . x by A20, FUNCT_1:70;
hence x in dom (proj1 * ((sn -FanMorphW ) | K1)) by A20, A21, FUNCT_1:21; :: thesis: verum

end;

dom (proj1 * ((sn -FanMorphW ) | K1)) c= dom ((sn -FanMorphW ) | K1) by RELAT_1:44;
then dom (proj1 * ((sn -FanMorphW ) | K1)) = dom ((sn -FanMorphW ) | K1) by A19, XBOOLE_0:def 10
.= (dom (sn -FanMorphW )) /\ K1 by RELAT_1:90
.= 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:29 ;
then reconsider g1 = proj1 * ((sn -FanMorphW ) | K1) as Function of ((TOP-REAL 2) | K1),R^1 by A8, FUNCT_2:4;
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); :: thesis: ( 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:90
.= 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:29;
assume A24: p in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: 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, Th25;
((sn -FanMorphW ) | K1) . p = (sn -FanMorphW ) . p by A24, A23, FUNCT_1:72;
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:23
.= |[(|.p.| * (- (sqrt (1 - (((((p `2 ) / |.p.|) - sn) / (1 - sn)) ^2 ))))),(|.p.| * ((((p `2 ) / |.p.|) - sn) / (1 - sn)))]| `1 by PSCOMP_1:def 28
.= |.p.| * (- (sqrt (1 - (((((p `2 ) / |.p.|) - sn) / (1 - sn)) ^2 )))) by EUCLID:56 ;
hence g1 . p = |.p.| * (- (sqrt (1 - (((((p `2 ) / |.p.|) - sn) / (1 - sn)) ^2 )))) ; :: thesis: 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) )

proof

let q be Point of (TOP-REAL 2); :: thesis: ( q in the carrier of ((TOP-REAL 2) | K1) implies ( q `1 <= 0 & (q `2 ) / |.q.| >= sn & q <> 0. (TOP-REAL 2) ) )
A27: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:29;
assume q in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: ( q `1 <= 0 & (q `2 ) / |.q.| >= sn & q <> 0. (TOP-REAL 2) )
then ex p3 being Point of (TOP-REAL 2) st
( q = p3 & (p3 `2 ) / |.p3.| >= sn & p3 `1 <= 0 & p3 <> 0. (TOP-REAL 2) ) by A3, A27;
hence ( q `1 <= 0 & (q `2 ) / |.q.| >= sn & q <> 0. (TOP-REAL 2) ) ; :: thesis: verum

end;

then A28: f1 is continuous by A3, A26, Th28;
A29: for x, y, r, s being real number 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 number ; :: thesis: ( |[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]| ) ; :: thesis: 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:29;
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:72
.= |[(|.|[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, Th25
.= |[r,s]| by A18, A30, A31, A33, A34 ;
hence f . |[x,y]| = |[r,s]| by A3; :: thesis: 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) )

proof

let q be Point of (TOP-REAL 2); :: thesis: ( q in the carrier of ((TOP-REAL 2) | K1) implies ( q `1 <= 0 & q <> 0. (TOP-REAL 2) ) )
A35: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:29;
assume q in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: ( q `1 <= 0 & q <> 0. (TOP-REAL 2) )
then ex p3 being Point of (TOP-REAL 2) st
( q = p3 & (p3 `2 ) / |.p3.| >= sn & p3 `1 <= 0 & p3 <> 0. (TOP-REAL 2) ) by A3, A35;
hence ( q `1 <= 0 & q <> 0. (TOP-REAL 2) ) ; :: thesis: verum

end;

then f2 is continuous by A3, A18, Th26;
hence f is continuous by A7, A9, A28, A29, JGRAPH_2:45; :: thesis: verum