let f be FinSequence of (TOP-REAL 2); for Q being Subset of (TOP-REAL 2)
for i being Element of 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 Element of 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 Element of 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 10;
then reconsider P = L~ f, R = LSeg f,i as non empty Subset of the carrier of (TOP-REAL 2) by A5, TOPREAL1:29;
A6:
P is_an_arc_of f /. 1,f /. (len f)
by A3, TOPREAL1:31;
set FPO = First_Point R,(f /. i),(f /. (i + 1)),Q;
set FPG = First_Point P,(f /. 1),(f /. (len f)),Q;
L~ f is closed
by SPPOL_1:49;
then A7:
(L~ f) /\ Q is closed
by A2, TOPS_1:35;
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, GOBOARD2:3;
A10:
( f is one-to-one & i in dom f )
by A3, A4, GOBOARD2:3, TOPREAL1:def 10;
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 2;
rng F =
[#] ((TOP-REAL 2) | P)
by A13, TOPS_2:def 5
.=
L~ f
by PRE_TOPC:def 10
;
then consider s21 being
set 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 5;
A17:
dom F =
[#] I[01]
by A13, TOPS_2:def 5
.=
[.0 ,1.]
by BORSUK_1:83
;
then reconsider s21 =
s21 as
Real by A15;
A18:
s21 <= 1
by A15, BORSUK_1:86;
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:83, 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:94;
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:27, TREAL_1:6;
Poz = [#] A
by A20, TOPMETR:25;
then A31:
I[01] | Poz = A
by PRE_TOPC:def 10;
hh " is
being_homeomorphism
by A28, TOPS_2:70;
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:90;
then A34:
hh . pi1 = f /. (i + 1)
by A25, A27, FUNCT_1:70;
the
carrier of
((TOP-REAL 2) | P) =
[#] ((TOP-REAL 2) | P)
.=
P
by PRE_TOPC:def 10
;
then reconsider SEG =
LSeg f,
i as non
empty Subset of the
carrier of
((TOP-REAL 2) | P) by A5, TOPREAL3:26;
A35: the
carrier of
(((TOP-REAL 2) | P) | SEG) =
[#] (((TOP-REAL 2) | P) | SEG)
.=
SEG
by PRE_TOPC:def 10
;
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:4;
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:90;
then A45:
hh . ppi = f /. i
by A24, A27, FUNCT_1:70;
A46:
dom hh = [#] (I[01] | Poz)
by A28, TOPS_2:def 5;
then A47:
dom hh = Poz
by PRE_TOPC:def 10;
A48:
rng hh =
hh .: (dom hh)
by A46, FUNCT_2:45
.=
[#] (((TOP-REAL 2) | P) | SEG)
by A23, A35, A27, A47, RELAT_1:162
;
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:86, TOPMETR:27;
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:62;
then A57:
rng ((hh " ) * g) = rng (hh " )
by A53, RELAT_1:47;
A58:
rng (hh " ) =
[#] (I[01] | Poz)
by A43, A55, A48, TOPS_2:62
.=
Poz
by PRE_TOPC:def 10
;
then
rng ((hh " ) * g) = Poz
by A53, A56, RELAT_1:47;
then A59:
rng ((hh " ) * g) c= the
carrier of
(Closed-Interval-TSpace ppi,pi1)
by A20, TOPMETR:25;
A60:
dom g =
[#] I[01]
by A36, TOPS_2:def 5
.=
the
carrier of
I[01]
;
then A61:
dom ((hh " ) * g) = the
carrier of
(Closed-Interval-TSpace 0 ,1)
by A43, A53, A56, RELAT_1:46, TOPMETR:27;
A62:
t in dom g
by A60, A49, A51, BORSUK_1:86;
then
g . t in [#] ((TOP-REAL 2) | SE)
by A53, FUNCT_1:def 5;
then A63:
g . t in SEG
by PRE_TOPC:def 10;
then consider x being
set such that A64:
x in dom F
and A65:
x in Poz
and A66:
g . t = F . x
by A23, FUNCT_1:def 12;
A67:
F is
one-to-one
by A13, TOPS_2:def 5;
then A68:
(F " ) . (g . t) in Poz
by A64, A65, A66, FUNCT_1:54;
x = (F " ) . (g . t)
by A67, A64, A66, FUNCT_1:54;
then
(F " ) . (g . t) in Poz
by A52, A65, TOPS_2:def 4;
then A69:
(F " ) . (g . t) in dom (id Poz)
by FUNCT_1:34;
g . t in the
carrier of
((TOP-REAL 2) | P)
by A63;
then A70:
g . t in dom (F " )
by A52, TOPS_2:62;
t in dom ((hh " ) * g)
by A43, A53, A62, A56, RELAT_1:46;
then A71:
F . (((hh " ) * g) . t) =
(((hh " ) * g) * F) . t
by FUNCT_1:23
.=
(g * ((hh " ) * F)) . t
by RELAT_1:55
.=
(F * (hh " )) . (g . t)
by A62, FUNCT_1:23
.=
(F * (hh " )) . (g . t)
by A43, A55, A48, TOPS_2:def 4
.=
(F * ((F " ) * ((id Poz) " ))) . (g . t)
by A67, A29, FUNCT_1:66
.=
(((F " ) * ((id Poz) " )) * F) . (g . t)
by A52, TOPS_2:def 4
.=
((F " ) * (((id Poz) " ) * F)) . (g . t)
by RELAT_1:55
.=
((F " ) * (F * (id Poz))) . (g . t)
by FUNCT_1:67
.=
(F * (id Poz)) . ((F " ) . (g . t))
by A70, FUNCT_1:23
.=
F . ((id Poz) . ((F " ) . (g . t)))
by A69, FUNCT_1:23
.=
F . ((id Poz) . ((F " ) . (g . t)))
by A52, TOPS_2:def 4
.=
F . ((F " ) . (g . t))
by A68, FUNCT_1:34
.=
g . t
by A52, A63, FUNCT_1:57
;
1
in dom g
by A60, BORSUK_1:86;
then A72:
((hh " ) * g) . 1 =
(hh " ) . (f /. (i + 1))
by A38, FUNCT_1:23
.=
(hh " ) . (f /. (i + 1))
by A43, A54, A48, TOPS_2:def 4
.=
pi1
by A54, A33, A34, FUNCT_1:54
;
0 in dom g
by A60, BORSUK_1:86;
then A73:
((hh " ) * g) . 0 =
(hh " ) . (f /. i)
by A37, FUNCT_1:23
.=
(hh " ) . (f /. i)
by A43, A54, A48, TOPS_2:def 4
.=
ppi
by A54, A44, A45, FUNCT_1:54
;
dom ((hh " ) * g) = dom g
by A43, A53, A56, RELAT_1:46;
then
((hh " ) * g) . t in Poz
by A58, A62, A57, FUNCT_1:def 5;
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 A74:
ss9 = ((hh " ) * g) . t
and A75:
ppi <= ss9
and
ss9 <= pi1
;
reconsider H =
(hh " ) * g as
Function of
(Closed-Interval-TSpace 0 ,1),
(Closed-Interval-TSpace ppi,pi1) by A61, A59, FUNCT_2:4;
A76:
ss9 = H . w2
by A74;
ex
z being
set st
(
z in dom F &
z in Poz &
F . s21 = F . z )
by A5, A16, A23, FUNCT_1:def 12;
then A77:
s21 in Poz
by A15, A67, FUNCT_1:def 8;
then
hh . s21 = g . s2
by A16, A39, A27, FUNCT_1:72;
then
s21 = (hh " ) . (g . s2)
by A55, A47, A77, FUNCT_1:54;
then A78:
s21 = (hh " ) . (g . s2)
by A43, A55, A48, TOPS_2:def 4;
s2 in dom g
by A40, A41, A60, BORSUK_1:86;
then
s21 = H . w1
by A78, FUNCT_1:23;
then
ss9 < s21
by A20, A50, A73, A72, A42, A32, A31, A76, JORDAN5A:16, TOPMETR:27;
hence
not
g . t in Q
by A1, A7, A6, A13, A14, A16, A18, A21, A74, A75, A71, Def1;
verum
end;
LSeg f,
i is
closed
by SPPOL_1:40;
then A79:
(LSeg f,i) /\ Q is
closed
by A2, TOPS_1:35;
(LSeg f,i) /\ Q <> {}
by A5, A8, XBOOLE_0:def 4;
then A80:
LSeg f,
i meets Q
by XBOOLE_0:def 7;
LSeg f,
i = LSeg (f /. i),
(f /. (i + 1))
by A4, TOPREAL1:def 5;
then A81:
R is_an_arc_of f /. i,
f /. (i + 1)
by A11, TOPREAL1:15;
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 A80, A79, A81, 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