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 -FanMorphE ) | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( 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 -FanMorphE ) | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( 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 -FanMorphE ) | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( 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;
defpred S₁[ Point of (TOP-REAL 2)] means ( ($1 `2 ) / |.$1.| >= sn & $1 `1 >= 0 & $1 <> 0. (TOP-REAL 2) );
|[(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;
assume A3: ( - 1 < sn & sn < 1 & f = (sn -FanMorphE ) | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( 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 ))),sn]| `1 > 0 by A1, SQUARE_1:93;
then |[(sqrt (1 - (sn ^2 ))),sn]| in K0 by A3, JGRAPH_2:11;
then reconsider K1 = K0 as non empty Subset of (TOP-REAL 2) ;
(sqrt (1 - (sn ^2 ))) ^2 = 1 - (sn ^2 ) by A4, SQUARE_1:def 4;
then A6: (|[(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 { p where p is Point of (TOP-REAL 2) : ( (p `2 ) / |.p.| >= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } by A5, JGRAPH_2:11;
{ p where p is Point of (TOP-REAL 2) : S₁[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 `2 ) / |.p.| >= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } as non empty Subset of (TOP-REAL 2) by A7;
A8: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:29;
defpred S₂[ Point of (TOP-REAL 2)] means ( $1 `2 >= sn * |.$1.| & $1 `1 >= 0 );
{ p where p is Point of (TOP-REAL 2) : S₂[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 `2 >= sn * |.p.| & p `1 >= 0 ) } as Subset of (TOP-REAL 2) ;
defpred S₃[ Point of (TOP-REAL 2)] means ( ($1 `2 ) / |.$1.| <= sn & $1 `1 >= 0 & $1 <> 0. (TOP-REAL 2) );
A9: { p where p is Point of (TOP-REAL 2) : S₃[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
A10: - (- (sqrt (1 - (sn ^2 )))) > 0 by A4, SQUARE_1:93;
then |[(sqrt (1 - (sn ^2 ))),sn]| in { p where p is Point of (TOP-REAL 2) : ( (p `2 ) / |.p.| <= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } by A1, A6, JGRAPH_2:11;
then reconsider K111 = { p where p is Point of (TOP-REAL 2) : ( (p `2 ) / |.p.| <= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } as non empty Subset of (TOP-REAL 2) by A9;
A11: [#] ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:def 10;
A12: rng ((sn -FanMorphE ) | K001) c= K1

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((sn -FanMorphE ) | K001) or y in K1 )
assume y in rng ((sn -FanMorphE ) | K001) ; :: thesis: y in K1
then consider x being set such that
A13: x in dom ((sn -FanMorphE ) | K001) and
A14: y = ((sn -FanMorphE ) | K001) . x by FUNCT_1:def 5;
reconsider q = x as Point of (TOP-REAL 2) by A13;
A15: y = (sn -FanMorphE ) . q by A13, A14, FUNCT_1:70;
dom ((sn -FanMorphE ) | K001) = (dom (sn -FanMorphE )) /\ K001 by RELAT_1:90
.= the carrier of (TOP-REAL 2) /\ K001 by FUNCT_2:def 1
.= K001 by XBOOLE_1:28 ;
then A16: ex p2 being Point of (TOP-REAL 2) st
( p2 = q & (p2 `2 ) / |.p2.| >= sn & p2 `1 >= 0 & p2 <> 0. (TOP-REAL 2) ) by A13;
then A17: ((q `2 ) / |.q.|) - sn >= 0 by XREAL_1:50;
|.q.| <> 0 by A16, TOPRNS_1:25;
then A18: |.q.| ^2 > 0 ^2 by SQUARE_1:74;
set q4 = |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]|;
A19: |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]| `2 = |.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)) by EUCLID:56;
A20: 1 - sn > 0 by A3, XREAL_1:151;
0 <= (q `1 ) ^2 by XREAL_1:65;
then 0 + ((q `2 ) ^2 ) <= ((q `1 ) ^2 ) + ((q `2 ) ^2 ) by XREAL_1:9;
then (q `2 ) ^2 <= |.q.| ^2 by JGRAPH_3:10;
then ((q `2 ) ^2 ) / (|.q.| ^2 ) <= (|.q.| ^2 ) / (|.q.| ^2 ) by XREAL_1:74;
then ((q `2 ) ^2 ) / (|.q.| ^2 ) <= 1 by A18, XCMPLX_1:60;
then ((q `2 ) / |.q.|) ^2 <= 1 by XCMPLX_1:77;
then 1 >= (q `2 ) / |.q.| by SQUARE_1:121;
then 1 - sn >= ((q `2 ) / |.q.|) - sn by XREAL_1:11;
then - (1 - sn) <= - (((q `2 ) / |.q.|) - sn) by XREAL_1:26;
then (- (1 - sn)) / (1 - sn) <= (- (((q `2 ) / |.q.|) - sn)) / (1 - sn) by A20, XREAL_1:74;
then - 1 <= (- (((q `2 ) / |.q.|) - sn)) / (1 - sn) by A20, XCMPLX_1:198;
then ((- (((q `2 ) / |.q.|) - sn)) / (1 - sn)) ^2 <= 1 ^2 by A20, A17, SQUARE_1:119;
then A21: 1 - (((- (((q `2 ) / |.q.|) - sn)) / (1 - sn)) ^2 ) >= 0 by XREAL_1:50;
then A22: 1 - ((- ((((q `2 ) / |.q.|) - sn) / (1 - sn))) ^2 ) >= 0 by XCMPLX_1:188;
sqrt (1 - (((- (((q `2 ) / |.q.|) - sn)) / (1 - sn)) ^2 )) >= 0 by A21, SQUARE_1:def 4;
then sqrt (1 - (((- (((q `2 ) / |.q.|) - sn)) ^2 ) / ((1 - sn) ^2 ))) >= 0 by XCMPLX_1:77;
then sqrt (1 - (((((q `2 ) / |.q.|) - sn) ^2 ) / ((1 - sn) ^2 ))) >= 0 ;
then A23: sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )) >= 0 by XCMPLX_1:77;
A24: |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]| `1 = |.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 ))) by EUCLID:56;
then A25: (|[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]| `1 ) ^2 = (|.q.| ^2 ) * ((sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 ))) ^2 )
.= (|.q.| ^2 ) * (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )) by A22, SQUARE_1:def 4 ;
|.|[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]|.| ^2 = ((|[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]| `1 ) ^2 ) + ((|[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]| `2 ) ^2 ) by JGRAPH_3:10
.= |.q.| ^2 by A19, A25 ;
then A26: |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]| <> 0. (TOP-REAL 2) by A18, TOPRNS_1:24;
(sn -FanMorphE ) . q = |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 - sn)))]| by A3, A16, Th91;
hence y in K1 by A3, A15, A24, A23, A26; :: thesis: verum

end;

A27: { p where p is Point of (TOP-REAL 2) : ( (p `2 ) / |.p.| <= sn & p `1 >= 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 `2 ) / |.p.| <= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } or x in K1 )
assume x in { p where p is Point of (TOP-REAL 2) : ( (p `2 ) / |.p.| <= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } ; :: thesis: x in K1
then ex p being Point of (TOP-REAL 2) st
( p = x & (p `2 ) / |.p.| <= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) ;
hence x in K1 by A3; :: thesis: verum

end;

|[(sqrt (1 - (sn ^2 ))),sn]| <> 0. (TOP-REAL 2) by A1, A4, JGRAPH_2:11, SQUARE_1:93;
then not |[(sqrt (1 - (sn ^2 ))),sn]| in {(0. (TOP-REAL 2))} by 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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in K1 or x in D )
assume A28: x in K1 ; :: thesis: x in D
then ex p6 being Point of (TOP-REAL 2) st
( p6 = x & p6 `1 >= 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, A28, XBOOLE_0:def 5; :: thesis: verum

end;

then D = K1 \/ D by XBOOLE_1:12;
then A29: (TOP-REAL 2) | K1 is SubSpace of (TOP-REAL 2) | D by TOPMETR:5;
A30: { p where p is Point of (TOP-REAL 2) : ( (p `2 ) / |.p.| >= sn & p `1 >= 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 `2 ) / |.p.| >= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } or x in K1 )
assume x in { p where p is Point of (TOP-REAL 2) : ( (p `2 ) / |.p.| >= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } ; :: thesis: x in K1
then ex p being Point of (TOP-REAL 2) st
( p = x & (p `2 ) / |.p.| >= sn & p `1 >= 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 `2 ) / |.p.| >= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | K1) by A7, PRE_TOPC:29;
A31: K003 is closed by Th98;
A32: rng ((sn -FanMorphE ) | K111) c= K1

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((sn -FanMorphE ) | K111) or y in K1 )
assume y in rng ((sn -FanMorphE ) | K111) ; :: thesis: y in K1
then consider x being set such that
A33: x in dom ((sn -FanMorphE ) | K111) and
A34: y = ((sn -FanMorphE ) | K111) . x by FUNCT_1:def 5;
reconsider q = x as Point of (TOP-REAL 2) by A33;
A35: y = (sn -FanMorphE ) . q by A33, A34, FUNCT_1:70;
dom ((sn -FanMorphE ) | K111) = (dom (sn -FanMorphE )) /\ K111 by RELAT_1:90
.= the carrier of (TOP-REAL 2) /\ K111 by FUNCT_2:def 1
.= K111 by XBOOLE_1:28 ;
then A36: ex p2 being Point of (TOP-REAL 2) st
( p2 = q & (p2 `2 ) / |.p2.| <= sn & p2 `1 >= 0 & p2 <> 0. (TOP-REAL 2) ) by A33;
then A37: ((q `2 ) / |.q.|) - sn <= 0 by XREAL_1:49;
|.q.| <> 0 by A36, TOPRNS_1:25;
then A38: |.q.| ^2 > 0 ^2 by SQUARE_1:74;
set q4 = |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]|;
A39: |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| `2 = |.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)) by EUCLID:56;
A40: 1 + sn > 0 by A3, XREAL_1:150;
0 <= (q `1 ) ^2 by XREAL_1:65;
then ( |.q.| ^2 = ((q `1 ) ^2 ) + ((q `2 ) ^2 ) & 0 + ((q `2 ) ^2 ) <= ((q `1 ) ^2 ) + ((q `2 ) ^2 ) ) by JGRAPH_3:10, XREAL_1:9;
then ((q `2 ) ^2 ) / (|.q.| ^2 ) <= (|.q.| ^2 ) / (|.q.| ^2 ) by XREAL_1:74;
then ((q `2 ) ^2 ) / (|.q.| ^2 ) <= 1 by A38, XCMPLX_1:60;
then ((q `2 ) / |.q.|) ^2 <= 1 by XCMPLX_1:77;
then - 1 <= (q `2 ) / |.q.| by SQUARE_1:121;
then (- 1) - sn <= ((q `2 ) / |.q.|) - sn by XREAL_1:11;
then (- (1 + sn)) / (1 + sn) <= (((q `2 ) / |.q.|) - sn) / (1 + sn) by A40, XREAL_1:74;
then - 1 <= (((q `2 ) / |.q.|) - sn) / (1 + sn) by A40, XCMPLX_1:198;
then A41: ((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 <= 1 ^2 by A40, A37, SQUARE_1:119;
then A42: 1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ) >= 0 by XREAL_1:50;
1 - ((- ((((q `2 ) / |.q.|) - sn) / (1 + sn))) ^2 ) >= 0 by A41, XREAL_1:50;
then 1 - (((- (((q `2 ) / |.q.|) - sn)) / (1 + sn)) ^2 ) >= 0 by XCMPLX_1:188;
then sqrt (1 - (((- (((q `2 ) / |.q.|) - sn)) / (1 + sn)) ^2 )) >= 0 by SQUARE_1:def 4;
then sqrt (1 - (((- (((q `2 ) / |.q.|) - sn)) ^2 ) / ((1 + sn) ^2 ))) >= 0 by XCMPLX_1:77;
then sqrt (1 - (((((q `2 ) / |.q.|) - sn) ^2 ) / ((1 + sn) ^2 ))) >= 0 ;
then A43: sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )) >= 0 by XCMPLX_1:77;
A44: |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| `1 = |.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))) by EUCLID:56;
then A45: (|[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| `1 ) ^2 = (|.q.| ^2 ) * ((sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))) ^2 )
.= (|.q.| ^2 ) * (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )) by A42, SQUARE_1:def 4 ;
|.|[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]|.| ^2 = ((|[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| `1 ) ^2 ) + ((|[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| `2 ) ^2 ) by JGRAPH_3:10
.= |.q.| ^2 by A39, A45 ;
then A46: |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| <> 0. (TOP-REAL 2) by A38, TOPRNS_1:24;
(sn -FanMorphE ) . q = |[(|.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]| by A3, A36, Th91;
hence y in K1 by A3, A35, A44, A43, A46; :: thesis: verum

end;

the carrier of ((TOP-REAL 2) | D) = D by PRE_TOPC:29;
then A47: rng (f | K00) c= D ;
the carrier of ((TOP-REAL 2) | B0) = the carrier of ((TOP-REAL 2) | D) ;
then A48: dom f = the carrier of ((TOP-REAL 2) | K1) by FUNCT_2:def 1
.= K1 by PRE_TOPC:29 ;
then dom (f | K00) = K00 by A30, RELAT_1:91
.= the carrier of (((TOP-REAL 2) | K1) | K00) by PRE_TOPC:29 ;
then reconsider f1 = f | K00 as Function of (((TOP-REAL 2) | K1) | K00),((TOP-REAL 2) | D) by A47, FUNCT_2:4;
A49: the carrier of ((TOP-REAL 2) | K1) = K0 by PRE_TOPC:29;
|[(sqrt (1 - (sn ^2 ))),sn]| in { p where p is Point of (TOP-REAL 2) : ( (p `2 ) / |.p.| <= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } by A1, A10, A6, JGRAPH_2:11;
then reconsider K11 = { p where p is Point of (TOP-REAL 2) : ( (p `2 ) / |.p.| <= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | K1) by A27, PRE_TOPC:29;
A50: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:29;
A51: dom (sn -FanMorphE ) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then dom ((sn -FanMorphE ) | K001) = K001 by RELAT_1:91
.= the carrier of ((TOP-REAL 2) | K001) by PRE_TOPC:29 ;
then reconsider f3 = (sn -FanMorphE ) | K001 as Function of ((TOP-REAL 2) | K001),((TOP-REAL 2) | K1) by A8, A12, FUNCT_2:4;
A52: D <> {} ;
dom ((sn -FanMorphE ) | K111) = K111 by A51, RELAT_1:91
.= the carrier of ((TOP-REAL 2) | K111) by PRE_TOPC:29 ;
then reconsider f4 = (sn -FanMorphE ) | K111 as Function of ((TOP-REAL 2) | K111),((TOP-REAL 2) | K1) by A50, A32, FUNCT_2:4;
the carrier of ((TOP-REAL 2) | D) = D by PRE_TOPC:29;
then A53: rng (f | K11) c= D ;
dom (f | K11) = K11 by A27, A48, RELAT_1:91
.= the carrier of (((TOP-REAL 2) | K1) | K11) by PRE_TOPC:29 ;
then reconsider f2 = f | K11 as Function of (((TOP-REAL 2) | K1) | K11),((TOP-REAL 2) | D) by A53, FUNCT_2:4;
the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:29;
then ( ((TOP-REAL 2) | K1) | K11 = (TOP-REAL 2) | K111 & f2 = f4 ) by A3, FUNCT_1:82, GOBOARD9:4;
then A54: f2 is continuous by A3, A29, Th97, PRE_TOPC:56;
the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:29;
then ( ((TOP-REAL 2) | K1) | K00 = (TOP-REAL 2) | K001 & f1 = f3 ) by A3, FUNCT_1:82, GOBOARD9:4;
then A55: f1 is continuous by A3, A29, Th96, PRE_TOPC:56;
A56: dom f2 = the carrier of (((TOP-REAL 2) | K1) | K11) by FUNCT_2:def 1
.= K11 by PRE_TOPC:29 ;
defpred S₄[ Point of (TOP-REAL 2)] means ( $1 `2 <= sn * |.$1.| & $1 `1 >= 0 );
{ p where p is Point of (TOP-REAL 2) : S₄[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 `2 <= sn * |.p.| & p `1 >= 0 ) } as Subset of (TOP-REAL 2) ;
A57: 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 A58: 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
A59: q1 = x and
A60: q1 `2 <= sn * |.q1.| and
q1 `1 >= 0 ;
x in K1 by A58, XBOOLE_0:def 4;
then A61: ex q2 being Point of (TOP-REAL 2) st
( q2 = x & q2 `1 >= 0 & q2 <> 0. (TOP-REAL 2) ) by A3;
(q1 `2 ) / |.q1.| <= (sn * |.q1.|) / |.q1.| by A60, XREAL_1:74;
then (q1 `2 ) / |.q1.| <= sn by A59, A61, TOPRNS_1:25, XCMPLX_1:90;
hence x in K11 by A59, A61; :: thesis: verum

end;

A62: K004 is closed by Th99;
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
A63: p = x and
A64: (p `2 ) / |.p.| <= sn and
A65: p `1 >= 0 and
A66: p <> 0. (TOP-REAL 2) ;
((p `2 ) / |.p.|) * |.p.| <= sn * |.p.| by A64, XREAL_1:66;
then p `2 <= sn * |.p.| by A66, TOPRNS_1:25, XCMPLX_1:88;
then A67: x in K004 by A63, A65;
x in K1 by A3, A63, A65, A66;
hence x in K004 /\ K1 by A67, XBOOLE_0:def 4; :: thesis: verum

end;

then K11 = K004 /\ ([#] ((TOP-REAL 2) | K1)) by A11, A57, XBOOLE_0:def 10;
then A68: K11 is closed by A62, PRE_TOPC:43;
A69: 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 A70: 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
A71: q1 = x and
A72: q1 `2 >= sn * |.q1.| and
q1 `1 >= 0 ;
x in K1 by A70, XBOOLE_0:def 4;
then A73: ex q2 being Point of (TOP-REAL 2) st
( q2 = x & q2 `1 >= 0 & q2 <> 0. (TOP-REAL 2) ) by A3;
(q1 `2 ) / |.q1.| >= (sn * |.q1.|) / |.q1.| by A72, XREAL_1:74;
then (q1 `2 ) / |.q1.| >= sn by A71, A73, TOPRNS_1:25, XCMPLX_1:90;
hence x in K00 by A71, A73; :: 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
A74: p = x and
A75: (p `2 ) / |.p.| >= sn and
A76: p `1 >= 0 and
A77: p <> 0. (TOP-REAL 2) ;
((p `2 ) / |.p.|) * |.p.| >= sn * |.p.| by A75, XREAL_1:66;
then p `2 >= sn * |.p.| by A77, TOPRNS_1:25, XCMPLX_1:88;
then A78: x in K003 by A74, A76;
x in K1 by A3, A74, A76, A77;
hence x in K003 /\ K1 by A78, XBOOLE_0:def 4; :: thesis: verum

end;

then K00 = K003 /\ ([#] ((TOP-REAL 2) | K1)) by A11, A69, XBOOLE_0:def 10;
then A79: K00 is closed by A31, PRE_TOPC:43;
set T1 = ((TOP-REAL 2) | K1) | K00;
set T2 = ((TOP-REAL 2) | K1) | K11;
A80: [#] (((TOP-REAL 2) | K1) | K11) = K11 by PRE_TOPC:def 10;
A81: [#] (((TOP-REAL 2) | K1) | K00) = K00 by PRE_TOPC:def 10;
A82: 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 A83: p in ([#] (((TOP-REAL 2) | K1) | K00)) /\ ([#] (((TOP-REAL 2) | K1) | K11)) ; :: thesis: f1 . p = f2 . p
then p in K00 by A81, XBOOLE_0:def 4;
hence f1 . p = f . p by FUNCT_1:72
.= f2 . p by A80, A83, FUNCT_1:72 ;
:: thesis: verum

end;

A84: 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
A85: ( p = x & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) by A3;

per cases ( (p `2 ) / |.p.| >= sn or (p `2 ) / |.p.| < sn ) ;

suppose (p `2 ) / |.p.| >= sn ; :: 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 `2 ) / |.p.| < sn ; :: 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 A81, A80, A11, 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 A81, A80, A79, A68, A55, A54, A82, JGRAPH_2:9;
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:29 ;
A90: 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 A91: y in dom h ; :: thesis: h . y = f . y

now

per cases ( ( y in K00 & not y in K11 ) or y in K11 ) by A84, A88, A49, 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 A56, A86, A92, FUNCT_4:def 1
.= f . y by A92, FUNCT_1:72 ;
:: thesis: verum

end;

suppose A93: y in K11 ; :: thesis: h . y = f . y

then y in (dom f1) \/ (dom f2) by A56, XBOOLE_0:def 3;
hence h . y = f2 . y by A56, A86, A93, FUNCT_4:def 1
.= f . y by A93, FUNCT_1:72 ;
:: thesis: verum

end;

end;

end;

hence h . y = f . y ; :: thesis: verum

end;

K0 = the carrier of ((TOP-REAL 2) | K0) by PRE_TOPC:29
.= dom f by A52, FUNCT_2:def 1 ;
hence f is continuous by A87, A88, A90, FUNCT_1:9, PRE_TOPC:29; :: thesis: verum