set Y1 = |[(- 1),1]|;
let D be non empty Subset of (TOP-REAL 2); ( D ` = {(0. (TOP-REAL 2))} implies ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = Sq_Circ | D & h is continuous ) )
A1:
the carrier of ((TOP-REAL 2) | D) = D
by PRE_TOPC:8;
dom Sq_Circ = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
then A2: dom (Sq_Circ | D) =
the carrier of (TOP-REAL 2) /\ D
by RELAT_1:61
.=
the carrier of ((TOP-REAL 2) | D)
by A1, XBOOLE_1:28
;
assume A3:
D ` = {(0. (TOP-REAL 2))}
; ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = Sq_Circ | D & h is continuous )
then A4: D =
{(0. (TOP-REAL 2))} `
.=
NonZero (TOP-REAL 2)
by SUBSET_1:def 4
;
A5:
{ p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } c= the carrier of ((TOP-REAL 2) | D)
1.REAL 2 in { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) }
by Lm9, Lm10;
then reconsider K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | D) by A5;
A7:
K0 = the carrier of (((TOP-REAL 2) | D) | K0)
by PRE_TOPC:8;
A8:
{ p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } c= the carrier of ((TOP-REAL 2) | D)
( |[(- 1),1]| `1 = - 1 & |[(- 1),1]| `2 = 1 )
by EUCLID:52;
then
|[(- 1),1]| in { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) }
by JGRAPH_2:3;
then reconsider K1 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | D) by A8;
A10:
K1 = the carrier of (((TOP-REAL 2) | D) | K1)
by PRE_TOPC:8;
A11:
D c= K0 \/ K1
A13: the carrier of ((TOP-REAL 2) | D) =
[#] ((TOP-REAL 2) | D)
.=
NonZero (TOP-REAL 2)
by A4, PRE_TOPC:def 5
;
A14:
the carrier of ((TOP-REAL 2) | D) = D
by PRE_TOPC:8;
A15:
rng (Sq_Circ | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)
proof
reconsider K00 =
K0 as
Subset of
(TOP-REAL 2) by A14, XBOOLE_1:1;
let y be
object ;
TARSKI:def 3 ( not y in rng (Sq_Circ | K0) or y in the carrier of (((TOP-REAL 2) | D) | K0) )
A16:
for
q being
Point of
(TOP-REAL 2) st
q in the
carrier of
((TOP-REAL 2) | K00) holds
q `1 <> 0
assume
y in rng (Sq_Circ | K0)
;
y in the carrier of (((TOP-REAL 2) | D) | K0)
then consider x being
object such that A20:
x in dom (Sq_Circ | K0)
and A21:
y = (Sq_Circ | K0) . x
by FUNCT_1:def 3;
A22:
x in (dom Sq_Circ) /\ K0
by A20, RELAT_1:61;
then A23:
x in K0
by XBOOLE_0:def 4;
K0 c= the
carrier of
(TOP-REAL 2)
by A14, XBOOLE_1:1;
then reconsider p =
x as
Point of
(TOP-REAL 2) by A23;
K00 = the
carrier of
((TOP-REAL 2) | K00)
by PRE_TOPC:8;
then
p in the
carrier of
((TOP-REAL 2) | K00)
by A22, XBOOLE_0:def 4;
then A24:
p `1 <> 0
by A16;
A25:
ex
px being
Point of
(TOP-REAL 2) st
(
x = px & ( (
px `2 <= px `1 &
- (px `1) <= px `2 ) or (
px `2 >= px `1 &
px `2 <= - (px `1) ) ) &
px <> 0. (TOP-REAL 2) )
by A23;
then A26:
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]|
by Def1;
A27:
sqrt (1 + (((p `2) / (p `1)) ^2)) > 0
by Lm1, SQUARE_1:25;
then
( (
(p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) <= (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) &
(- (p `1)) / (sqrt (1 + (((p `2) / (p `1)) ^2))) <= (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) ) or (
(p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) >= (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) &
(p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) <= (- (p `1)) / (sqrt (1 + (((p `2) / (p `1)) ^2))) ) )
by A25, XREAL_1:72;
then A28:
( (
(p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) <= (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) &
- ((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))) <= (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) ) or (
(p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) >= (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) &
(p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) <= - ((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))) ) )
by XCMPLX_1:187;
set p9 =
|[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]|;
A29:
(
|[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1 = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) &
|[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `2 = (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) )
by EUCLID:52;
A30:
|[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| `1 = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))
by EUCLID:52;
Sq_Circ . p = y
by A21, A23, FUNCT_1:49;
then
y in K0
by A31, A26, A28, A29;
then
y in [#] (((TOP-REAL 2) | D) | K0)
by PRE_TOPC:def 5;
hence
y in the
carrier of
(((TOP-REAL 2) | D) | K0)
;
verum
end;
A32:
K0 c= the carrier of (TOP-REAL 2)
dom (Sq_Circ | K0) =
(dom Sq_Circ) /\ K0
by RELAT_1:61
.=
the carrier of (TOP-REAL 2) /\ K0
by FUNCT_2:def 1
.=
K0
by A32, XBOOLE_1:28
;
then reconsider f = Sq_Circ | K0 as Function of (((TOP-REAL 2) | D) | K0),((TOP-REAL 2) | D) by A7, A15, FUNCT_2:2, XBOOLE_1:1;
A33:
K1 = [#] (((TOP-REAL 2) | D) | K1)
by PRE_TOPC:def 5;
A34:
K1 c= the carrier of (TOP-REAL 2)
A35:
rng (Sq_Circ | K1) c= the carrier of (((TOP-REAL 2) | D) | K1)
proof
reconsider K10 =
K1 as
Subset of
(TOP-REAL 2) by A34;
let y be
object ;
TARSKI:def 3 ( not y in rng (Sq_Circ | K1) or y in the carrier of (((TOP-REAL 2) | D) | K1) )
A36:
for
q being
Point of
(TOP-REAL 2) st
q in the
carrier of
((TOP-REAL 2) | K10) holds
q `2 <> 0
assume
y in rng (Sq_Circ | K1)
;
y in the carrier of (((TOP-REAL 2) | D) | K1)
then consider x being
object such that A40:
x in dom (Sq_Circ | K1)
and A41:
y = (Sq_Circ | K1) . x
by FUNCT_1:def 3;
A42:
x in (dom Sq_Circ) /\ K1
by A40, RELAT_1:61;
then A43:
x in K1
by XBOOLE_0:def 4;
then reconsider p =
x as
Point of
(TOP-REAL 2) by A34;
K10 = the
carrier of
((TOP-REAL 2) | K10)
by PRE_TOPC:8;
then
p in the
carrier of
((TOP-REAL 2) | K10)
by A42, XBOOLE_0:def 4;
then A44:
p `2 <> 0
by A36;
set p9 =
|[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]|;
A45:
(
|[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2 = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) &
|[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `1 = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) )
by EUCLID:52;
A46:
ex
px being
Point of
(TOP-REAL 2) st
(
x = px & ( (
px `1 <= px `2 &
- (px `2) <= px `1 ) or (
px `1 >= px `2 &
px `1 <= - (px `2) ) ) &
px <> 0. (TOP-REAL 2) )
by A43;
then A47:
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]|
by Th4;
A48:
sqrt (1 + (((p `1) / (p `2)) ^2)) > 0
by Lm1, SQUARE_1:25;
then
( (
(p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) <= (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) &
(- (p `2)) / (sqrt (1 + (((p `1) / (p `2)) ^2))) <= (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ) or (
(p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) >= (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) &
(p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) <= (- (p `2)) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ) )
by A46, XREAL_1:72;
then A49:
( (
(p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) <= (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) &
- ((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2)))) <= (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ) or (
(p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) >= (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) &
(p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) <= - ((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2)))) ) )
by XCMPLX_1:187;
A50:
|[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| `2 = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2)))
by EUCLID:52;
Sq_Circ . p = y
by A41, A43, FUNCT_1:49;
then
y in K1
by A51, A47, A49, A45;
hence
y in the
carrier of
(((TOP-REAL 2) | D) | K1)
by PRE_TOPC:8;
verum
end;
dom (Sq_Circ | K1) =
(dom Sq_Circ) /\ K1
by RELAT_1:61
.=
the carrier of (TOP-REAL 2) /\ K1
by FUNCT_2:def 1
.=
K1
by A34, XBOOLE_1:28
;
then reconsider g = Sq_Circ | K1 as Function of (((TOP-REAL 2) | D) | K1),((TOP-REAL 2) | D) by A10, A35, FUNCT_2:2, XBOOLE_1:1;
A52:
dom g = K1
by A10, FUNCT_2:def 1;
g = Sq_Circ | K1
;
then A53:
K1 is closed
by A4, Th18;
A54:
K0 = [#] (((TOP-REAL 2) | D) | K0)
by PRE_TOPC:def 5;
A55:
for x being object st x in ([#] (((TOP-REAL 2) | D) | K0)) /\ ([#] (((TOP-REAL 2) | D) | K1)) holds
f . x = g . x
f = Sq_Circ | K0
;
then A57:
K0 is closed
by A4, Th17;
A58:
dom f = K0
by A7, FUNCT_2:def 1;
D = [#] ((TOP-REAL 2) | D)
by PRE_TOPC:def 5;
then A59:
([#] (((TOP-REAL 2) | D) | K0)) \/ ([#] (((TOP-REAL 2) | D) | K1)) = [#] ((TOP-REAL 2) | D)
by A54, A33, A11;
A60:
( f is continuous & g is continuous )
by A4, Th17, Th18;
then consider h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) such that
A61:
h = f +* g
and
h is continuous
by A54, A33, A59, A57, A53, A55, JGRAPH_2:1;
( K0 = [#] (((TOP-REAL 2) | D) | K0) & K1 = [#] (((TOP-REAL 2) | D) | K1) )
by PRE_TOPC:def 5;
then A62:
f tolerates g
by A55, A58, A52, PARTFUN1:def 4;
A63:
for x being object st x in dom h holds
h . x = (Sq_Circ | D) . x
dom h = the carrier of ((TOP-REAL 2) | D)
by FUNCT_2:def 1;
then
f +* g = Sq_Circ | D
by A61, A2, A63;
hence
ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = Sq_Circ | D & h is continuous )
by A54, A33, A59, A57, A60, A53, A55, JGRAPH_2:1; verum