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 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( 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 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( 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 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( 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 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( 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;
then |[cn,(- (sqrt (1 - (cn ^2))))]| in K0 by A3, A1, A5;
then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;
(- (- (sqrt (1 - (cn ^2))))) ^2 = 1 - (cn ^2) by A4, SQUARE_1:def 2;
then A7: (|[cn,(- (sqrt (1 - (cn ^2))))]| `1) / |.|[cn,(- (sqrt (1 - (cn ^2))))]|.| = cn by A2, EUCLID:52;
then A8: |[cn,(- (sqrt (1 - (cn ^2))))]| in { p where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| >= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } by A1, A6, A5;
not |[cn,(- (sqrt (1 - (cn ^2))))]| in {(0. (TOP-REAL 2))} by A6, TARSKI:def 1;
then reconsider D = B0 as non empty Subset of (TOP-REAL 2) by A3, XBOOLE_0:def 5;
K1 c= D
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in K1 or x in D )
assume A9: x in K1 ; :: thesis: x in D
then ex p6 being Point of (TOP-REAL 2) st
( p6 = x & p6 `2 <= 0 & p6 <> 0. (TOP-REAL 2) ) by A3;
then not x in {(0. (TOP-REAL 2))} by TARSKI:def 1;
hence x in D by A3, A9, XBOOLE_0:def 5; :: thesis: verum
end;
then D = K1 \/ D by XBOOLE_1:12;
then A10: (TOP-REAL 2) | K1 is SubSpace of (TOP-REAL 2) | D by TOPMETR:4;
A11: { p where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| <= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } c= K1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| <= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } or x in K1 )
assume x in { p where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| <= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } ; :: thesis: x in K1
then ex p being Point of (TOP-REAL 2) st
( p = x & (p `1) / |.p.| <= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) ;
hence x in K1 by A3; :: thesis: verum
end;
A12: { p where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| >= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } c= K1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| >= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } or x in K1 )
assume x in { p where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| >= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } ; :: thesis: x in K1
then ex p being Point of (TOP-REAL 2) st
( p = x & (p `1) / |.p.| >= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) ;
hence x in K1 by A3; :: thesis: verum
end;
then reconsider K00 = { p where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| >= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | K1) by A8, PRE_TOPC:8;
the carrier of ((TOP-REAL 2) | D) = D by PRE_TOPC:8;
then A13: rng (f | K00) c= D ;
|[cn,(- (sqrt (1 - (cn ^2))))]| in { p where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| <= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } by A1, A6, A5, A7;
then reconsider K11 = { p where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| <= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | K1) by A11, PRE_TOPC:8;
the carrier of ((TOP-REAL 2) | D) = D by PRE_TOPC:8;
then A14: rng (f | K11) c= D ;
the carrier of ((TOP-REAL 2) | B0) = the carrier of ((TOP-REAL 2) | D) ;
then A15: dom f = the carrier of ((TOP-REAL 2) | K1) by FUNCT_2:def 1
.= K1 by PRE_TOPC:8 ;
then dom (f | K00) = K00 by A12, RELAT_1:62
.= the carrier of (((TOP-REAL 2) | K1) | K00) by PRE_TOPC:8 ;
then reconsider f1 = f | K00 as Function of (((TOP-REAL 2) | K1) | K00),((TOP-REAL 2) | D) by A13, FUNCT_2:2;
dom (f | K11) = K11 by A11, A15, RELAT_1:62
.= the carrier of (((TOP-REAL 2) | K1) | K11) by PRE_TOPC:8 ;
then reconsider f2 = f | K11 as Function of (((TOP-REAL 2) | K1) | K11),((TOP-REAL 2) | D) by A14, FUNCT_2:2;
A16: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;
defpred S1[ Point of (TOP-REAL 2)] means ( ($1 `1) / |.$1.| >= cn & $1 `2 <= 0 & $1 <> 0. (TOP-REAL 2) );
A17: dom f2 = the carrier of (((TOP-REAL 2) | K1) | K11) by FUNCT_2:def 1
.= K11 by PRE_TOPC:8 ;
{ p where p is Point of (TOP-REAL 2) : S1[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
 then reconsider K001 = { p where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| >= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } as non empty Subset of (TOP-REAL 2) by A8;
A18: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;
defpred S2[ Point of (TOP-REAL 2)] means ( $1 `1 >= cn * |.$1.| & $1 `2 <= 0 );
{ p where p is Point of (TOP-REAL 2) : S2[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
 then reconsider K003 = { p where p is Point of (TOP-REAL 2) : ( p `1 >= cn * |.p.| & p `2 <= 0 ) } as Subset of (TOP-REAL 2) ;
defpred S3[ Point of (TOP-REAL 2)] means ( ($1 `1) / |.$1.| <= cn & $1 `2 <= 0 & $1 <> 0. (TOP-REAL 2) );
A19: { p where p is Point of (TOP-REAL 2) : S3[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
 A20: rng ((cn -FanMorphS) | K001) c= K1
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((cn -FanMorphS) | K001) or y in K1 )
assume y in rng ((cn -FanMorphS) | K001) ; :: thesis: y in K1
then consider x being object such that
A21: x in dom ((cn -FanMorphS) | K001) and
A22: y = ((cn -FanMorphS) | K001) . x by FUNCT_1:def 3;
x in dom (cn -FanMorphS) by A21, RELAT_1:57;
then reconsider q = x as Point of (TOP-REAL 2) ;
A23: y = (cn -FanMorphS) . q by A21, A22, FUNCT_1:47;
dom ((cn -FanMorphS) | K001) = (dom (cn -FanMorphS)) /\ K001 by RELAT_1:61
.= the carrier of (TOP-REAL 2) /\ K001 by FUNCT_2:def 1
.= K001 by XBOOLE_1:28 ;
then A24: ex p2 being Point of (TOP-REAL 2) st
( p2 = q & (p2 `1) / |.p2.| >= cn & p2 `2 <= 0 & p2 <> 0. (TOP-REAL 2) ) by A21;
then A25: ((q `1) / |.q.|) - cn >= 0 by XREAL_1:48;
|.q.| <> 0 by A24, TOPRNS_1:24;
then A26: |.q.| ^2 > 0 ^2 by SQUARE_1:12;
set q4 = |[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 - cn)) ^2)))))]|;
A27: |[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 - cn)) ^2)))))]| `1 = |.q.| * ((((q `1) / |.q.|) - cn) / (1 - cn)) by EUCLID:52;
A28: 1 - cn > 0 by A3, XREAL_1:149;
0 <= (q `2) ^2 by XREAL_1:63;
then 0 + ((q `1) ^2) <= ((q `1) ^2) + ((q `2) ^2) by XREAL_1:7;
then (q `1) ^2 <= |.q.| ^2 by JGRAPH_3:1;
then ((q `1) ^2) / (|.q.| ^2) <= (|.q.| ^2) / (|.q.| ^2) by XREAL_1:72;
then ((q `1) ^2) / (|.q.| ^2) <= 1 by A26, XCMPLX_1:60;
then ((q `1) / |.q.|) ^2 <= 1 by XCMPLX_1:76;
then 1 >= (q `1) / |.q.| by SQUARE_1:51;
then 1 - cn >= ((q `1) / |.q.|) - cn by XREAL_1:9;
then - (1 - cn) <= - (((q `1) / |.q.|) - cn) by XREAL_1:24;
then (- (1 - cn)) / (1 - cn) <= (- (((q `1) / |.q.|) - cn)) / (1 - cn) by A28, XREAL_1:72;
then - 1 <= (- (((q `1) / |.q.|) - cn)) / (1 - cn) by A28, XCMPLX_1:197;
then ((- (((q `1) / |.q.|) - cn)) / (1 - cn)) ^2 <= 1 ^2 by A28, A25, SQUARE_1:49;
then A29: 1 - (((- (((q `1) / |.q.|) - cn)) / (1 - cn)) ^2) >= 0 by XREAL_1:48;
then A30: 1 - ((- ((((q `1) / |.q.|) - cn) / (1 - cn))) ^2) >= 0 by XCMPLX_1:187;
sqrt (1 - (((- (((q `1) / |.q.|) - cn)) / (1 - cn)) ^2)) >= 0 by A29, SQUARE_1:def 2;
then sqrt (1 - (((- (((q `1) / |.q.|) - cn)) ^2) / ((1 - cn) ^2))) >= 0 by XCMPLX_1:76;
then sqrt (1 - (((((q `1) / |.q.|) - cn) ^2) / ((1 - cn) ^2))) >= 0 ;
then A31: sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 - cn)) ^2)) >= 0 by XCMPLX_1:76;
A32: |[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 - cn)) ^2)))))]| `2 = |.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 - cn)) ^2)))) by EUCLID:52;
then A33: (|[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 - cn)) ^2)))))]| `2) ^2 = (|.q.| ^2) * ((sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 - cn)) ^2))) ^2)
.= (|.q.| ^2) * (1 - (((((q `1) / |.q.|) - cn) / (1 - cn)) ^2)) by A30, SQUARE_1:def 2 ;
|.|[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 - cn)) ^2)))))]|.| ^2 = ((|[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 - cn)) ^2)))))]| `1) ^2) + ((|[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 - cn)) ^2)))))]| `2) ^2) by JGRAPH_3:1
.= |.q.| ^2 by A27, A33 ;
then A34: |[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 - cn)) ^2)))))]| <> 0. (TOP-REAL 2) by A26, TOPRNS_1:23;
(cn -FanMorphS) . q = |[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 - cn)) ^2)))))]| by A3, A24, Th115;
hence y in K1 by A3, A23, A32, A31, A34; :: thesis: verum
end;
A35: dom (cn -FanMorphS) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then dom ((cn -FanMorphS) | K001) = K001 by RELAT_1:62
.= the carrier of ((TOP-REAL 2) | K001) by PRE_TOPC:8 ;
then reconsider f3 = (cn -FanMorphS) | K001 as Function of ((TOP-REAL 2) | K001),((TOP-REAL 2) | K1) by A18, A20, FUNCT_2:2;
A36: K003 is closed by Th122;
defpred S4[ Point of (TOP-REAL 2)] means ( $1 `1 <= cn * |.$1.| & $1 `2 <= 0 );
{ p where p is Point of (TOP-REAL 2) : S4[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
 then reconsider K004 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= cn * |.p.| & p `2 <= 0 ) } as Subset of (TOP-REAL 2) ;
A37: K004 /\ K1 c= K11
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in K004 /\ K1 or x in K11 )
assume A38: x in K004 /\ K1 ; :: thesis: x in K11
then x in K004 by XBOOLE_0:def 4;
then consider q1 being Point of (TOP-REAL 2) such that
A39: q1 = x and
A40: q1 `1 <= cn * |.q1.| and
q1 `2 <= 0 ;
x in K1 by A38, XBOOLE_0:def 4;
then A41: ex q2 being Point of (TOP-REAL 2) st
( q2 = x & q2 `2 <= 0 & q2 <> 0. (TOP-REAL 2) ) by A3;
(q1 `1) / |.q1.| <= (cn * |.q1.|) / |.q1.| by A40, XREAL_1:72;
then (q1 `1) / |.q1.| <= cn by A39, A41, TOPRNS_1:24, XCMPLX_1:89;
hence x in K11 by A39, A41; :: thesis: verum
end;
A42: K004 is closed by Th123;
the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;
then ( ((TOP-REAL 2) | K1) | K00 = (TOP-REAL 2) | K001 & f1 = f3 ) by A3, FUNCT_1:51, GOBOARD9:2;
then A43: f1 is continuous by A3, A10, Th120, PRE_TOPC:26;
A44: [#] ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:def 5;
|[cn,(- (sqrt (1 - (cn ^2))))]| in { p where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| <= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } by A1, A6, A5, A7;
then reconsider K111 = { p where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| <= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } as non empty Subset of (TOP-REAL 2) by A19;
A45: rng ((cn -FanMorphS) | K111) c= K1
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((cn -FanMorphS) | K111) or y in K1 )
assume y in rng ((cn -FanMorphS) | K111) ; :: thesis: y in K1
then consider x being object such that
A46: x in dom ((cn -FanMorphS) | K111) and
A47: y = ((cn -FanMorphS) | K111) . x by FUNCT_1:def 3;
x in dom (cn -FanMorphS) by A46, RELAT_1:57;
then reconsider q = x as Point of (TOP-REAL 2) ;
A48: y = (cn -FanMorphS) . q by A46, A47, FUNCT_1:47;
dom ((cn -FanMorphS) | K111) = (dom (cn -FanMorphS)) /\ K111 by RELAT_1:61
.= the carrier of (TOP-REAL 2) /\ K111 by FUNCT_2:def 1
.= K111 by XBOOLE_1:28 ;
then A49: ex p2 being Point of (TOP-REAL 2) st
( p2 = q & (p2 `1) / |.p2.| <= cn & p2 `2 <= 0 & p2 <> 0. (TOP-REAL 2) ) by A46;
then A50: ((q `1) / |.q.|) - cn <= 0 by XREAL_1:47;
|.q.| <> 0 by A49, TOPRNS_1:24;
then A51: |.q.| ^2 > 0 ^2 by SQUARE_1:12;
set q4 = |[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2)))))]|;
A52: |[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2)))))]| `1 = |.q.| * ((((q `1) / |.q.|) - cn) / (1 + cn)) by EUCLID:52;
A53: 1 + cn > 0 by A3, XREAL_1:148;
0 <= (q `2) ^2 by XREAL_1:63;
then ( |.q.| ^2 = ((q `1) ^2) + ((q `2) ^2) & 0 + ((q `1) ^2) <= ((q `1) ^2) + ((q `2) ^2) ) by JGRAPH_3:1, XREAL_1:7;
then ((q `1) ^2) / (|.q.| ^2) <= (|.q.| ^2) / (|.q.| ^2) by XREAL_1:72;
then ((q `1) ^2) / (|.q.| ^2) <= 1 by A51, XCMPLX_1:60;
then ((q `1) / |.q.|) ^2 <= 1 by XCMPLX_1:76;
then - 1 <= (q `1) / |.q.| by SQUARE_1:51;
then (- 1) - cn <= ((q `1) / |.q.|) - cn by XREAL_1:9;
then (- (1 + cn)) / (1 + cn) <= (((q `1) / |.q.|) - cn) / (1 + cn) by A53, XREAL_1:72;
then - 1 <= (((q `1) / |.q.|) - cn) / (1 + cn) by A53, XCMPLX_1:197;
then A54: ((((q `1) / |.q.|) - cn) / (1 + cn)) ^2 <= 1 ^2 by A53, A50, SQUARE_1:49;
then A55: 1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2) >= 0 by XREAL_1:48;
1 - ((- ((((q `1) / |.q.|) - cn) / (1 + cn))) ^2) >= 0 by A54, XREAL_1:48;
then 1 - (((- (((q `1) / |.q.|) - cn)) / (1 + cn)) ^2) >= 0 by XCMPLX_1:187;
then sqrt (1 - (((- (((q `1) / |.q.|) - cn)) / (1 + cn)) ^2)) >= 0 by SQUARE_1:def 2;
then sqrt (1 - (((- (((q `1) / |.q.|) - cn)) ^2) / ((1 + cn) ^2))) >= 0 by XCMPLX_1:76;
then sqrt (1 - (((((q `1) / |.q.|) - cn) ^2) / ((1 + cn) ^2))) >= 0 ;
then A56: sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2)) >= 0 by XCMPLX_1:76;
A57: |[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2)))))]| `2 = |.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2)))) by EUCLID:52;
then A58: (|[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2)))))]| `2) ^2 = (|.q.| ^2) * ((sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2))) ^2)
.= (|.q.| ^2) * (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2)) by A55, SQUARE_1:def 2 ;
|.|[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2)))))]|.| ^2 = ((|[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2)))))]| `1) ^2) + ((|[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2)))))]| `2) ^2) by JGRAPH_3:1
.= |.q.| ^2 by A52, A58 ;
then A59: |[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2)))))]| <> 0. (TOP-REAL 2) by A51, TOPRNS_1:23;
(cn -FanMorphS) . q = |[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2)))))]| by A3, A49, Th115;
hence y in K1 by A3, A48, A57, A56, A59; :: thesis: verum
end;
dom ((cn -FanMorphS) | K111) = K111 by A35, RELAT_1:62
.= the carrier of ((TOP-REAL 2) | K111) by PRE_TOPC:8 ;
then reconsider f4 = (cn -FanMorphS) | K111 as Function of ((TOP-REAL 2) | K111),((TOP-REAL 2) | K1) by A16, A45, FUNCT_2:2;
the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;
then ( ((TOP-REAL 2) | K1) | K11 = (TOP-REAL 2) | K111 & f2 = f4 ) by A3, FUNCT_1:51, GOBOARD9:2;
then A60: f2 is continuous by A3, A10, Th121, PRE_TOPC:26;
set T1 = ((TOP-REAL 2) | K1) | K00;
set T2 = ((TOP-REAL 2) | K1) | K11;
A61: [#] (((TOP-REAL 2) | K1) | K11) = K11 by PRE_TOPC:def 5;
K11 c= K004 /\ K1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in K11 or x in K004 /\ K1 )
assume x in K11 ; :: thesis: x in K004 /\ K1
then consider p being Point of (TOP-REAL 2) such that
A62: p = x and
A63: (p `1) / |.p.| <= cn and
A64: p `2 <= 0 and
A65: p <> 0. (TOP-REAL 2) ;
((p `1) / |.p.|) * |.p.| <= cn * |.p.| by A63, XREAL_1:64;
then p `1 <= cn * |.p.| by A65, TOPRNS_1:24, XCMPLX_1:87;
then A66: x in K004 by A62, A64;
x in K1 by A3, A62, A64, A65;
hence x in K004 /\ K1 by A66, XBOOLE_0:def 4; :: thesis: verum
end;
then K11 = K004 /\ ([#] ((TOP-REAL 2) | K1)) by A44, A37, XBOOLE_0:def 10;
then A67: K11 is closed by A42, PRE_TOPC:13;
A68: K003 /\ K1 c= K00
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in K003 /\ K1 or x in K00 )
assume A69: x in K003 /\ K1 ; :: thesis: x in K00
then x in K003 by XBOOLE_0:def 4;
then consider q1 being Point of (TOP-REAL 2) such that
A70: q1 = x and
A71: q1 `1 >= cn * |.q1.| and
q1 `2 <= 0 ;
x in K1 by A69, XBOOLE_0:def 4;
then A72: ex q2 being Point of (TOP-REAL 2) st
( q2 = x & q2 `2 <= 0 & q2 <> 0. (TOP-REAL 2) ) by A3;
(q1 `1) / |.q1.| >= (cn * |.q1.|) / |.q1.| by A71, XREAL_1:72;
then (q1 `1) / |.q1.| >= cn by A70, A72, TOPRNS_1:24, XCMPLX_1:89;
hence x in K00 by A70, A72; :: thesis: verum
end;
A73: the carrier of ((TOP-REAL 2) | K1) = K0 by PRE_TOPC:8;
A74: D <> {} ;
A75: [#] (((TOP-REAL 2) | K1) | K00) = K00 by PRE_TOPC:def 5;
A76: for p being object st p in ([#] (((TOP-REAL 2) | K1) | K00)) /\ ([#] (((TOP-REAL 2) | K1) | K11)) holds
f1 . p = f2 . p
proof
let p be object ; :: thesis: ( p in ([#] (((TOP-REAL 2) | K1) | K00)) /\ ([#] (((TOP-REAL 2) | K1) | K11)) implies f1 . p = f2 . p )
assume A77: p in ([#] (((TOP-REAL 2) | K1) | K00)) /\ ([#] (((TOP-REAL 2) | K1) | K11)) ; :: thesis: f1 . p = f2 . p
then p in K00 by A75, XBOOLE_0:def 4;
hence f1 . p = f . p by FUNCT_1:49
.= f2 . p by A61, A77, FUNCT_1:49 ;
:: thesis: verum
end;
K00 c= K003 /\ K1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in K00 or x in K003 /\ K1 )
assume x in K00 ; :: thesis: x in K003 /\ K1
then consider p being Point of (TOP-REAL 2) such that
A78: p = x and
A79: (p `1) / |.p.| >= cn and
A80: p `2 <= 0 and
A81: p <> 0. (TOP-REAL 2) ;
((p `1) / |.p.|) * |.p.| >= cn * |.p.| by A79, XREAL_1:64;
then p `1 >= cn * |.p.| by A81, TOPRNS_1:24, XCMPLX_1:87;
then A82: x in K003 by A78, A80;
x in K1 by A3, A78, A80, A81;
hence x in K003 /\ K1 by A82, XBOOLE_0:def 4; :: thesis: verum
end;
then K00 = K003 /\ ([#] ((TOP-REAL 2) | K1)) by A44, A68, XBOOLE_0:def 10;
then A83: K00 is closed by A36, PRE_TOPC:13;
A84: K1 c= K00 \/ K11
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in K1 or x in K00 \/ K11 )
assume x in K1 ; :: thesis: x in K00 \/ K11
then consider p being Point of (TOP-REAL 2) such that
A85: ( p = x & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) by A3;
per cases ( (p `1) / |.p.| >= cn or (p `1) / |.p.| < cn ) ;
suppose (p `1) / |.p.| >= cn ; :: thesis: x in K00 \/ K11
then x in K00 by A85;
hence x in K00 \/ K11 by XBOOLE_0:def 3; :: thesis: verum
end;
suppose (p `1) / |.p.| < cn ; :: thesis: x in K00 \/ K11
then x in K11 by A85;
hence x in K00 \/ K11 by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
then ([#] (((TOP-REAL 2) | K1) | K00)) \/ ([#] (((TOP-REAL 2) | K1) | K11)) = [#] ((TOP-REAL 2) | K1) by A75, A61, A44, XBOOLE_0:def 10;
then consider h being Function of ((TOP-REAL 2) | K1),((TOP-REAL 2) | D) such that
A86: h = f1 +* f2 and
A87: h is continuous by A75, A61, A83, A67, A43, A60, A76, JGRAPH_2:1;
A88: dom h = the carrier of ((TOP-REAL 2) | K1) by FUNCT_2:def 1;
A89: dom f1 = the carrier of (((TOP-REAL 2) | K1) | K00) by FUNCT_2:def 1
.= K00 by PRE_TOPC:8 ;
A90: for y being object st y in dom h holds
h . y = f . y
proof
let y be object ; :: thesis: ( y in dom h implies h . y = f . y )
assume A91: y in dom h ; :: thesis: h . y = f . y
per cases ( ( y in K00 & not y in K11 ) or y in K11 ) by A84, A88, A73, A91, XBOOLE_0:def 3;
suppose A92: ( y in K00 & not y in K11 ) ; :: thesis: h . y = f . y
then y in (dom f1) \/ (dom f2) by A89, XBOOLE_0:def 3;
hence h . y = f1 . y by A17, A86, A92, FUNCT_4:def 1
.= f . y by A92, FUNCT_1:49 ;
:: thesis: verum
end;
suppose A93: y in K11 ; :: thesis: h . y = f . y
then y in (dom f1) \/ (dom f2) by A17, XBOOLE_0:def 3;
hence h . y = f2 . y by A17, A86, A93, FUNCT_4:def 1
.= f . y by A93, FUNCT_1:49 ;
:: thesis: verum
end;
end;
end;
K0 = the carrier of ((TOP-REAL 2) | K0) by PRE_TOPC:8
.= dom f by A74, FUNCT_2:def 1 ;
hence f is continuous by A87, A88, A90, FUNCT_1:2, PRE_TOPC:8; :: thesis: verum