set Y1 = |[(- 1),1]|;
set B0 = {(0. (TOP-REAL 2))};
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 Th29, 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:
K0 c= the carrier of (TOP-REAL 2)
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;
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;
then reconsider p =
x as
Point of
(TOP-REAL 2) by A14;
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;
set p9 =
|[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]|;
A25:
(
|[((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;
A26:
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 A27:
(Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]|
by Th28;
A28:
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 A26, XREAL_1:64;
then A29:
( (
(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)))) ) )
;
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, A27, A29, A25;
hence
y in the
carrier of
(((TOP-REAL 2) | D) | K0)
by PRE_TOPC:8;
verum
end;
dom ((Sq_Circ ") | K0) =
(dom (Sq_Circ ")) /\ K0
by RELAT_1:61
.=
the carrier of (TOP-REAL 2) /\ K0
by Th29, FUNCT_2:def 1
.=
K0
by A14, 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;
A32:
K1 = [#] (((TOP-REAL 2) | D) | K1)
by PRE_TOPC:def 5;
A33:
K1 c= the carrier of (TOP-REAL 2)
A34:
rng ((Sq_Circ ") | K1) c= the carrier of (((TOP-REAL 2) | D) | K1)
proof
reconsider K10 =
K1 as
Subset of
(TOP-REAL 2) by A33;
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) )
A35:
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 A39:
x in dom ((Sq_Circ ") | K1)
and A40:
y = ((Sq_Circ ") | K1) . x
by FUNCT_1:def 3;
A41:
x in (dom (Sq_Circ ")) /\ K1
by A39, RELAT_1:61;
then A42:
x in K1
by XBOOLE_0:def 4;
then reconsider p =
x as
Point of
(TOP-REAL 2) by A33;
K10 = the
carrier of
((TOP-REAL 2) | K10)
by PRE_TOPC:8;
then
p in the
carrier of
((TOP-REAL 2) | K10)
by A41, XBOOLE_0:def 4;
then A43:
p `2 <> 0
by A35;
set p9 =
|[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]|;
A44:
(
|[((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;
A45:
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 A42;
then A46:
(Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]|
by Th30;
A47:
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 A45, XREAL_1:64;
then A48:
( (
(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)))) ) )
;
A49:
|[((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 A40, A42, FUNCT_1:49;
then
y in K1
by A50, A46, A48, A44;
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 Th29, FUNCT_2:def 1
.=
K1
by A33, XBOOLE_1:28
;
then reconsider g = (Sq_Circ ") | K1 as Function of (((TOP-REAL 2) | D) | K1),((TOP-REAL 2) | D) by A10, A34, FUNCT_2:2, XBOOLE_1:1;
A51:
dom g = K1
by A10, FUNCT_2:def 1;
g = (Sq_Circ ") | K1
;
then A52:
K1 is closed
by A4, Th40;
A53:
K0 = [#] (((TOP-REAL 2) | D) | K0)
by PRE_TOPC:def 5;
f = (Sq_Circ ") | K0
;
then A56:
K0 is closed
by A4, Th39;
A57:
dom f = K0
by A7, FUNCT_2:def 1;
D = [#] ((TOP-REAL 2) | D)
by PRE_TOPC:def 5;
then A58:
([#] (((TOP-REAL 2) | D) | K0)) \/ ([#] (((TOP-REAL 2) | D) | K1)) = [#] ((TOP-REAL 2) | D)
by A53, A32, A11;
A59:
( f is continuous & g is continuous )
by A4, Th39, Th40;
then consider h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) such that
A60:
h = f +* g
and
h is continuous
by A53, A32, A58, A56, A52, A54, JGRAPH_2:1;
( K0 = [#] (((TOP-REAL 2) | D) | K0) & K1 = [#] (((TOP-REAL 2) | D) | K1) )
by PRE_TOPC:def 5;
then A61:
f tolerates g
by A54, A57, A51, PARTFUN1:def 4;
A62:
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 A60, A2, A62;
hence
ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = (Sq_Circ ") | D & h is continuous )
by A53, A32, A58, A56, A59, A52, A54, JGRAPH_2:1; verum