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; :: 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 -FanMorphS) | 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 -FanMorphS) | D & h is continuous ) )
assume that
A1: ( - 1 < cn & cn < 1 ) and
A2: D ` = {(0. (TOP-REAL 2))} ; :: thesis: 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)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((cn -FanMorphS) | K0) or y in the carrier of (((TOP-REAL 2) | D) | K0) )
assume y in rng ((cn -FanMorphS) | K0) ; :: thesis: y in the carrier of (((TOP-REAL 2) | D) | K0)
then consider x being object such that
A12: x in dom ((cn -FanMorphS) | K0) and
A13: y = ((cn -FanMorphS) | K0) . x by FUNCT_1:def 3;
x in (dom (cn -FanMorphS)) /\ K0 by A12, RELAT_1:61;
then A14: x in K0 by XBOOLE_0:def 4;
K0 c= the carrier of (TOP-REAL 2) by A10, XBOOLE_1:1;
then reconsider p = x as Point of (TOP-REAL 2) by A14;
(cn -FanMorphS) . p = y by A13, A14, FUNCT_1:49;
then y in K0 by A1, A14, Th129;
hence y in the carrier of (((TOP-REAL 2) | D) | K0) by PRE_TOPC:8; :: thesis: verum
end;
A15: 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;
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)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((cn -FanMorphS) | K1) or y in the carrier of (((TOP-REAL 2) | D) | K1) )
assume y in rng ((cn -FanMorphS) | K1) ; :: thesis: y in the carrier of (((TOP-REAL 2) | D) | K1)
then consider x being object such that
A18: x in dom ((cn -FanMorphS) | K1) and
A19: y = ((cn -FanMorphS) | K1) . x by FUNCT_1:def 3;
x in (dom (cn -FanMorphS)) /\ 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 A10, XBOOLE_1:1;
then reconsider p = x as Point of (TOP-REAL 2) by A20;
(cn -FanMorphS) . p = y by A19, A20, FUNCT_1:49;
then y in K1 by A1, A20, Th130;
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 -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
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 A7, 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 K1 or x in K0 ) ;
hence x in K0 \/ K1 by XBOOLE_0:def 3; :: thesis: verum
end;
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
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 -FanMorphS) . 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 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
proof
let x be object ; :: thesis: ( x in dom h implies h . x = ((cn -FanMorphS) | D) . x )
assume A36: x in dom h ; :: thesis: h . x = ((cn -FanMorphS) | D) . x
then reconsider p = x as Point of (TOP-REAL 2) by A34, XBOOLE_0:def 5;
not x in {(0. (TOP-REAL 2))} by A7, A3, A36, XBOOLE_0:def 5;
then A37: x <> 0. (TOP-REAL 2) by TARSKI:def 1;
per cases ( x in K0 or not x in K0 ) ;
suppose A38: x in K0 ; :: thesis: h . x = ((cn -FanMorphS) | D) . x
A39: ((cn -FanMorphS) | D) . p = (cn -FanMorphS) . p by A3, A36, FUNCT_1:49
.= f . p by A38, FUNCT_1:49 ;
h . p = (g +* f) . p by A31, A33, FUNCT_4:34
.= f . p by A25, A38, FUNCT_4:13 ;
hence h . x = ((cn -FanMorphS) | D) . x by A39; :: thesis: verum
end;
suppose not x in K0 ; :: thesis: h . x = ((cn -FanMorphS) | D) . x
then not p `2 <= 0 by A37;
then A40: x in K1 by A37;
((cn -FanMorphS) | D) . p = (cn -FanMorphS) . p by A3, A36, FUNCT_1:49
.= g . p by A40, FUNCT_1:49 ;
hence h . x = ((cn -FanMorphS) | D) . x by A31, A32, A40, FUNCT_4:13; :: thesis: verum
end;
end;
end;
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; :: thesis: verum