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 )
assume A1: ( - 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
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;
A5: now
assume |[cn,(- (sqrt (1 - (cn ^2 ))))]| = 0. (TOP-REAL 2) ; :: thesis: contradiction
then - (- (- (sqrt (1 - (cn ^2 ))))) = - 0 by EUCLID:56, JGRAPH_2:11;
hence contradiction by A4, SQUARE_1:93; :: thesis: verum
end;
- (- (sqrt (1 - (cn ^2 )))) > 0 by A4, SQUARE_1:93;
then A6: - (sqrt (1 - (cn ^2 ))) < 0 ;
A7: |.|[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 A8: (|[cn,(- (sqrt (1 - (cn ^2 ))))]| `1 ) / |.|[cn,(- (sqrt (1 - (cn ^2 ))))]|.| = cn by A7, EUCLID:56, SQUARE_1:83;
|[cn,(- (sqrt (1 - (cn ^2 ))))]| in K0 by A1, A3, A5, A6;
then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;
( |[cn,(- (sqrt (1 - (cn ^2 ))))]| in the carrier of (TOP-REAL 2) & not |[cn,(- (sqrt (1 - (cn ^2 ))))]| in {(0. (TOP-REAL 2))} ) by A5, TARSKI:def 1;
then reconsider D = B0 as non empty Subset of (TOP-REAL 2) by A1, XBOOLE_0:def 5;
A9: |[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 A3, A5, A6, A8;
defpred S1[ Point of (TOP-REAL 2)] means ( ($1 `1 ) / |.$1.| >= cn & $1 `2 <= 0 & $1 <> 0. (TOP-REAL 2) );
A10: { p where p is Point of (TOP-REAL 2) : S1[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
 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 set ; :: 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 consider p being Point of (TOP-REAL 2) such that
A12: ( p = x & (p `1 ) / |.p.| >= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) ;
thus x in K1 by A1, A12; :: 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 A9, PRE_TOPC:29;
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 A9, A10;
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) ;
A13: |[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 A3, A5, A6, A8;
A14: { 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 set ; :: 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 consider p being Point of (TOP-REAL 2) such that
A15: ( p = x & (p `1 ) / |.p.| <= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) ;
thus x in K1 by A1, A15; :: thesis: verum
end;
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 A13, PRE_TOPC:29;
A16: |[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 A3, A5, A6, A8;
defpred S3[ Point of (TOP-REAL 2)] means ( ($1 `1 ) / |.$1.| <= cn & $1 `2 <= 0 & $1 <> 0. (TOP-REAL 2) );
{ p where p is Point of (TOP-REAL 2) : S3[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
 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 A16;
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) ;
the carrier of ((TOP-REAL 2) | B0) = the carrier of ((TOP-REAL 2) | D) ;
then A17: dom f = the carrier of ((TOP-REAL 2) | K1) by FUNCT_2:def 1
.= K1 by PRE_TOPC:29 ;
then A18: dom (f | K00) = K00 by A11, RELAT_1:91
.= the carrier of (((TOP-REAL 2) | K1) | K00) by PRE_TOPC:29 ;
the carrier of ((TOP-REAL 2) | D) = D by PRE_TOPC:29;
then rng (f | K00) c= D ;
then reconsider f1 = f | K00 as Function of (((TOP-REAL 2) | K1) | K00),((TOP-REAL 2) | D) by A18, FUNCT_2:4;
A19: dom f1 = the carrier of (((TOP-REAL 2) | K1) | K00) by FUNCT_2:def 1
.= K00 by PRE_TOPC:29 ;
A20: dom (cn -FanMorphS ) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A21: dom ((cn -FanMorphS ) | K001) = K001 by RELAT_1:91
.= the carrier of ((TOP-REAL 2) | K001) by PRE_TOPC:29 ;
A22: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:29;
rng ((cn -FanMorphS ) | K001) c= K1
proof
let y be set ; :: 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 set such that
A23: ( x in dom ((cn -FanMorphS ) | K001) & y = ((cn -FanMorphS ) | K001) . x ) by FUNCT_1:def 5;
A24: dom ((cn -FanMorphS ) | K001) = (dom (cn -FanMorphS )) /\ K001 by RELAT_1:90
.= the carrier of (TOP-REAL 2) /\ K001 by FUNCT_2:def 1
.= K001 by XBOOLE_1:28 ;
reconsider q = x as Point of (TOP-REAL 2) by A23;
A25: y = (cn -FanMorphS ) . q by A23, FUNCT_1:70;
consider p2 being Point of (TOP-REAL 2) such that
A26: ( p2 = q & (p2 `1 ) / |.p2.| >= cn & p2 `2 <= 0 & p2 <> 0. (TOP-REAL 2) ) by A23, A24;
A27: (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| by A1, A26, Th122;
set q4 = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]|;
|.q.| <> 0 by A26, TOPRNS_1:25;
then A28: |.q.| ^2 > 0 ^2 by SQUARE_1:74;
A29: 1 - cn > 0 by A1, XREAL_1:151;
A30: ( |[(|.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 )))) & |[(|.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:56;
A31: ((q `1 ) / |.q.|) - cn >= 0 by A26, XREAL_1:50;
0 <= (q `2 ) ^2 by XREAL_1:65;
then 0 + ((q `1 ) ^2 ) <= ((q `1 ) ^2 ) + ((q `2 ) ^2 ) by XREAL_1:9;
then (q `1 ) ^2 <= |.q.| ^2 by JGRAPH_3:10;
then ((q `1 ) ^2 ) / (|.q.| ^2 ) <= (|.q.| ^2 ) / (|.q.| ^2 ) by XREAL_1:74;
then ((q `1 ) ^2 ) / (|.q.| ^2 ) <= 1 by A28, XCMPLX_1:60;
then ((q `1 ) / |.q.|) ^2 <= 1 by XCMPLX_1:77;
then 1 >= (q `1 ) / |.q.| by SQUARE_1:121;
then A32: 1 - cn >= ((q `1 ) / |.q.|) - cn by XREAL_1:11;
A33: - (1 - cn) <= - 0 by A29;
- (1 - cn) <= - (((q `1 ) / |.q.|) - cn) by A32, XREAL_1:26;
then (- (1 - cn)) / (1 - cn) <= (- (((q `1 ) / |.q.|) - cn)) / (1 - cn) by A29, XREAL_1:74;
then A34: - 1 <= (- (((q `1 ) / |.q.|) - cn)) / (1 - cn) by A29, XCMPLX_1:198;
- (- (1 - cn)) >= - (((q `1 ) / |.q.|) - cn) by A31, A33, XREAL_1:26;
then (- (((q `1 ) / |.q.|) - cn)) / (1 - cn) <= 1 by A29, XREAL_1:187;
then ((- (((q `1 ) / |.q.|) - cn)) / (1 - cn)) ^2 <= 1 ^2 by A34, SQUARE_1:119;
then A35: 1 - (((- (((q `1 ) / |.q.|) - cn)) / (1 - cn)) ^2 ) >= 0 by XREAL_1:50;
then A36: 1 - ((- ((((q `1 ) / |.q.|) - cn) / (1 - cn))) ^2 ) >= 0 by XCMPLX_1:188;
sqrt (1 - (((- (((q `1 ) / |.q.|) - cn)) / (1 - cn)) ^2 )) >= 0 by A35, SQUARE_1:def 4;
then sqrt (1 - (((- (((q `1 ) / |.q.|) - cn)) ^2 ) / ((1 - cn) ^2 ))) >= 0 by XCMPLX_1:77;
then sqrt (1 - (((((q `1 ) / |.q.|) - cn) ^2 ) / ((1 - cn) ^2 ))) >= 0 ;
then sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )) >= 0 by XCMPLX_1:77;
then A37: - (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 ))) <= 0 ;
A38: (|[(|.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 ) by A30
.= (|.q.| ^2 ) * (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )) by A36, SQUARE_1:def 4 ;
|.|[(|.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:10
.= |.q.| ^2 by A30, A38 ;
then ( |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| `2 <= 0 ^2 & |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))))]| <> 0. (TOP-REAL 2) ) by A28, A30, A37, TOPRNS_1:24;
hence y in K1 by A1, A25, A27; :: thesis: verum
end;
then reconsider f3 = (cn -FanMorphS ) | K001 as Function of ((TOP-REAL 2) | K001),((TOP-REAL 2) | K1) by A21, A22, FUNCT_2:4;
A39: dom (f | K11) = K11 by A14, A17, RELAT_1:91
.= the carrier of (((TOP-REAL 2) | K1) | K11) by PRE_TOPC:29 ;
the carrier of ((TOP-REAL 2) | D) = D by PRE_TOPC:29;
then rng (f | K11) c= D ;
then reconsider f2 = f | K11 as Function of (((TOP-REAL 2) | K1) | K11),((TOP-REAL 2) | D) by A39, FUNCT_2:4;
A40: dom f2 = the carrier of (((TOP-REAL 2) | K1) | K11) by FUNCT_2:def 1
.= K11 by PRE_TOPC:29 ;
A41: dom ((cn -FanMorphS ) | K111) = K111 by A20, RELAT_1:91
.= the carrier of ((TOP-REAL 2) | K111) by PRE_TOPC:29 ;
A42: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:29;
rng ((cn -FanMorphS ) | K111) c= K1
proof
let y be set ; :: 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 set such that
A43: ( x in dom ((cn -FanMorphS ) | K111) & y = ((cn -FanMorphS ) | K111) . x ) by FUNCT_1:def 5;
A44: dom ((cn -FanMorphS ) | K111) = (dom (cn -FanMorphS )) /\ K111 by RELAT_1:90
.= the carrier of (TOP-REAL 2) /\ K111 by FUNCT_2:def 1
.= K111 by XBOOLE_1:28 ;
reconsider q = x as Point of (TOP-REAL 2) by A43;
A45: y = (cn -FanMorphS ) . q by A43, FUNCT_1:70;
consider p2 being Point of (TOP-REAL 2) such that
A46: ( p2 = q & (p2 `1 ) / |.p2.| <= cn & p2 `2 <= 0 & p2 <> 0. (TOP-REAL 2) ) by A43, A44;
A47: (cn -FanMorphS ) . q = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| by A1, A46, Th122;
set q4 = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]|;
|.q.| <> 0 by A46, TOPRNS_1:25;
then A48: |.q.| ^2 > 0 ^2 by SQUARE_1:74;
A49: 1 + cn > 0 by A1, XREAL_1:150;
A50: ( |[(|.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 )))) & |[(|.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:56;
A51: ((q `1 ) / |.q.|) - cn <= 0 by A46, XREAL_1:49;
A52: |.q.| ^2 = ((q `1 ) ^2 ) + ((q `2 ) ^2 ) by JGRAPH_3:10;
0 <= (q `2 ) ^2 by XREAL_1:65;
then 0 + ((q `1 ) ^2 ) <= ((q `1 ) ^2 ) + ((q `2 ) ^2 ) by XREAL_1:9;
then ((q `1 ) ^2 ) / (|.q.| ^2 ) <= (|.q.| ^2 ) / (|.q.| ^2 ) by A52, XREAL_1:74;
then ((q `1 ) ^2 ) / (|.q.| ^2 ) <= 1 by A48, XCMPLX_1:60;
then ((q `1 ) / |.q.|) ^2 <= 1 by XCMPLX_1:77;
then - 1 <= (q `1 ) / |.q.| by SQUARE_1:121;
then A53: (- 1) - cn <= ((q `1 ) / |.q.|) - cn by XREAL_1:11;
(1 + cn) / (1 + cn) >= (((q `1 ) / |.q.|) - cn) / (1 + cn) by A49, A51, XREAL_1:74;
then A54: 1 >= (((q `1 ) / |.q.|) - cn) / (1 + cn) by A49, XCMPLX_1:60;
(- (1 + cn)) / (1 + cn) <= (((q `1 ) / |.q.|) - cn) / (1 + cn) by A49, A53, XREAL_1:74;
then - 1 <= (((q `1 ) / |.q.|) - cn) / (1 + cn) by A49, XCMPLX_1:198;
then A55: ((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 <= 1 ^2 by A54, SQUARE_1:119;
then A56: 1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 ) >= 0 by XREAL_1:50;
1 - ((- ((((q `1 ) / |.q.|) - cn) / (1 + cn))) ^2 ) >= 0 by A55, XREAL_1:50;
then 1 - (((- (((q `1 ) / |.q.|) - cn)) / (1 + cn)) ^2 ) >= 0 by XCMPLX_1:188;
then sqrt (1 - (((- (((q `1 ) / |.q.|) - cn)) / (1 + cn)) ^2 )) >= 0 by SQUARE_1:def 4;
then sqrt (1 - (((- (((q `1 ) / |.q.|) - cn)) ^2 ) / ((1 + cn) ^2 ))) >= 0 by XCMPLX_1:77;
then sqrt (1 - (((((q `1 ) / |.q.|) - cn) ^2 ) / ((1 + cn) ^2 ))) >= 0 ;
then sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )) >= 0 by XCMPLX_1:77;
then - (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 ))) <= 0 ;
then A57: |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| `2 <= 0 by A50;
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 ) by A50
.= (|.q.| ^2 ) * (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )) by A56, SQUARE_1:def 4 ;
|.|[(|.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:10
.= |.q.| ^2 by A50, A58 ;
then |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )))))]| <> 0. (TOP-REAL 2) by A48, TOPRNS_1:24;
hence y in K1 by A1, A45, A47, A57; :: thesis: verum
end;
then reconsider f4 = (cn -FanMorphS ) | K111 as Function of ((TOP-REAL 2) | K111),((TOP-REAL 2) | K1) by A41, A42, FUNCT_2:4;
set T1 = ((TOP-REAL 2) | K1) | K00;
set T2 = ((TOP-REAL 2) | K1) | K11;
A59: [#] (((TOP-REAL 2) | K1) | K00) = K00 by PRE_TOPC:def 10;
A60: [#] (((TOP-REAL 2) | K1) | K11) = K11 by PRE_TOPC:def 10;
A61: [#] ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:def 10;
A62: K1 c= K00 \/ K11
proof
let x be set ; :: 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
A63: ( p = x & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) by A1;
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 A63;
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 A63;
hence x in K00 \/ K11 by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
then A64: ([#] (((TOP-REAL 2) | K1) | K00)) \/ ([#] (((TOP-REAL 2) | K1) | K11)) = [#] ((TOP-REAL 2) | K1) by A59, A60, A61, XBOOLE_0:def 10;
A65: K003 is closed by Th129;
A66: K003 /\ K1 c= K00
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in K003 /\ K1 or x in K00 )
assume x in K003 /\ K1 ; :: thesis: x in K00
then A67: ( x in K003 & x in K1 ) by XBOOLE_0:def 4;
then consider q1 being Point of (TOP-REAL 2) such that
A68: ( q1 = x & q1 `1 >= cn * |.q1.| & q1 `2 <= 0 ) ;
consider q2 being Point of (TOP-REAL 2) such that
A69: ( q2 = x & q2 `2 <= 0 & q2 <> 0. (TOP-REAL 2) ) by A1, A67;
(q1 `1 ) / |.q1.| >= (cn * |.q1.|) / |.q1.| by A68, XREAL_1:74;
then (q1 `1 ) / |.q1.| >= cn by A68, A69, TOPRNS_1:25, XCMPLX_1:90;
hence x in K00 by A68, A69; :: thesis: verum
end;
K00 c= K003 /\ K1
proof
let x be set ; :: 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
A71: ( p = x & (p `1 ) / |.p.| >= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) ;
((p `1 ) / |.p.|) * |.p.| >= cn * |.p.| by A71, XREAL_1:66;
then p `1 >= cn * |.p.| by A71, TOPRNS_1:25, XCMPLX_1:88;
then A72: x in K003 by A71;
x in K1 by A1, A71;
hence x in K003 /\ K1 by A72, XBOOLE_0:def 4; :: thesis: verum
end;
then K00 = K003 /\ ([#] ((TOP-REAL 2) | K1)) by A61, A66, XBOOLE_0:def 10;
then A73: K00 is closed by A65, PRE_TOPC:43;
A74: K004 is closed by Th130;
A75: K004 /\ K1 c= K11
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in K004 /\ K1 or x in K11 )
assume x in K004 /\ K1 ; :: thesis: x in K11
then A76: ( x in K004 & x in K1 ) by XBOOLE_0:def 4;
then consider q1 being Point of (TOP-REAL 2) such that
A77: ( q1 = x & q1 `1 <= cn * |.q1.| & q1 `2 <= 0 ) ;
consider q2 being Point of (TOP-REAL 2) such that
A78: ( q2 = x & q2 `2 <= 0 & q2 <> 0. (TOP-REAL 2) ) by A1, A76;
(q1 `1 ) / |.q1.| <= (cn * |.q1.|) / |.q1.| by A77, XREAL_1:74;
then (q1 `1 ) / |.q1.| <= cn by A77, A78, TOPRNS_1:25, XCMPLX_1:90;
hence x in K11 by A77, A78; :: thesis: verum
end;
K11 c= K004 /\ K1
proof
let x be set ; :: 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
A80: ( p = x & (p `1 ) / |.p.| <= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) ;
((p `1 ) / |.p.|) * |.p.| <= cn * |.p.| by A80, XREAL_1:66;
then p `1 <= cn * |.p.| by A80, TOPRNS_1:25, XCMPLX_1:88;
then A81: x in K004 by A80;
x in K1 by A1, A80;
hence x in K004 /\ K1 by A81, XBOOLE_0:def 4; :: thesis: verum
end;
then K11 = K004 /\ ([#] ((TOP-REAL 2) | K1)) by A61, A75, XBOOLE_0:def 10;
then A82: K11 is closed by A74, PRE_TOPC:43;
A83: ((TOP-REAL 2) | K1) | K00 = (TOP-REAL 2) | K001 by GOBOARD9:4;
K1 c= D
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in K1 or x in D )
assume x in K1 ; :: thesis: x in D
then consider p6 being Point of (TOP-REAL 2) such that
A84: ( p6 = x & p6 `2 <= 0 & p6 <> 0. (TOP-REAL 2) ) by A1;
( x in the carrier of (TOP-REAL 2) & not x in {(0. (TOP-REAL 2))} ) by A84, TARSKI:def 1;
hence x in D by A1, XBOOLE_0:def 5; :: thesis: verum
end;
then D = K1 \/ D by XBOOLE_1:12;
then A85: (TOP-REAL 2) | K1 is SubSpace of (TOP-REAL 2) | D by TOPMETR:5;
the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:29;
then f1 = f3 by A1, FUNCT_1:82;
then A86: f1 is continuous by A1, A83, A85, Th127, PRE_TOPC:56;
A87: ((TOP-REAL 2) | K1) | K11 = (TOP-REAL 2) | K111 by GOBOARD9:4;
the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:29;
then f2 = f4 by A1, FUNCT_1:82;
then A88: f2 is continuous by A1, A85, A87, Th128, PRE_TOPC:56;
A89: D <> {} ;
for p being set st p in ([#] (((TOP-REAL 2) | K1) | K00)) /\ ([#] (((TOP-REAL 2) | K1) | K11)) holds
f1 . p = f2 . p
proof
let p be set ; :: thesis: ( p in ([#] (((TOP-REAL 2) | K1) | K00)) /\ ([#] (((TOP-REAL 2) | K1) | K11)) implies f1 . p = f2 . p )
assume A91: p in ([#] (((TOP-REAL 2) | K1) | K00)) /\ ([#] (((TOP-REAL 2) | K1) | K11)) ; :: thesis: f1 . p = f2 . p
then ( p in K00 & p in K11 ) by A59, A60, XBOOLE_0:def 4;
hence f1 . p = f . p by FUNCT_1:72
.= f2 . p by A60, A91, FUNCT_1:72 ;
:: thesis: verum
end;
then consider h being Function of ((TOP-REAL 2) | K1),((TOP-REAL 2) | D) such that
A92: ( h = f1 +* f2 & h is continuous ) by A59, A60, A64, A73, A82, A86, A88, JGRAPH_2:9;
A93: dom h = the carrier of ((TOP-REAL 2) | K1) by FUNCT_2:def 1;
A94: the carrier of ((TOP-REAL 2) | K1) = K0 by PRE_TOPC:29;
A95: K0 = the carrier of ((TOP-REAL 2) | K0) by PRE_TOPC:29
.= dom f by A89, FUNCT_2:def 1 ;
for y being set st y in dom h holds
h . y = f . y
proof
let y be set ; :: thesis: ( y in dom h implies h . y = f . y )
assume A96: y in dom h ; :: thesis: h . y = f . y
per cases ( ( y in K00 & not y in K11 ) or y in K11 ) by A62, A93, A94, A96, XBOOLE_0:def 3;
suppose A97: ( y in K00 & not y in K11 ) ; :: thesis: h . y = f . y
then y in (dom f1) \/ (dom f2) by A19, XBOOLE_0:def 3;
hence h . y = f1 . y by A40, A92, A97, FUNCT_4:def 1
.= f . y by A97, FUNCT_1:72 ;
:: thesis: verum
end;
suppose A98: y in K11 ; :: thesis: h . y = f . y
then y in (dom f1) \/ (dom f2) by A40, XBOOLE_0:def 3;
hence h . y = f2 . y by A40, A92, A98, FUNCT_4:def 1
.= f . y by A98, FUNCT_1:72 ;
:: thesis: verum
end;
end;
end;
hence f is continuous by A92, A93, A94, A95, FUNCT_1:9; :: thesis: verum