let sn be Real; :: thesis: 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); :: thesis: ( - 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 A1: ( - 1 < sn & sn < 1 & D ` = {(0. (TOP-REAL 2))} ) ; :: thesis: ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (sn -FanMorphE ) | D & h is continuous )
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 S1[ Point of (TOP-REAL 2)] means $1 `1 >= 0 ;
A3: { 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(A2);
 ( |[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 `1 >= 0 & p <> 0. (TOP-REAL 2) ) } by JGRAPH_2:11;
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 A3;
defpred S2[ Point of (TOP-REAL 2)] means $1 `1 <= 0 ;
A4: { 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(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 `1 <= 0 & p <> 0. (TOP-REAL 2) ) } by JGRAPH_2:11;
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 A4;
A5: the carrier of ((TOP-REAL 2) | D) = D by PRE_TOPC:29;
A6: K0 c= the carrier of (TOP-REAL 2)
proof
let z be set ; :: 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 consider p8 being Point of (TOP-REAL 2) such that
A7: ( p8 = z & p8 `1 >= 0 & p8 <> 0. (TOP-REAL 2) ) ;
thus z in the carrier of (TOP-REAL 2) by A7; :: thesis: verum
end;
A8: dom ((sn -FanMorphE ) | K0) = (dom (sn -FanMorphE )) /\ K0 by RELAT_1:90
.= the carrier of (TOP-REAL 2) /\ K0 by FUNCT_2:def 1
.= K0 by A6, XBOOLE_1:28 ;
A9: K0 = the carrier of (((TOP-REAL 2) | D) | K0) by PRE_TOPC:29;
rng ((sn -FanMorphE ) | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((sn -FanMorphE ) | K0) or y in the carrier of (((TOP-REAL 2) | D) | K0) )
assume y in rng ((sn -FanMorphE ) | K0) ; :: thesis: y in the carrier of (((TOP-REAL 2) | D) | K0)
then consider x being set such that
A10: ( x in dom ((sn -FanMorphE ) | K0) & y = ((sn -FanMorphE ) | K0) . x ) by FUNCT_1:def 5;
x in (dom (sn -FanMorphE )) /\ K0 by A10, RELAT_1:90;
then A11: x in K0 by XBOOLE_0:def 4;
K0 c= the carrier of (TOP-REAL 2) by A5, XBOOLE_1:1;
then reconsider p = x as Point of (TOP-REAL 2) by A11;
(sn -FanMorphE ) . p = y by A10, A11, FUNCT_1:72;
then y in K0 by A1, A11, Th105;
hence y in the carrier of (((TOP-REAL 2) | D) | K0) by PRE_TOPC:29; :: thesis: verum
end;
then reconsider f = (sn -FanMorphE ) | K0 as Function of (((TOP-REAL 2) | D) | K0),((TOP-REAL 2) | D) by A8, A9, FUNCT_2:4, XBOOLE_1:1;
A12: K1 c= the carrier of (TOP-REAL 2)
proof
let z be set ; :: 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 consider p8 being Point of (TOP-REAL 2) such that
A13: ( p8 = z & p8 `1 <= 0 & p8 <> 0. (TOP-REAL 2) ) ;
thus z in the carrier of (TOP-REAL 2) by A13; :: thesis: verum
end;
A14: dom ((sn -FanMorphE ) | K1) = (dom (sn -FanMorphE )) /\ K1 by RELAT_1:90
.= the carrier of (TOP-REAL 2) /\ K1 by FUNCT_2:def 1
.= K1 by A12, XBOOLE_1:28 ;
A15: K1 = the carrier of (((TOP-REAL 2) | D) | K1) by PRE_TOPC:29;
rng ((sn -FanMorphE ) | K1) c= the carrier of (((TOP-REAL 2) | D) | K1)
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((sn -FanMorphE ) | K1) or y in the carrier of (((TOP-REAL 2) | D) | K1) )
assume y in rng ((sn -FanMorphE ) | K1) ; :: thesis: y in the carrier of (((TOP-REAL 2) | D) | K1)
then consider x being set such that
A16: ( x in dom ((sn -FanMorphE ) | K1) & y = ((sn -FanMorphE ) | K1) . x ) by FUNCT_1:def 5;
x in (dom (sn -FanMorphE )) /\ K1 by A16, RELAT_1:90;
then A17: x in K1 by XBOOLE_0:def 4;
K1 c= the carrier of (TOP-REAL 2) by A5, XBOOLE_1:1;
then reconsider p = x as Point of (TOP-REAL 2) by A17;
(sn -FanMorphE ) . p = y by A16, A17, FUNCT_1:72;
then y in K1 by A1, A17, Th106;
hence y in the carrier of (((TOP-REAL 2) | D) | K1) by PRE_TOPC:29; :: thesis: verum
end;
then reconsider g = (sn -FanMorphE ) | K1 as Function of (((TOP-REAL 2) | D) | K1),((TOP-REAL 2) | D) by A14, A15, FUNCT_2:4, XBOOLE_1:1;
A18: K0 = [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 10;
A19: K1 = [#] (((TOP-REAL 2) | D) | K1) by PRE_TOPC:def 10;
A20: D = [#] ((TOP-REAL 2) | D) by PRE_TOPC:def 10;
D c= K0 \/ K1
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in K0 \/ K1 )
assume A21: x in D ; :: thesis: x in K0 \/ K1
then A22: ( 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 A21;
( ( px `1 >= 0 & px <> 0. (TOP-REAL 2) ) or ( px `1 <= 0 & px <> 0. (TOP-REAL 2) ) ) by A22, TARSKI:def 1;
then ( x in K0 or x in K1 ) ;
hence x in K0 \/ K1 by XBOOLE_0:def 3; :: thesis: verum
end;
then A23: ([#] (((TOP-REAL 2) | D) | K0)) \/ ([#] (((TOP-REAL 2) | D) | K1)) = [#] ((TOP-REAL 2) | D) by A18, A19, A20, XBOOLE_0:def 10;
A24: ( f is continuous & K0 is closed ) by A1, A2, Th38, Th102;
A25: ( g is continuous & K1 is closed ) by A1, A2, Th36, Th103;
A26: for x being set st x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) holds
f . x = g . x
proof
let x be set ; :: thesis: ( x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) implies f . x = g . x )
assume A27: x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) ; :: thesis: f . x = g . x
then ( x in K0 & x in K1 ) by A18, A19, XBOOLE_0:def 4;
then f . x = (sn -FanMorphE ) . x by FUNCT_1:72;
hence f . x = g . x by A19, A27, FUNCT_1:72; :: thesis: verum
end;
then consider h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) such that
A28: ( h = f +* g & h is continuous ) by A18, A19, A23, A24, A25, JGRAPH_2:9;
A29: dom h = the carrier of ((TOP-REAL 2) | D) by FUNCT_2:def 1;
A30: the carrier of ((TOP-REAL 2) | D) = D by PRE_TOPC:29;
A31: the carrier of ((TOP-REAL 2) | D) = NonZero (TOP-REAL 2) by A2, PRE_TOPC:29;
dom (sn -FanMorphE ) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A32: dom ((sn -FanMorphE ) | D) = the carrier of (TOP-REAL 2) /\ D by RELAT_1:90
.= the carrier of ((TOP-REAL 2) | D) by A30, XBOOLE_1:28 ;
A33: dom f = K0 by A9, FUNCT_2:def 1;
A34: K0 = [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 10;
A35: dom g = K1 by A15, FUNCT_2:def 1;
K1 = [#] (((TOP-REAL 2) | D) | K1) by PRE_TOPC:def 10;
then A36: f tolerates g by A26, A33, A34, A35, PARTFUN1:def 6;
for x being set st x in dom h holds
h . x = ((sn -FanMorphE ) | D) . x
proof
let x be set ; :: thesis: ( x in dom h implies h . x = ((sn -FanMorphE ) | D) . x )
assume A37: x in dom h ; :: thesis: h . x = ((sn -FanMorphE ) | D) . x
then ( x in the carrier of (TOP-REAL 2) & not x in {(0. (TOP-REAL 2))} ) by A31, XBOOLE_0:def 5;
then A38: x <> 0. (TOP-REAL 2) by TARSKI:def 1;
reconsider p = x as Point of (TOP-REAL 2) by A31, A37, XBOOLE_0:def 5;
A39: x in (D ` ) ` by A29, A37, PRE_TOPC:29;
now
per cases ( x in K0 or not x in K0 ) ;
case A40: x in K0 ; :: thesis: h . x = ((sn -FanMorphE ) | D) . x
A41: ((sn -FanMorphE ) | D) . p = (sn -FanMorphE ) . p by A39, FUNCT_1:72
.= f . p by A40, FUNCT_1:72 ;
h . p = (g +* f) . p by A28, A36, FUNCT_4:35
.= f . p by A33, A40, FUNCT_4:14 ;
hence h . x = ((sn -FanMorphE ) | D) . x by A41; :: thesis: verum
end;
case not x in K0 ; :: thesis: h . x = ((sn -FanMorphE ) | D) . x
then not p `1 >= 0 by A38;
then A42: x in K1 by A38;
((sn -FanMorphE ) | D) . p = (sn -FanMorphE ) . p by A39, FUNCT_1:72
.= g . p by A42, FUNCT_1:72 ;
hence h . x = ((sn -FanMorphE ) | D) . x by A28, A35, A42, FUNCT_4:14; :: thesis: verum
end;
end;
end;
hence h . x = ((sn -FanMorphE ) | D) . x ; :: thesis: verum
end;
then f +* g = (sn -FanMorphE ) | D by A28, A29, A32, FUNCT_1:9;
hence ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (sn -FanMorphE ) | D & h is continuous ) by A18, A19, A23, A24, A25, A26, JGRAPH_2:9; :: thesis: verum