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 -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); :: thesis: 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); :: thesis: ( - 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 )
assume A1: ( - 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) ) } ) ; :: thesis: f is continuous
set sn = sqrt (1 - (cn ^2 ));
set p0 = |[cn,(sqrt (1 - (cn ^2 )))]|;
A2: |[cn,(sqrt (1 - (cn ^2 )))]| `1 = cn by EUCLID:56;
A3: |[cn,(sqrt (1 - (cn ^2 )))]| `2 = sqrt (1 - (cn ^2 )) by EUCLID:56;
cn ^2 < 1 ^2 by A1, SQUARE_1:120;
then A4: 1 - (cn ^2 ) > 0 by XREAL_1:52;
then A5: |[cn,(sqrt (1 - (cn ^2 )))]| `2 > 0 by A3, SQUARE_1:93;
A6: |.|[cn,(sqrt (1 - (cn ^2 )))]|.| = sqrt (((sqrt (1 - (cn ^2 ))) ^2 ) + (cn ^2 )) by A2, A3, JGRAPH_3:10;
(sqrt (1 - (cn ^2 ))) ^2 = 1 - (cn ^2 ) by A4, SQUARE_1:def 4;
then (|[cn,(sqrt (1 - (cn ^2 )))]| `1 ) / |.|[cn,(sqrt (1 - (cn ^2 )))]|.| = cn by A6, EUCLID:56, SQUARE_1:83;
then A7: |[cn,(sqrt (1 - (cn ^2 )))]| in K0 by A1, A5, JGRAPH_2:11;
then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;
A8: 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 consider p8 being Point of (TOP-REAL 2) such that
A9: ( x = p8 & (p8 `1 ) / |.p8.| <= cn & p8 `2 >= 0 & p8 <> 0. (TOP-REAL 2) ) by A1;
thus x in B0 by A1, A9; :: thesis: verum

end;

A10: dom (proj1 * ((cn -FanMorphN ) | K1)) c= dom ((cn -FanMorphN ) | K1) by RELAT_1:44;
dom ((cn -FanMorphN ) | K1) c= dom (proj1 * ((cn -FanMorphN ) | K1))

proof

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

end;

then A15: dom (proj1 * ((cn -FanMorphN ) | K1)) = dom ((cn -FanMorphN ) | K1) by A10, XBOOLE_0:def 10
.= (dom (cn -FanMorphN )) /\ 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 ;
rng (proj1 * ((cn -FanMorphN ) | K1)) c= the carrier of R^1 by TOPMETR:24;
then reconsider g2 = proj1 * ((cn -FanMorphN ) | K1) as Function of ((TOP-REAL 2) | K1),R^1 by A15, FUNCT_2:4;
A16: dom (proj2 * ((cn -FanMorphN ) | K1)) c= dom ((cn -FanMorphN ) | K1) by RELAT_1:44;
dom ((cn -FanMorphN ) | K1) c= dom (proj2 * ((cn -FanMorphN ) | K1))

proof

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

end;

then A21: dom (proj2 * ((cn -FanMorphN ) | K1)) = dom ((cn -FanMorphN ) | K1) by A16, XBOOLE_0:def 10
.= (dom (cn -FanMorphN )) /\ 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 ;
rng (proj2 * ((cn -FanMorphN ) | K1)) c= the carrier of R^1 by TOPMETR:24;
then reconsider g1 = proj2 * ((cn -FanMorphN ) | K1) as Function of ((TOP-REAL 2) | K1),R^1 by A21, FUNCT_2:4;
A22: 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) ) )
assume A23: q in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: ( q `2 >= 0 & q <> 0. (TOP-REAL 2) )
the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:29;
then consider p3 being Point of (TOP-REAL 2) such that
A24: ( q = p3 & (p3 `1 ) / |.p3.| <= cn & p3 `2 >= 0 & p3 <> 0. (TOP-REAL 2) ) by A1, A23;
thus ( q `2 >= 0 & q <> 0. (TOP-REAL 2) ) by A24; :: thesis: verum

end;

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)) )
assume A25: p in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: g2 . p = |.p.| * ((((p `1 ) / |.p.|) - cn) / (1 + cn))
A26: dom ((cn -FanMorphN ) | K1) = (dom (cn -FanMorphN )) /\ K1 by RELAT_1:90
.= the carrier of (TOP-REAL 2) /\ K1 by FUNCT_2:def 1
.= K1 by XBOOLE_1:28 ;
A27: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:29;
then consider p3 being Point of (TOP-REAL 2) such that
A28: ( p = p3 & (p3 `1 ) / |.p3.| <= cn & p3 `2 >= 0 & p3 <> 0. (TOP-REAL 2) ) by A1, A25;
A29: (cn -FanMorphN ) . p = |[(|.p.| * ((((p `1 ) / |.p.|) - cn) / (1 + cn))),(|.p.| * (sqrt (1 - (((((p `1 ) / |.p.|) - cn) / (1 + cn)) ^2 ))))]| by A1, A28, Th58;
((cn -FanMorphN ) | K1) . p = (cn -FanMorphN ) . p by A25, A27, FUNCT_1:72;
then g2 . p = proj1 . |[(|.p.| * ((((p `1 ) / |.p.|) - cn) / (1 + cn))),(|.p.| * (sqrt (1 - (((((p `1 ) / |.p.|) - cn) / (1 + cn)) ^2 ))))]| by A25, A26, A27, A29, FUNCT_1:23
.= |[(|.p.| * ((((p `1 ) / |.p.|) - cn) / (1 + cn))),(|.p.| * (sqrt (1 - (((((p `1 ) / |.p.|) - cn) / (1 + cn)) ^2 ))))]| `1 by PSCOMP_1:def 28
.= |.p.| * ((((p `1 ) / |.p.|) - cn) / (1 + cn)) by EUCLID:56 ;
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
A30: 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)) ;
A31: f2 is continuous by A1, A22, A30, Th60;
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 ))) )
assume A32: p in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: g1 . p = |.p.| * (sqrt (1 - (((((p `1 ) / |.p.|) - cn) / (1 + cn)) ^2 )))
A33: dom ((cn -FanMorphN ) | K1) = (dom (cn -FanMorphN )) /\ K1 by RELAT_1:90
.= the carrier of (TOP-REAL 2) /\ K1 by FUNCT_2:def 1
.= K1 by XBOOLE_1:28 ;
A34: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:29;
then consider p3 being Point of (TOP-REAL 2) such that
A35: ( p = p3 & (p3 `1 ) / |.p3.| <= cn & p3 `2 >= 0 & p3 <> 0. (TOP-REAL 2) ) by A1, A32;
A36: (cn -FanMorphN ) . p = |[(|.p.| * ((((p `1 ) / |.p.|) - cn) / (1 + cn))),(|.p.| * (sqrt (1 - (((((p `1 ) / |.p.|) - cn) / (1 + cn)) ^2 ))))]| by A1, A35, Th58;
((cn -FanMorphN ) | K1) . p = (cn -FanMorphN ) . p by A32, A34, FUNCT_1:72;
then g1 . p = proj2 . |[(|.p.| * ((((p `1 ) / |.p.|) - cn) / (1 + cn))),(|.p.| * (sqrt (1 - (((((p `1 ) / |.p.|) - cn) / (1 + cn)) ^2 ))))]| by A32, A33, A34, A36, FUNCT_1:23
.= |[(|.p.| * ((((p `1 ) / |.p.|) - cn) / (1 + cn))),(|.p.| * (sqrt (1 - (((((p `1 ) / |.p.|) - cn) / (1 + cn)) ^2 ))))]| `2 by PSCOMP_1:def 29
.= |.p.| * (sqrt (1 - (((((p `1 ) / |.p.|) - cn) / (1 + cn)) ^2 ))) by EUCLID:56 ;
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
A37: 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) ) )
assume A38: q in the carrier of ((TOP-REAL 2) | K1) ; :: thesis: ( q `2 >= 0 & (q `1 ) / |.q.| <= cn & q <> 0. (TOP-REAL 2) )
the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:29;
then consider p3 being Point of (TOP-REAL 2) such that
A39: ( q = p3 & (p3 `1 ) / |.p3.| <= cn & p3 `2 >= 0 & p3 <> 0. (TOP-REAL 2) ) by A1, A38;
thus ( q `2 >= 0 & (q `1 ) / |.q.| <= cn & q <> 0. (TOP-REAL 2) ) by A39; :: thesis: verum

end;

then A40: f1 is continuous by A1, A37, Th62;
for x, y, s, r being real number 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 number ; :: thesis: ( |[x,y]| in K1 & s = f2 . |[x,y]| & r = f1 . |[x,y]| implies f . |[x,y]| = |[s,r]| )
assume A41: ( |[x,y]| in K1 & s = f2 . |[x,y]| & r = f1 . |[x,y]| ) ; :: thesis: f . |[x,y]| = |[s,r]|
set p99 = |[x,y]|;
A42: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:29;
consider p3 being Point of (TOP-REAL 2) such that
A43: ( |[x,y]| = p3 & (p3 `1 ) / |.p3.| <= cn & p3 `2 >= 0 & p3 <> 0. (TOP-REAL 2) ) by A1, A41;
A44: f1 . |[x,y]| = |.|[x,y]|.| * (sqrt (1 - (((((|[x,y]| `1 ) / |.|[x,y]|.|) - cn) / (1 + cn)) ^2 ))) by A37, A41, A42;
((cn -FanMorphN ) | K0) . |[x,y]| = (cn -FanMorphN ) . |[x,y]| by A41, FUNCT_1:72
.= |[(|.|[x,y]|.| * ((((|[x,y]| `1 ) / |.|[x,y]|.|) - cn) / (1 + cn))),(|.|[x,y]|.| * (sqrt (1 - (((((|[x,y]| `1 ) / |.|[x,y]|.|) - cn) / (1 + cn)) ^2 ))))]| by A1, A43, Th58
.= |[s,r]| by A30, A41, A42, A44 ;
hence f . |[x,y]| = |[s,r]| by A1; :: thesis: verum

end;

hence f is continuous by A7, A8, A31, A40, JGRAPH_2:45; :: thesis: verum