let cn be Real; :: thesis:
let D be non empty Subset of (TOP-REAL 2); :: thesis:
assume A1: ( - 1 < cn & cn < 1 & D ` = {(0. (TOP-REAL 2))} ) ; :: thesis:
reconsider B0 = {(0. (TOP-REAL 2))} as Subset of (TOP-REAL 2) ;
A2: D = B0 ` by A1
.= NonZero (TOP-REAL 2) by SUBSET_1:def 5 ;
defpred S₁[ Point of (TOP-REAL 2)] means $1 `2 <= 0 ;
A3: { p where p is Point of (TOP-REAL 2) : ( S₁[p] & p <> 0. (TOP-REAL 2) ) } c= the carrier of ((TOP-REAL 2) | D) from JGRAPH_4:sch 1(A2);
A4: ( |[0 ,(- 1)]| `1 = 0 & |[0 ,(- 1)]| `2 = - 1 ) by EUCLID:56;
|[0 ,(- 1)]| <> 0. (TOP-REAL 2) by EUCLID:56, JGRAPH_2:11;
then |[0 ,(- 1)]| in { p where p is Point of (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } by A4;
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 A3;
defpred S₂[ Point of (TOP-REAL 2)] means $1 `2 >= 0 ;
A5: { p where p is Point of (TOP-REAL 2) : ( S₂[p] & p <> 0. (TOP-REAL 2) ) } c= the carrier of ((TOP-REAL 2) | D) from JGRAPH_4:sch 1(A2);
set Y1 = |[0 ,1]|;
( |[0 ,1]| `1 = 0 & |[0 ,1]| `2 = 1 ) by EUCLID:56;
then |[0 ,1]| in { p where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } by JGRAPH_2:11;
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 A5;
A6: the carrier of ((TOP-REAL 2) | D) = D by PRE_TOPC:29;
A7: K0 c= the carrier of (TOP-REAL 2)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in K0 ; :: thesis:
then consider p8 being Point of (TOP-REAL 2) such that
A8: ( p8 = z & p8 `2 <= 0 & p8 <> 0. (TOP-REAL 2) ) ;
thus z in the carrier of (TOP-REAL 2) by A8; :: thesis:

end;

A9: dom ((cn -FanMorphS ) | K0) = (dom (cn -FanMorphS )) /\ K0 by RELAT_1:90
.= the carrier of (TOP-REAL 2) /\ K0 by FUNCT_2:def 1
.= K0 by A7, XBOOLE_1:28 ;
A10: K0 = the carrier of (((TOP-REAL 2) | D) | K0) by PRE_TOPC:29;
rng ((cn -FanMorphS ) | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng ((cn -FanMorphS ) | K0) ; :: thesis:
then consider x being set such that
A11: ( x in dom ((cn -FanMorphS ) | K0) & y = ((cn -FanMorphS ) | K0) . x ) by FUNCT_1:def 5;
x in (dom (cn -FanMorphS )) /\ K0 by A11, RELAT_1:90;
then A12: x in K0 by XBOOLE_0:def 4;
K0 c= the carrier of (TOP-REAL 2) by A6, XBOOLE_1:1;
then reconsider p = x as Point of (TOP-REAL 2) by A12;
(cn -FanMorphS ) . p = y by A11, A12, FUNCT_1:72;
then y in K0 by A1, A12, Th136;
hence y in the carrier of (((TOP-REAL 2) | D) | K0) by PRE_TOPC:29; :: thesis:

end;

then reconsider f = (cn -FanMorphS ) | K0 as Function of (((TOP-REAL 2) | D) | K0),((TOP-REAL 2) | D) by A9, A10, FUNCT_2:4, XBOOLE_1:1;
A13: K1 c= the carrier of (TOP-REAL 2)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in K1 ; :: thesis:
then consider p8 being Point of (TOP-REAL 2) such that
A14: ( p8 = z & p8 `2 >= 0 & p8 <> 0. (TOP-REAL 2) ) ;
thus z in the carrier of (TOP-REAL 2) by A14; :: thesis:

end;

A15: dom ((cn -FanMorphS ) | K1) = (dom (cn -FanMorphS )) /\ K1 by RELAT_1:90
.= the carrier of (TOP-REAL 2) /\ K1 by FUNCT_2:def 1
.= K1 by A13, XBOOLE_1:28 ;
A16: K1 = the carrier of (((TOP-REAL 2) | D) | K1) by PRE_TOPC:29;
rng ((cn -FanMorphS ) | K1) c= the carrier of (((TOP-REAL 2) | D) | K1)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng ((cn -FanMorphS ) | K1) ; :: thesis:
then consider x being set such that
A17: ( x in dom ((cn -FanMorphS ) | K1) & y = ((cn -FanMorphS ) | K1) . x ) by FUNCT_1:def 5;
x in (dom (cn -FanMorphS )) /\ K1 by A17, RELAT_1:90;
then A18: x in K1 by XBOOLE_0:def 4;
K1 c= the carrier of (TOP-REAL 2) by A6, XBOOLE_1:1;
then reconsider p = x as Point of (TOP-REAL 2) by A18;
(cn -FanMorphS ) . p = y by A17, A18, FUNCT_1:72;
then y in K1 by A1, A18, Th137;
hence y in the carrier of (((TOP-REAL 2) | D) | K1) by PRE_TOPC:29; :: thesis:

end;

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A22: x in D ; :: thesis:
then A23: ( x in the carrier of (TOP-REAL 2) & not x in {(0. (TOP-REAL 2))} ) by A2, XBOOLE_0:def 5;
reconsider px = x as Point of (TOP-REAL 2) by A22;
( ( px `2 >= 0 & px <> 0. (TOP-REAL 2) ) or ( px `2 <= 0 & px <> 0. (TOP-REAL 2) ) ) by A23, TARSKI:def 1;
then ( x in K1 or x in K0 ) ;
hence x in K0 \/ K1 by XBOOLE_0:def 3; :: thesis:

end;

proof

let x be set ; :: thesis:
assume A28: x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) ; :: thesis:
then ( x in K0 & x in K1 ) by A19, A20, XBOOLE_0:def 4;
then f . x = (cn -FanMorphS ) . x by FUNCT_1:72;
hence f . x = g . x by A20, A28, FUNCT_1:72; :: thesis:

end;

then consider h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) such that
A29: ( h = f +* g & h is continuous ) by A19, A20, A24, A25, A26, JGRAPH_2:9;
A30: dom h = the carrier of ((TOP-REAL 2) | D) by FUNCT_2:def 1;
A31: the carrier of ((TOP-REAL 2) | D) = D by PRE_TOPC:29;
A32: the carrier of ((TOP-REAL 2) | D) = NonZero (TOP-REAL 2) by A2, PRE_TOPC:29;
dom (cn -FanMorphS ) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A33: dom ((cn -FanMorphS ) | D) = the carrier of (TOP-REAL 2) /\ D by RELAT_1:90
.= the carrier of ((TOP-REAL 2) | D) by A31, XBOOLE_1:28 ;
A34: dom f = K0 by A10, FUNCT_2:def 1;
A35: K0 = [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 10;
A36: dom g = K1 by A16, FUNCT_2:def 1;
K1 = [#] (((TOP-REAL 2) | D) | K1) by PRE_TOPC:def 10;
then A37: f tolerates g by A27, A34, A35, A36, PARTFUN1:def 6;
for x being set st x in dom h holds
h . x = ((cn -FanMorphS ) | D) . x

proof

let x be set ; :: thesis:
assume A38: x in dom h ; :: thesis:
then ( x in the carrier of (TOP-REAL 2) & not x in {(0. (TOP-REAL 2))} ) by A2, A31, XBOOLE_0:def 5;
then A39: x <> 0. (TOP-REAL 2) by TARSKI:def 1;
reconsider p = x as Point of (TOP-REAL 2) by A32, A38, XBOOLE_0:def 5;

per cases ;

suppose A40: x in K0 ; :: thesis:

A41: ((cn -FanMorphS ) | D) . p = (cn -FanMorphS ) . p by A31, A38, FUNCT_1:72
.= f . p by A40, FUNCT_1:72 ;
h . p = (g +* f) . p by A29, A37, FUNCT_4:35
.= f . p by A34, A40, FUNCT_4:14 ;
hence h . x = ((cn -FanMorphS ) | D) . x by A41; :: thesis:

end;

suppose not x in K0 ; :: thesis:

then not p `2 <= 0 by A39;
then A42: x in K1 by A39;
((cn -FanMorphS ) | D) . p = (cn -FanMorphS ) . p by A31, A38, FUNCT_1:72
.= g . p by A42, FUNCT_1:72 ;
hence h . x = ((cn -FanMorphS ) | D) . x by A29, A36, A42, FUNCT_4:14; :: thesis:

end;

then f +* g = (cn -FanMorphS ) | D by A29, A30, A33, FUNCT_1:9;
hence ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (cn -FanMorphS ) | D & h is continuous ) by A19, A20, A24, A25, A26, A27, JGRAPH_2:9; :: thesis: