|[0,1]| `2 = 1 by EUCLID:52;
then A1: |[0,1]| in { p where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } by JGRAPH_2:3;
set Y1 = |[0,(- 1)]|;
reconsider B0 = {(0. (TOP-REAL 2))} as Subset of (TOP-REAL 2) ;
defpred S1[ Point of (TOP-REAL 2)] means $1 `2 >= 0 ;
let cn be Real; :: thesis: 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 -FanMorphN) | D & h is continuous )
let D be non empty Subset of (TOP-REAL 2); :: thesis: ( - 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 -FanMorphN) | D & h is continuous ) )
assume that
A2: ( - 1 < cn & cn < 1 ) and
A3: D ` = {(0. (TOP-REAL 2))} ; :: thesis: ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (cn -FanMorphN) | 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 `2 >= 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 ((cn -FanMorphN) | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((cn -FanMorphN) | K0) or y in the carrier of (((TOP-REAL 2) | D) | K0) )
assume y in rng ((cn -FanMorphN) | K0) ; :: thesis: y in the carrier of (((TOP-REAL 2) | D) | K0)
then consider x being object such that
A9: x in dom ((cn -FanMorphN) | K0) and
A10: y = ((cn -FanMorphN) | K0) . x by FUNCT_1:def 3;
x in (dom (cn -FanMorphN)) /\ K0 by A9, RELAT_1:61;
then A11: x in K0 by XBOOLE_0:def 4;
K0 c= the carrier of (TOP-REAL 2) by A7, XBOOLE_1:1;
then reconsider p = x as Point of (TOP-REAL 2) by A11;
(cn -FanMorphN) . p = y by A10, A11, FUNCT_1:49;
then y in K0 by A2, A11, Th67;
hence y in the carrier of (((TOP-REAL 2) | D) | K0) by PRE_TOPC:8; :: thesis: verum
end;
A12: K0 c= the carrier of (TOP-REAL 2)
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in K0 or z in the carrier of (TOP-REAL 2) )
assume z in K0 ; :: thesis: z in the carrier of (TOP-REAL 2)
then ex p8 being Point of (TOP-REAL 2) st
( p8 = z & p8 `2 >= 0 & p8 <> 0. (TOP-REAL 2) ) ;
hence z in the carrier of (TOP-REAL 2) ; :: thesis: verum
end;
( |[0,(- 1)]| `2 = - 1 & 0. (TOP-REAL 2) <> |[0,(- 1)]| ) by EUCLID:52, JGRAPH_2:3;
then A13: |[0,(- 1)]| in { p where p is Point of (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } ;
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 `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(A5);
 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 A13;
A15: ( K0 is closed & K1 is closed ) by A5, Th62, Th63;
dom ((cn -FanMorphN) | K0) = (dom (cn -FanMorphN)) /\ 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 = (cn -FanMorphN) | 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 ((cn -FanMorphN) | K1) c= the carrier of (((TOP-REAL 2) | D) | K1)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((cn -FanMorphN) | K1) or y in the carrier of (((TOP-REAL 2) | D) | K1) )
assume y in rng ((cn -FanMorphN) | K1) ; :: thesis: y in the carrier of (((TOP-REAL 2) | D) | K1)
then consider x being object such that
A18: x in dom ((cn -FanMorphN) | K1) and
A19: y = ((cn -FanMorphN) | K1) . x by FUNCT_1:def 3;
x in (dom (cn -FanMorphN)) /\ K1 by A18, RELAT_1:61;
then A20: x in K1 by XBOOLE_0:def 4;
K1 c= the carrier of (TOP-REAL 2) by A7, XBOOLE_1:1;
then reconsider p = x as Point of (TOP-REAL 2) by A20;
(cn -FanMorphN) . p = y by A19, A20, FUNCT_1:49;
then y in K1 by A2, A20, Th68;
hence y in the carrier of (((TOP-REAL 2) | D) | K1) by PRE_TOPC:8; :: thesis: verum
end;
A21: K1 c= the carrier of (TOP-REAL 2)
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in K1 or z in the carrier of (TOP-REAL 2) )
assume z in K1 ; :: thesis: z in the carrier of (TOP-REAL 2)
then ex p8 being Point of (TOP-REAL 2) st
( p8 = z & p8 `2 <= 0 & p8 <> 0. (TOP-REAL 2) ) ;
hence z in the carrier of (TOP-REAL 2) ; :: thesis: verum
end;
dom ((cn -FanMorphN) | K1) = (dom (cn -FanMorphN)) /\ 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 -FanMorphN) | 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
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in K0 \/ K1 )
assume A24: x in D ; :: thesis: x in K0 \/ K1
then reconsider px = x as Point of (TOP-REAL 2) ;
not x in {(0. (TOP-REAL 2))} by A5, A24, XBOOLE_0:def 5;
then ( ( px `2 >= 0 & px <> 0. (TOP-REAL 2) ) or ( px `2 <= 0 & px <> 0. (TOP-REAL 2) ) ) by TARSKI:def 1;
then ( x in K0 or x in K1 ) ;
hence x in K0 \/ K1 by XBOOLE_0:def 3; :: thesis: verum
end;
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
proof
let x be object ; :: thesis: ( x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) implies f . x = g . x )
assume A28: x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) ; :: thesis: f . x = g . x
then x in K0 by A26, XBOOLE_0:def 4;
then f . x = (cn -FanMorphN) . x by FUNCT_1:49;
hence f . x = g . x by A22, A28, FUNCT_1:49; :: thesis: verum
end;
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, Th64, Th65;
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 = ((cn -FanMorphN) | D) . x
proof
let x be object ; :: thesis: ( x in dom h implies h . x = ((cn -FanMorphN) | D) . x )
assume A36: x in dom h ; :: thesis: h . x = ((cn -FanMorphN) | D) . x
then reconsider p = x as Point of (TOP-REAL 2) by A14, XBOOLE_0:def 5;
not x in {(0. (TOP-REAL 2))} by A14, A36, XBOOLE_0:def 5;
then A37: x <> 0. (TOP-REAL 2) by TARSKI:def 1;
A38: x in (D `) ` by A32, A36, PRE_TOPC:8;
now :: thesis: ( ( x in K0 & h . x = ((cn -FanMorphN) | D) . x ) or ( not x in K0 & h . x = ((cn -FanMorphN) | D) . x ) )
per cases ( x in K0 or not x in K0 ) ;
case A39: x in K0 ; :: thesis: h . x = ((cn -FanMorphN) | D) . x
A40: ((cn -FanMorphN) | D) . p = (cn -FanMorphN) . p by A38, FUNCT_1:49
.= f . p by A39, FUNCT_1:49 ;
h . p = (g +* f) . p by A31, A34, FUNCT_4:34
.= f . p by A25, A39, FUNCT_4:13 ;
hence h . x = ((cn -FanMorphN) | D) . x by A40; :: thesis: verum
end;
case not x in K0 ; :: thesis: h . x = ((cn -FanMorphN) | D) . x
then not p `2 >= 0 by A37;
then A41: x in K1 by A37;
((cn -FanMorphN) | D) . p = (cn -FanMorphN) . p by A38, FUNCT_1:49
.= g . p by A41, FUNCT_1:49 ;
hence h . x = ((cn -FanMorphN) | D) . x by A31, A33, A41, FUNCT_4:13; :: thesis: verum
end;
end;
end;
hence h . x = ((cn -FanMorphN) | D) . x ; :: thesis: verum
end;
dom (cn -FanMorphN) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then dom ((cn -FanMorphN) | 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 = (cn -FanMorphN) | D by A31, A32, A35, FUNCT_1:2;
hence ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (cn -FanMorphN) | D & h is continuous ) by A26, A22, A29, A30, A15, A27, JGRAPH_2:1; :: thesis: verum