set Y1 = |[0,1]|;
defpred S1[ Point of (TOP-REAL 2)] means $1 `2 <= 0 ;
reconsider B0 = {(0. (TOP-REAL 2))} as Subset of (TOP-REAL 2) ;
let cn be Real; for D being non empty Subset of (TOP-REAL 2) st - 1 < cn & cn < 1 & D ` = {(0. (TOP-REAL 2))} holds
ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (cn -FanMorphS) | D & h is continuous )
let D be non empty Subset of (TOP-REAL 2); ( - 1 < cn & cn < 1 & D ` = {(0. (TOP-REAL 2))} implies ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (cn -FanMorphS) | D & h is continuous ) )
assume that
A1:
( - 1 < cn & cn < 1 )
and
A2:
D ` = {(0. (TOP-REAL 2))}
; ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (cn -FanMorphS) | D & h is continuous )
A3:
the carrier of ((TOP-REAL 2) | D) = D
by PRE_TOPC:8;
dom (cn -FanMorphS) = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
then A4: dom ((cn -FanMorphS) | D) =
the carrier of (TOP-REAL 2) /\ D
by RELAT_1:61
.=
the carrier of ((TOP-REAL 2) | D)
by A3, XBOOLE_1:28
;
( |[0,(- 1)]| `2 = - 1 & |[0,(- 1)]| <> 0. (TOP-REAL 2) )
by EUCLID:52, JGRAPH_2:3;
then A5:
|[0,(- 1)]| in { p where p is Point of (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) }
;
|[0,1]| `2 = 1
by EUCLID:52;
then A6:
|[0,1]| in { p where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) }
by JGRAPH_2:3;
A7: D =
B0 `
by A2
.=
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(A7);
then reconsider K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | D) by A5;
A8:
K0 = the carrier of (((TOP-REAL 2) | D) | K0)
by PRE_TOPC:8;
defpred S2[ Point of (TOP-REAL 2)] means $1 `2 >= 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(A7);
then reconsider K1 = { p where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | D) by A6;
A9:
( K0 is closed & K1 is closed )
by A7, Th62, Th63;
A10:
the carrier of ((TOP-REAL 2) | D) = D
by PRE_TOPC:8;
A11:
rng ((cn -FanMorphS) | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)
A15:
K0 c= the carrier of (TOP-REAL 2)
dom ((cn -FanMorphS) | K0) =
(dom (cn -FanMorphS)) /\ K0
by RELAT_1:61
.=
the carrier of (TOP-REAL 2) /\ K0
by FUNCT_2:def 1
.=
K0
by A15, XBOOLE_1:28
;
then reconsider f = (cn -FanMorphS) | K0 as Function of (((TOP-REAL 2) | D) | K0),((TOP-REAL 2) | D) by A8, A11, FUNCT_2:2, XBOOLE_1:1;
A16:
K1 = the carrier of (((TOP-REAL 2) | D) | K1)
by PRE_TOPC:8;
A17:
rng ((cn -FanMorphS) | K1) c= the carrier of (((TOP-REAL 2) | D) | K1)
A21:
K1 c= the carrier of (TOP-REAL 2)
dom ((cn -FanMorphS) | K1) =
(dom (cn -FanMorphS)) /\ 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 = (cn -FanMorphS) | 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 A8, 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 A1, A7, Th126, Th127;
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, A9, A27, JGRAPH_2:1;
A32:
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 A33:
f tolerates g
by A27, A25, A32, PARTFUN1:def 4;
A34:
the carrier of ((TOP-REAL 2) | D) = NonZero (TOP-REAL 2)
by A7, PRE_TOPC:8;
A35:
for x being object st x in dom h holds
h . x = ((cn -FanMorphS) | D) . x
dom h = the carrier of ((TOP-REAL 2) | D)
by FUNCT_2:def 1;
then
f +* g = (cn -FanMorphS) | D
by A31, A4, A35, FUNCT_1:2;
hence
ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (cn -FanMorphS) | D & h is continuous )
by A26, A22, A29, A30, A9, A27, JGRAPH_2:1; verum