let cn be Real; 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); 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); ( - 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) ) } )
; 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;
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, SQUARE_1:18;
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
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
A12:
{ p where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| >= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } c= K1
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 ;
TARSKI:def 3 ( not y in rng ((cn -FanMorphS) | K001) or y in K1 )
assume
y in rng ((cn -FanMorphS) | K001)
;
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;
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
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 ;
TARSKI:def 3 ( not y in rng ((cn -FanMorphS) | K111) or y in K1 )
assume
y in rng ((cn -FanMorphS) | K111)
;
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;
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
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
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
K00 c= K003 /\ K1
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
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
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; verum