let f be FinSequence of (TOP-REAL 2); for Q being Subset of (TOP-REAL 2)
for i being Nat st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds
First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)
let Q be Subset of (TOP-REAL 2); for i being Nat st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds
First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)
let i be Nat; ( L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) implies First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) )
assume that
A1:
L~ f meets Q
and
A2:
Q is closed
and
A3:
f is being_S-Seq
and
A4:
( 1 <= i & i + 1 <= len f )
and
A5:
First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i)
; First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)
len f >= 2
by A3, TOPREAL1:def 8;
then reconsider P = L~ f, R = LSeg (f,i) as non empty Subset of the carrier of (TOP-REAL 2) by A5, TOPREAL1:23;
A6:
P is_an_arc_of f /. 1,f /. (len f)
by A3, TOPREAL1:25;
set FPO = First_Point (R,(f /. i),(f /. (i + 1)),Q);
set FPG = First_Point (P,(f /. 1),(f /. (len f)),Q);
A7:
(L~ f) /\ Q is closed
by A2, TOPS_1:8;
then
First_Point (P,(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q
by A1, A6, Def1;
then A8:
First_Point (P,(f /. 1),(f /. (len f)),Q) in Q
by XBOOLE_0:def 4;
A9:
i + 1 in dom f
by A4, SEQ_4:134;
A10:
( f is one-to-one & i in dom f )
by A3, A4, SEQ_4:134, TOPREAL1:def 8;
A11:
f /. i <> f /. (i + 1)
First_Point (P,(f /. 1),(f /. (len f)),Q) = First_Point (R,(f /. i),(f /. (i + 1)),Q)
proof
First_Point (
P,
(f /. 1),
(f /. (len f)),
Q)
in (L~ f) /\ Q
by A1, A7, A6, Def1;
then A12:
First_Point (
P,
(f /. 1),
(f /. (len f)),
Q)
in L~ f
by XBOOLE_0:def 4;
consider F being
Function of
I[01],
((TOP-REAL 2) | P) such that A13:
F is
being_homeomorphism
and A14:
(
F . 0 = f /. 1 &
F . 1
= f /. (len f) )
by A6, TOPREAL1:def 1;
rng F =
[#] ((TOP-REAL 2) | P)
by A13, TOPS_2:def 5
.=
L~ f
by PRE_TOPC:def 5
;
then consider s21 being
object such that A15:
s21 in dom F
and A16:
F . s21 = First_Point (
P,
(f /. 1),
(f /. (len f)),
Q)
by A12, FUNCT_1:def 3;
A17:
dom F =
[#] I[01]
by A13, TOPS_2:def 5
.=
[.0,1.]
by BORSUK_1:40
;
then reconsider s21 =
s21 as
Real by A15;
A18:
s21 <= 1
by A15, BORSUK_1:43;
A19:
for
g being
Function of
I[01],
((TOP-REAL 2) | R) for
s2 being
Real st
g is
being_homeomorphism &
g . 0 = f /. i &
g . 1
= f /. (i + 1) &
g . s2 = First_Point (
P,
(f /. 1),
(f /. (len f)),
Q) &
0 <= s2 &
s2 <= 1 holds
for
t being
Real st
0 <= t &
t < s2 holds
not
g . t in Q
proof
consider ppi,
pi1 being
Real such that A20:
ppi < pi1
and A21:
0 <= ppi
and
ppi <= 1
and
0 <= pi1
and A22:
pi1 <= 1
and A23:
LSeg (
f,
i)
= F .: [.ppi,pi1.]
and A24:
F . ppi = f /. i
and A25:
F . pi1 = f /. (i + 1)
by A3, A4, A13, A14, JORDAN5B:7;
A26:
ppi in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) }
by A20;
then reconsider Poz =
[.ppi,pi1.] as non
empty Subset of
I[01] by A21, A22, BORSUK_1:40, RCOMP_1:def 1, XXREAL_1:34;
consider hh being
Function of
(I[01] | Poz),
((TOP-REAL 2) | R) such that A27:
hh = F | Poz
and A28:
hh is
being_homeomorphism
by A3, A4, A13, A14, A23, JORDAN5B:8;
A29:
hh = F * (id Poz)
by A27, RELAT_1:65;
A30:
[.ppi,pi1.] c= [.0,1.]
by A21, A22, XXREAL_1:34;
reconsider A =
Closed-Interval-TSpace (
ppi,
pi1) as
strict SubSpace of
I[01] by A20, A21, A22, TOPMETR:20, TREAL_1:3;
Poz = [#] A
by A20, TOPMETR:18;
then A31:
I[01] | Poz = A
by PRE_TOPC:def 5;
hh " is
being_homeomorphism
by A28, TOPS_2:56;
then A32:
(
hh " is
continuous &
hh " is
one-to-one )
by TOPS_2:def 5;
pi1 in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) }
by A20;
then
pi1 in [.ppi,pi1.]
by RCOMP_1:def 1;
then
pi1 in (dom F) /\ Poz
by A17, A30, XBOOLE_0:def 4;
then A33:
pi1 in dom hh
by A27, RELAT_1:61;
then A34:
hh . pi1 = f /. (i + 1)
by A25, A27, FUNCT_1:47;
the
carrier of
((TOP-REAL 2) | P) =
[#] ((TOP-REAL 2) | P)
.=
P
by PRE_TOPC:def 5
;
then reconsider SEG =
LSeg (
f,
i) as non
empty Subset of the
carrier of
((TOP-REAL 2) | P) by A5, TOPREAL3:19;
A35: the
carrier of
(((TOP-REAL 2) | P) | SEG) =
[#] (((TOP-REAL 2) | P) | SEG)
.=
SEG
by PRE_TOPC:def 5
;
reconsider SE =
SEG as non
empty Subset of
(TOP-REAL 2) ;
let g be
Function of
I[01],
((TOP-REAL 2) | R);
for s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = First_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Qlet s2 be
Real;
( g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = First_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 implies for t being Real st 0 <= t & t < s2 holds
not g . t in Q )
assume that A36:
g is
being_homeomorphism
and A37:
g . 0 = f /. i
and A38:
g . 1
= f /. (i + 1)
and A39:
g . s2 = First_Point (
P,
(f /. 1),
(f /. (len f)),
Q)
and A40:
0 <= s2
and A41:
s2 <= 1
;
for t being Real st 0 <= t & t < s2 holds
not g . t in Q
A42:
(
g is
continuous &
g is
one-to-one )
by A36, TOPS_2:def 5;
reconsider SEG =
SEG as non
empty Subset of
((TOP-REAL 2) | P) ;
A43:
((TOP-REAL 2) | P) | SEG = (TOP-REAL 2) | SE
by GOBOARD9:2;
ppi in [.ppi,pi1.]
by A26, RCOMP_1:def 1;
then
ppi in (dom F) /\ Poz
by A17, A30, XBOOLE_0:def 4;
then A44:
ppi in dom hh
by A27, RELAT_1:61;
then A45:
hh . ppi = f /. i
by A24, A27, FUNCT_1:47;
A46:
dom hh = [#] (I[01] | Poz)
by A28, TOPS_2:def 5;
then A47:
dom hh = Poz
by PRE_TOPC:def 5;
A48:
rng hh =
hh .: (dom hh)
by A46, RELSET_1:22
.=
[#] (((TOP-REAL 2) | P) | SEG)
by A23, A35, A27, A47, RELAT_1:129
;
let t be
Real;
( 0 <= t & t < s2 implies not g . t in Q )
assume that A49:
0 <= t
and A50:
t < s2
;
not g . t in Q
A51:
t < 1
by A41, A50, XXREAL_0:2;
then reconsider w1 =
s2,
w2 =
t as
Point of
(Closed-Interval-TSpace (0,1)) by A40, A41, A49, BORSUK_1:43, TOPMETR:20;
A52:
(
F is
one-to-one &
rng F = [#] ((TOP-REAL 2) | P) )
by A13, TOPS_2:def 5;
set H =
(hh ") * g;
A53:
rng g = [#] ((TOP-REAL 2) | SE)
by A36, TOPS_2:def 5;
set ss =
((hh ") * g) . t;
A54:
hh is
one-to-one
by A28, TOPS_2:def 5;
A55:
hh is
one-to-one
by A28, TOPS_2:def 5;
then A56:
dom (hh ") = [#] (((TOP-REAL 2) | P) | SEG)
by A43, A48, TOPS_2:49;
then A57:
rng ((hh ") * g) = rng (hh ")
by A53, RELAT_1:28;
A58:
rng (hh ") =
[#] (I[01] | Poz)
by A43, A55, A48, TOPS_2:49
.=
Poz
by PRE_TOPC:def 5
;
then
rng ((hh ") * g) = Poz
by A53, A56, RELAT_1:28;
then A59:
rng ((hh ") * g) c= the
carrier of
(Closed-Interval-TSpace (ppi,pi1))
by A20, TOPMETR:18;
hh is
onto
by A43, A48, FUNCT_2:def 3;
then A60:
hh " = hh "
by A55, TOPS_2:def 4;
A61:
dom g =
[#] I[01]
by A36, TOPS_2:def 5
.=
the
carrier of
I[01]
;
then A62:
dom ((hh ") * g) = the
carrier of
(Closed-Interval-TSpace (0,1))
by A43, A53, A56, RELAT_1:27, TOPMETR:20;
A63:
t in dom g
by A61, A49, A51, BORSUK_1:43;
then
g . t in [#] ((TOP-REAL 2) | SE)
by A53, FUNCT_1:def 3;
then A64:
g . t in SEG
by PRE_TOPC:def 5;
then consider x being
object such that A65:
x in dom F
and A66:
x in Poz
and A67:
g . t = F . x
by A23, FUNCT_1:def 6;
A68:
F is
one-to-one
by A52;
then A69:
(F ") . (g . t) in Poz
by A65, A66, A67, FUNCT_1:32;
F is
onto
by A52, FUNCT_2:def 3;
then A70:
F " = F "
by A52, TOPS_2:def 4;
x = (F ") . (g . t)
by A68, A65, A67, FUNCT_1:32;
then
(F ") . (g . t) in Poz
by A66, A70;
then A71:
(F ") . (g . t) in dom (id Poz)
by FUNCT_1:17;
g . t in the
carrier of
((TOP-REAL 2) | P)
by A64;
then A72:
g . t in dom (F ")
by A52, TOPS_2:49;
t in dom ((hh ") * g)
by A43, A53, A63, A56, RELAT_1:27;
then A73:
F . (((hh ") * g) . t) =
(((hh ") * g) * F) . t
by FUNCT_1:13
.=
(g * ((hh ") * F)) . t
by RELAT_1:36
.=
(F * (hh ")) . (g . t)
by A63, FUNCT_1:13
.=
(F * ((F ") * ((id Poz) "))) . (g . t)
by A68, A29, A60, FUNCT_1:44
.=
(((F ") * ((id Poz) ")) * F) . (g . t)
by A70
.=
((F ") * (((id Poz) ") * F)) . (g . t)
by RELAT_1:36
.=
((F ") * (F * (id Poz))) . (g . t)
by FUNCT_1:45
.=
(F * (id Poz)) . ((F ") . (g . t))
by A72, FUNCT_1:13
.=
F . ((id Poz) . ((F ") . (g . t)))
by A71, FUNCT_1:13
.=
F . ((F ") . (g . t))
by A69, A70, FUNCT_1:17
.=
g . t
by A52, A64, FUNCT_1:35
;
1
in dom g
by A61, BORSUK_1:43;
then A74:
((hh ") * g) . 1 =
(hh ") . (f /. (i + 1))
by A38, FUNCT_1:13
.=
pi1
by A54, A33, A34, A60, FUNCT_1:32
;
0 in dom g
by A61, BORSUK_1:43;
then A75:
((hh ") * g) . 0 =
(hh ") . (f /. i)
by A37, FUNCT_1:13
.=
ppi
by A54, A44, A45, A60, FUNCT_1:32
;
dom ((hh ") * g) = dom g
by A43, A53, A56, RELAT_1:27;
then
((hh ") * g) . t in Poz
by A58, A63, A57, FUNCT_1:def 3;
then
((hh ") * g) . t in { l where l is Real : ( ppi <= l & l <= pi1 ) }
by RCOMP_1:def 1;
then consider ss9 being
Real such that A76:
ss9 = ((hh ") * g) . t
and A77:
ppi <= ss9
and
ss9 <= pi1
;
reconsider H =
(hh ") * g as
Function of
(Closed-Interval-TSpace (0,1)),
(Closed-Interval-TSpace (ppi,pi1)) by A62, A59, FUNCT_2:2;
A78:
ss9 = H . w2
by A76;
ex
z being
object st
(
z in dom F &
z in Poz &
F . s21 = F . z )
by A5, A16, A23, FUNCT_1:def 6;
then A79:
s21 in Poz
by A15, A68, FUNCT_1:def 4;
then
hh . s21 = g . s2
by A16, A39, A27, FUNCT_1:49;
then
s21 = (hh ") . (g . s2)
by A55, A47, A79, FUNCT_1:32;
then A80:
s21 = (hh ") . (g . s2)
by A60;
s2 in dom g
by A40, A41, A61, BORSUK_1:43;
then
s21 = H . w1
by A80, FUNCT_1:13;
then
ss9 < s21
by A20, A50, A75, A74, A42, A32, A31, A78, JORDAN5A:15, TOPMETR:20;
hence
not
g . t in Q
by A1, A7, A6, A13, A14, A16, A18, A21, A76, A77, A73, Def1;
verum
end;
A81:
(LSeg (f,i)) /\ Q is
closed
by A2, TOPS_1:8;
(LSeg (f,i)) /\ Q <> {}
by A5, A8, XBOOLE_0:def 4;
then A82:
LSeg (
f,
i)
meets Q
;
LSeg (
f,
i)
= LSeg (
(f /. i),
(f /. (i + 1)))
by A4, TOPREAL1:def 3;
then A83:
R is_an_arc_of f /. i,
f /. (i + 1)
by A11, TOPREAL1:9;
First_Point (
P,
(f /. 1),
(f /. (len f)),
Q)
in (LSeg (f,i)) /\ Q
by A5, A8, XBOOLE_0:def 4;
hence
First_Point (
P,
(f /. 1),
(f /. (len f)),
Q)
= First_Point (
R,
(f /. i),
(f /. (i + 1)),
Q)
by A82, A81, A83, A19, Def1;
verum
end;
hence
First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)
; verum