let cn 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 < cn & cn < 1 & f = (cn -FanMorphS) | 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); :: thesis: for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st - 1 < cn & cn < 1 & f = (cn -FanMorphS) | 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); :: thesis: ( - 1 < cn & cn < 1 & f = (cn -FanMorphS) | 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 -FanMorphS) | 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) ) } ) ; :: thesis: f is continuous
then cn ^2 < 1 ^2 by SQUARE_1:50;
then A4: 1 - (cn ^2) > 0 by XREAL_1:50;
then A5: - (- (sqrt (1 - (cn ^2)))) > 0 by SQUARE_1:25;

A6: now :: thesis: not |[cn,(- (sqrt (1 - (cn ^2))))]| = 0. (TOP-REAL 2)

assume |[cn,(- (sqrt (1 - (cn ^2))))]| = 0. (TOP-REAL 2) ; :: thesis: contradiction
then - (- (- (sqrt (1 - (cn ^2))))) = - 0 by EUCLID:52, JGRAPH_2:3;
hence contradiction by A4, SQUARE_1:25; :: thesis: verum

end;

(- (- (sqrt (1 - (cn ^2))))) ^2 = 1 - (cn ^2) by A4, SQUARE_1:def 2;
then (|[cn,(- (sqrt (1 - (cn ^2))))]| `1) / |.|[cn,(- (sqrt (1 - (cn ^2))))]|.| = cn by A2, EUCLID:52;
then A7: |[cn,(- (sqrt (1 - (cn ^2))))]| in K0 by A3, A1, A6, A5;
then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;
A8: rng (proj2 * ((cn -FanMorphS) | K1)) c= the carrier of R^1 by TOPMETR:17;
A9: K0 c= B0

proof

let x be object ; :: 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 `1) / |.p8.| <= cn & p8 `2 <= 0 & p8 <> 0. (TOP-REAL 2) ) by A3;
hence x in B0 by A3; :: thesis: verum

end;

A10: dom ((cn -FanMorphS) | K1) c= dom (proj1 * ((cn -FanMorphS) | K1))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((cn -FanMorphS) | K1) or x in dom (proj1 * ((cn -FanMorphS) | K1)) )
assume A11: x in dom ((cn -FanMorphS) | K1) ; :: thesis: x in dom (proj1 * ((cn -FanMorphS) | K1))
then x in (dom (cn -FanMorphS)) /\ K1 by RELAT_1:61;
then x in dom (cn -FanMorphS) by XBOOLE_0:def 4;
then A12: ( dom proj1 = the carrier of (TOP-REAL 2) & (cn -FanMorphS) . x in rng (cn -FanMorphS) ) by FUNCT_1:3, FUNCT_2:def 1;
((cn -FanMorphS) | K1) . x = (cn -FanMorphS) . x by A11, FUNCT_1:47;
hence x in dom (proj1 * ((cn -FanMorphS) | K1)) by A11, A12, FUNCT_1:11; :: thesis: verum

end;

A13: rng (proj1 * ((cn -FanMorphS) | K1)) c= the carrier of R^1 by TOPMETR:17;
dom (proj1 * ((cn -FanMorphS) | K1)) c= dom ((cn -FanMorphS) | K1) by RELAT_1:25;
then dom (proj1 * ((cn -FanMorphS) | K1)) = dom ((cn -FanMorphS) | K1) by A10, XBOOLE_0:def 10
.= (dom (cn -FanMorphS)) /\ 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 -FanMorphS) | 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 `1) / |.p.|) - cn) / (1 + cn))

proof

let p be Point of (TOP-REAL 2); :: thesis: ( p in the carrier of ((TOP-REAL 2) | K1) implies g2 . p = |.p.| * ((((p `1) / |.p.|) - cn) / (1 + cn)) )
A14: dom ((cn -FanMorphS) | K1) = (dom (cn -FanMorphS)) /\ 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) ; :: thesis: 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, A15;
then A17: (cn -FanMorphS) . p = |[(|.p.| * ((((p `1) / |.p.|) - cn) / (1 + cn))),(|.p.| * (- (sqrt (1 - (((((p `1) / |.p.|) - cn) / (1 + cn)) ^2)))))]| by A3, Th115;
((cn -FanMorphS) | K1) . p = (cn -FanMorphS) . p by A16, A15, 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 A16, A14, A15, A17, 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)) ; :: 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 `1) / |.p.|) - cn) / (1 + cn)) ;
A19: dom ((cn -FanMorphS) | K1) c= dom (proj2 * ((cn -FanMorphS) | K1))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((cn -FanMorphS) | K1) or x in dom (proj2 * ((cn -FanMorphS) | K1)) )
assume A20: x in dom ((cn -FanMorphS) | K1) ; :: thesis: x in dom (proj2 * ((cn -FanMorphS) | K1))
then x in (dom (cn -FanMorphS)) /\ K1 by RELAT_1:61;
then x in dom (cn -FanMorphS) by XBOOLE_0:def 4;
then A21: ( dom proj2 = the carrier of (TOP-REAL 2) & (cn -FanMorphS) . x in rng (cn -FanMorphS) ) by FUNCT_1:3, FUNCT_2:def 1;
((cn -FanMorphS) | K1) . x = (cn -FanMorphS) . x by A20, FUNCT_1:47;
hence x in dom (proj2 * ((cn -FanMorphS) | K1)) by A20, A21, FUNCT_1:11; :: thesis: verum

end;

dom (proj2 * ((cn -FanMorphS) | K1)) c= dom ((cn -FanMorphS) | K1) by RELAT_1:25;
then dom (proj2 * ((cn -FanMorphS) | K1)) = dom ((cn -FanMorphS) | K1) by A19, XBOOLE_0:def 10
.= (dom (cn -FanMorphS)) /\ 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 -FanMorphS) | 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 `1) / |.p.|) - cn) / (1 + cn)) ^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 `1) / |.p.|) - cn) / (1 + cn)) ^2)))) )
A22: dom ((cn -FanMorphS) | K1) = (dom (cn -FanMorphS)) /\ 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) ; :: thesis: 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, A23;
then A25: (cn -FanMorphS) . p = |[(|.p.| * ((((p `1) / |.p.|) - cn) / (1 + cn))),(|.p.| * (- (sqrt (1 - (((((p `1) / |.p.|) - cn) / (1 + cn)) ^2)))))]| by A3, Th115;
((cn -FanMorphS) | K1) . p = (cn -FanMorphS) . p by A24, A23, 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 A24, A22, A23, A25, 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)))) ; :: 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 `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) )

proof

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

end;

then A28: f1 is continuous by A3, A26, Th119;
A29: 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; :: thesis: ( |[x,y]| in K1 & s = f2 . |[x,y]| & r = f1 . |[x,y]| implies f . |[x,y]| = |[s,r]| )
assume that
A30: |[x,y]| in K1 and
A31: ( s = f2 . |[x,y]| & r = f1 . |[x,y]| ) ; :: thesis: f . |[x,y]| = |[s,r]|
set p99 = |[x,y]|;
A32: 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, 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]| `1) / |.|[x,y]|.|) - cn) / (1 + cn)) ^2)))) by A26, A30;
((cn -FanMorphS) | K0) . |[x,y]| = (cn -FanMorphS) . |[x,y]| by A30, 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, A32, Th115
.= |[s,r]| by A18, A30, A31, A33, A34 ;
hence f . |[x,y]| = |[s,r]| 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 `2 <= 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 `2 <= 0 & q <> 0. (TOP-REAL 2) ) )
A35: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;
assume q in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: ( q `2 <= 0 & q <> 0. (TOP-REAL 2) )
then ex p3 being Point of (TOP-REAL 2) st
( q = p3 & (p3 `1) / |.p3.| <= cn & p3 `2 <= 0 & p3 <> 0. (TOP-REAL 2) ) by A3, A35;
hence ( q `2 <= 0 & q <> 0. (TOP-REAL 2) ) ; :: thesis: verum

end;

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