( |[0,1]| `1 = 0 & |[0,1]| `2 = 1 )
by EUCLID:52;
then A1:
|[0,1]| in { p where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) }
by JGRAPH_2:3;
set Y1 = |[0,1]|;
defpred S1[ Point of (TOP-REAL 2)] means $1 `1 >= 0 ;
reconsider B0 = {(0. (TOP-REAL 2))} as Subset of (TOP-REAL 2) ;
let sn be Real; for D being non empty Subset of (TOP-REAL 2) st - 1 < sn & sn < 1 & D ` = {(0. (TOP-REAL 2))} holds
ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (sn -FanMorphE) | D & h is continuous )
let D be non empty Subset of (TOP-REAL 2); ( - 1 < sn & sn < 1 & D ` = {(0. (TOP-REAL 2))} implies ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (sn -FanMorphE) | D & h is continuous ) )
assume that
A2:
( - 1 < sn & sn < 1 )
and
A3:
D ` = {(0. (TOP-REAL 2))}
; ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (sn -FanMorphE) | D & h is continuous )
A4:
the carrier of ((TOP-REAL 2) | D) = D
by PRE_TOPC:8;
A5: D =
B0 `
by A3
.=
NonZero (TOP-REAL 2)
by SUBSET_1:def 4
;
{ p where p is Point of (TOP-REAL 2) : ( S1[p] & p <> 0. (TOP-REAL 2) ) } c= the carrier of ((TOP-REAL 2) | D)
from JGRAPH_4:sch 1(A5);
then reconsider K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | D) by A1;
A6:
K0 = the carrier of (((TOP-REAL 2) | D) | K0)
by PRE_TOPC:8;
A7:
the carrier of ((TOP-REAL 2) | D) = D
by PRE_TOPC:8;
A8:
rng ((sn -FanMorphE) | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)
A12:
K0 c= the carrier of (TOP-REAL 2)
( |[0,1]| `1 = 0 & |[0,1]| `2 = 1 )
by EUCLID:52;
then A13:
|[0,1]| in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) }
by JGRAPH_2:3;
A14:
the carrier of ((TOP-REAL 2) | D) = NonZero (TOP-REAL 2)
by A5, PRE_TOPC:8;
defpred S2[ Point of (TOP-REAL 2)] means $1 `1 <= 0 ;
{ p where p is Point of (TOP-REAL 2) : ( S2[p] & p <> 0. (TOP-REAL 2) ) } c= the carrier of ((TOP-REAL 2) | D)
from JGRAPH_4:sch 1(A5);
then reconsider K1 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | D) by A13;
A15:
( K0 is closed & K1 is closed )
by A5, Th29, Th31;
dom ((sn -FanMorphE) | K0) =
(dom (sn -FanMorphE)) /\ K0
by RELAT_1:61
.=
the carrier of (TOP-REAL 2) /\ K0
by FUNCT_2:def 1
.=
K0
by A12, XBOOLE_1:28
;
then reconsider f = (sn -FanMorphE) | K0 as Function of (((TOP-REAL 2) | D) | K0),((TOP-REAL 2) | D) by A6, A8, FUNCT_2:2, XBOOLE_1:1;
A16:
K1 = the carrier of (((TOP-REAL 2) | D) | K1)
by PRE_TOPC:8;
A17:
rng ((sn -FanMorphE) | K1) c= the carrier of (((TOP-REAL 2) | D) | K1)
A21:
K1 c= the carrier of (TOP-REAL 2)
dom ((sn -FanMorphE) | K1) =
(dom (sn -FanMorphE)) /\ K1
by RELAT_1:61
.=
the carrier of (TOP-REAL 2) /\ K1
by FUNCT_2:def 1
.=
K1
by A21, XBOOLE_1:28
;
then reconsider g = (sn -FanMorphE) | K1 as Function of (((TOP-REAL 2) | D) | K1),((TOP-REAL 2) | D) by A16, A17, FUNCT_2:2, XBOOLE_1:1;
A22:
K1 = [#] (((TOP-REAL 2) | D) | K1)
by PRE_TOPC:def 5;
A23:
D c= K0 \/ K1
A25:
dom f = K0
by A6, FUNCT_2:def 1;
A26:
K0 = [#] (((TOP-REAL 2) | D) | K0)
by PRE_TOPC:def 5;
A27:
for x being object st x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) holds
f . x = g . x
D = [#] ((TOP-REAL 2) | D)
by PRE_TOPC:def 5;
then A29:
([#] (((TOP-REAL 2) | D) | K0)) \/ ([#] (((TOP-REAL 2) | D) | K1)) = [#] ((TOP-REAL 2) | D)
by A26, A22, A23, XBOOLE_0:def 10;
A30:
( f is continuous & g is continuous )
by A2, A5, Th95, Th96;
then consider h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) such that
A31:
h = f +* g
and
h is continuous
by A26, A22, A29, A15, A27, JGRAPH_2:1;
A32:
dom h = the carrier of ((TOP-REAL 2) | D)
by FUNCT_2:def 1;
A33:
dom g = K1
by A16, FUNCT_2:def 1;
( K0 = [#] (((TOP-REAL 2) | D) | K0) & K1 = [#] (((TOP-REAL 2) | D) | K1) )
by PRE_TOPC:def 5;
then A34:
f tolerates g
by A27, A25, A33, PARTFUN1:def 4;
A35:
for x being object st x in dom h holds
h . x = ((sn -FanMorphE) | D) . x
dom (sn -FanMorphE) = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
then dom ((sn -FanMorphE) | D) =
the carrier of (TOP-REAL 2) /\ D
by RELAT_1:61
.=
the carrier of ((TOP-REAL 2) | D)
by A4, XBOOLE_1:28
;
then
f +* g = (sn -FanMorphE) | D
by A31, A32, A35, FUNCT_1:2;
hence
ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (sn -FanMorphE) | D & h is continuous )
by A26, A22, A29, A30, A15, A27, JGRAPH_2:1; verum