let sn 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 < 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); 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); ( - 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:52;
defpred S1[ 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:52;
then A2:
|.|[(sqrt (1 - (sn ^2))),sn]|.| = sqrt (((sqrt (1 - (sn ^2))) ^2) + (sn ^2))
by A1, JGRAPH_3:1;
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) ) } )
; f is continuous
then
sn ^2 < 1 ^2
by SQUARE_1:50;
then A4:
1 - (sn ^2) > 0
by XREAL_1:50;
then A5:
|[(sqrt (1 - (sn ^2))),sn]| `1 > 0
by A1, SQUARE_1:25;
then
|[(sqrt (1 - (sn ^2))),sn]| in K0
by A3, JGRAPH_2:3;
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 2;
then A6:
(|[(sqrt (1 - (sn ^2))),sn]| `2) / |.|[(sqrt (1 - (sn ^2))),sn]|.| = sn
by A2, EUCLID:52, SQUARE_1:18;
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:3;
{ 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 `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:8;
defpred S2[ Point of (TOP-REAL 2)] means ( $1 `2 >= sn * |.$1.| & $1 `1 >= 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 `2 >= sn * |.p.| & p `1 >= 0 ) } as Subset of (TOP-REAL 2) ;
defpred S3[ 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) : S3[p] } is Subset of (TOP-REAL 2)
from DOMAIN_1:sch 7();
A10:
- (- (sqrt (1 - (sn ^2)))) > 0
by A4, SQUARE_1:25;
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:3;
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 5;
A12:
rng ((sn -FanMorphE) | K001) c= K1
proof
let y be
object ;
TARSKI:def 3 ( not y in rng ((sn -FanMorphE) | K001) or y in K1 )
assume
y in rng ((sn -FanMorphE) | K001)
;
y in K1
then consider x being
object such that A13:
x in dom ((sn -FanMorphE) | K001)
and A14:
y = ((sn -FanMorphE) | K001) . x
by FUNCT_1:def 3;
x in dom (sn -FanMorphE)
by A13, RELAT_1:57;
then reconsider q =
x as
Point of
(TOP-REAL 2) ;
A15:
y = (sn -FanMorphE) . q
by A13, A14, FUNCT_1:47;
dom ((sn -FanMorphE) | K001) =
(dom (sn -FanMorphE)) /\ K001
by RELAT_1:61
.=
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:48;
|.q.| <> 0
by A16, TOPRNS_1:24;
then A18:
|.q.| ^2 > 0 ^2
by SQUARE_1:12;
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:52;
A20:
1
- sn > 0
by A3, XREAL_1:149;
0 <= (q `1) ^2
by XREAL_1:63;
then
0 + ((q `2) ^2) <= ((q `1) ^2) + ((q `2) ^2)
by XREAL_1:7;
then
(q `2) ^2 <= |.q.| ^2
by JGRAPH_3:1;
then
((q `2) ^2) / (|.q.| ^2) <= (|.q.| ^2) / (|.q.| ^2)
by XREAL_1:72;
then
((q `2) ^2) / (|.q.| ^2) <= 1
by A18, XCMPLX_1:60;
then
((q `2) / |.q.|) ^2 <= 1
by XCMPLX_1:76;
then
1
>= (q `2) / |.q.|
by SQUARE_1:51;
then
1
- sn >= ((q `2) / |.q.|) - sn
by XREAL_1:9;
then
- (1 - sn) <= - (((q `2) / |.q.|) - sn)
by XREAL_1:24;
then
(- (1 - sn)) / (1 - sn) <= (- (((q `2) / |.q.|) - sn)) / (1 - sn)
by A20, XREAL_1:72;
then
- 1
<= (- (((q `2) / |.q.|) - sn)) / (1 - sn)
by A20, XCMPLX_1:197;
then
((- (((q `2) / |.q.|) - sn)) / (1 - sn)) ^2 <= 1
^2
by A20, A17, SQUARE_1:49;
then A21:
1
- (((- (((q `2) / |.q.|) - sn)) / (1 - sn)) ^2) >= 0
by XREAL_1:48;
then A22:
1
- ((- ((((q `2) / |.q.|) - sn) / (1 - sn))) ^2) >= 0
by XCMPLX_1:187;
sqrt (1 - (((- (((q `2) / |.q.|) - sn)) / (1 - sn)) ^2)) >= 0
by A21, SQUARE_1:def 2;
then
sqrt (1 - (((- (((q `2) / |.q.|) - sn)) ^2) / ((1 - sn) ^2))) >= 0
by XCMPLX_1:76;
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:76;
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:52;
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 2
;
|.|[(|.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:1
.=
|.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:23;
(sn -FanMorphE) . q = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 - sn)))]|
by A3, A16, Th84;
hence
y in K1
by A3, A15, A24, A23, A26;
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
|[(sqrt (1 - (sn ^2))),sn]| <> 0. (TOP-REAL 2)
by A1, A4, JGRAPH_2:3, SQUARE_1:25;
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
then
D = K1 \/ D
by XBOOLE_1:12;
then A29:
(TOP-REAL 2) | K1 is SubSpace of (TOP-REAL 2) | D
by TOPMETR:4;
A30:
{ p where p is Point of (TOP-REAL 2) : ( (p `2) / |.p.| >= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } c= K1
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:8;
A31:
K003 is closed
by Th91;
A32:
rng ((sn -FanMorphE) | K111) c= K1
proof
let y be
object ;
TARSKI:def 3 ( not y in rng ((sn -FanMorphE) | K111) or y in K1 )
assume
y in rng ((sn -FanMorphE) | K111)
;
y in K1
then consider x being
object such that A33:
x in dom ((sn -FanMorphE) | K111)
and A34:
y = ((sn -FanMorphE) | K111) . x
by FUNCT_1:def 3;
x in dom (sn -FanMorphE)
by A33, RELAT_1:57;
then reconsider q =
x as
Point of
(TOP-REAL 2) ;
A35:
y = (sn -FanMorphE) . q
by A33, A34, FUNCT_1:47;
dom ((sn -FanMorphE) | K111) =
(dom (sn -FanMorphE)) /\ K111
by RELAT_1:61
.=
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:47;
|.q.| <> 0
by A36, TOPRNS_1:24;
then A38:
|.q.| ^2 > 0 ^2
by SQUARE_1:12;
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:52;
A40:
1
+ sn > 0
by A3, XREAL_1:148;
0 <= (q `1) ^2
by XREAL_1:63;
then
(
|.q.| ^2 = ((q `1) ^2) + ((q `2) ^2) &
0 + ((q `2) ^2) <= ((q `1) ^2) + ((q `2) ^2) )
by JGRAPH_3:1, XREAL_1:7;
then
((q `2) ^2) / (|.q.| ^2) <= (|.q.| ^2) / (|.q.| ^2)
by XREAL_1:72;
then
((q `2) ^2) / (|.q.| ^2) <= 1
by A38, XCMPLX_1:60;
then
((q `2) / |.q.|) ^2 <= 1
by XCMPLX_1:76;
then
- 1
<= (q `2) / |.q.|
by SQUARE_1:51;
then
(- 1) - sn <= ((q `2) / |.q.|) - sn
by XREAL_1:9;
then
(- (1 + sn)) / (1 + sn) <= (((q `2) / |.q.|) - sn) / (1 + sn)
by A40, XREAL_1:72;
then
- 1
<= (((q `2) / |.q.|) - sn) / (1 + sn)
by A40, XCMPLX_1:197;
then A41:
((((q `2) / |.q.|) - sn) / (1 + sn)) ^2 <= 1
^2
by A40, A37, SQUARE_1:49;
then A42:
1
- (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2) >= 0
by XREAL_1:48;
1
- ((- ((((q `2) / |.q.|) - sn) / (1 + sn))) ^2) >= 0
by A41, XREAL_1:48;
then
1
- (((- (((q `2) / |.q.|) - sn)) / (1 + sn)) ^2) >= 0
by XCMPLX_1:187;
then
sqrt (1 - (((- (((q `2) / |.q.|) - sn)) / (1 + sn)) ^2)) >= 0
by SQUARE_1:def 2;
then
sqrt (1 - (((- (((q `2) / |.q.|) - sn)) ^2) / ((1 + sn) ^2))) >= 0
by XCMPLX_1:76;
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:76;
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:52;
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 2
;
|.|[(|.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:1
.=
|.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:23;
(sn -FanMorphE) . q = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn)))]|
by A3, A36, Th84;
hence
y in K1
by A3, A35, A44, A43, A46;
verum
end;
the carrier of ((TOP-REAL 2) | D) = D
by PRE_TOPC:8;
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:8
;
then dom (f | K00) =
K00
by A30, 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 A47, FUNCT_2:2;
A49:
the carrier of ((TOP-REAL 2) | K1) = K0
by PRE_TOPC:8;
|[(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:3;
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:8;
A50:
the carrier of ((TOP-REAL 2) | K1) = K1
by PRE_TOPC:8;
A51:
dom (sn -FanMorphE) = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
then dom ((sn -FanMorphE) | K001) =
K001
by RELAT_1:62
.=
the carrier of ((TOP-REAL 2) | K001)
by PRE_TOPC:8
;
then reconsider f3 = (sn -FanMorphE) | K001 as Function of ((TOP-REAL 2) | K001),((TOP-REAL 2) | K1) by A8, A12, FUNCT_2:2;
A52:
D <> {}
;
dom ((sn -FanMorphE) | K111) =
K111
by A51, RELAT_1:62
.=
the carrier of ((TOP-REAL 2) | K111)
by PRE_TOPC:8
;
then reconsider f4 = (sn -FanMorphE) | K111 as Function of ((TOP-REAL 2) | K111),((TOP-REAL 2) | K1) by A50, A32, FUNCT_2:2;
the carrier of ((TOP-REAL 2) | D) = D
by PRE_TOPC:8;
then A53:
rng (f | K11) c= D
;
dom (f | K11) =
K11
by A27, A48, 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 A53, 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 A54:
f2 is continuous
by A3, A29, Th90, PRE_TOPC:26;
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 A55:
f1 is continuous
by A3, A29, Th89, PRE_TOPC:26;
A56: dom f2 =
the carrier of (((TOP-REAL 2) | K1) | K11)
by FUNCT_2:def 1
.=
K11
by PRE_TOPC:8
;
defpred S4[ Point of (TOP-REAL 2)] means ( $1 `2 <= sn * |.$1.| & $1 `1 >= 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 `2 <= sn * |.p.| & p `1 >= 0 ) } as Subset of (TOP-REAL 2) ;
A57:
K004 /\ K1 c= K11
A62:
K004 is closed
by Th92;
K11 c= K004 /\ K1
then
K11 = K004 /\ ([#] ((TOP-REAL 2) | K1))
by A11, A57, XBOOLE_0:def 10;
then A68:
K11 is closed
by A62, PRE_TOPC:13;
A69:
K003 /\ K1 c= K00
K00 c= K003 /\ K1
then
K00 = K003 /\ ([#] ((TOP-REAL 2) | K1))
by A11, A69, XBOOLE_0:def 10;
then A79:
K00 is closed
by A31, PRE_TOPC:13;
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 5;
A81:
[#] (((TOP-REAL 2) | K1) | K00) = K00
by PRE_TOPC:def 5;
A82:
for p being object st p in ([#] (((TOP-REAL 2) | K1) | K00)) /\ ([#] (((TOP-REAL 2) | K1) | K11)) holds
f1 . p = f2 . p
A84:
K1 c= K00 \/ K11
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: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 A52, FUNCT_2:def 1
;
hence
f is continuous
by A87, A88, A90, FUNCT_1:2, PRE_TOPC:8; verum