let f be FinSequence of (TOP-REAL 2); :: thesis: 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 & Last_Point (L~ f),(f /. 1),(f /. (len f)),Q in LSeg f,i holds
Last_Point (L~ f),(f /. 1),(f /. (len f)),Q = Last_Point (LSeg f,i),(f /. i),(f /. (i + 1)),Q
let Q be Subset of (TOP-REAL 2); :: thesis: 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 & Last_Point (L~ f),(f /. 1),(f /. (len f)),Q in LSeg f,i holds
Last_Point (L~ f),(f /. 1),(f /. (len f)),Q = Last_Point (LSeg f,i),(f /. i),(f /. (i + 1)),Q
let i be Element of NAT ; :: thesis: ( L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & Last_Point (L~ f),(f /. 1),(f /. (len f)),Q in LSeg f,i implies Last_Point (L~ f),(f /. 1),(f /. (len f)),Q = Last_Point (LSeg f,i),(f /. i),(f /. (i + 1)),Q )
A1:
L~ f is closed
by SPPOL_1:49;
assume A2:
( L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & Last_Point (L~ f),(f /. 1),(f /. (len f)),Q in LSeg f,i )
; :: thesis: Last_Point (L~ f),(f /. 1),(f /. (len f)),Q = Last_Point (LSeg f,i),(f /. i),(f /. (i + 1)),Q
then A3:
f is one-to-one
by TOPREAL1:def 10;
len f >= 2
by A2, TOPREAL1:def 10;
then reconsider P = L~ f, R = LSeg f,i as non empty Subset of (TOP-REAL 2) by A2, TOPREAL1:29;
A4:
( L~ f meets Q & (L~ f) /\ Q is closed & P is_an_arc_of f /. 1,f /. (len f) )
by A1, A2, TOPREAL1:31, TOPS_1:35;
then
Last_Point P,(f /. 1),(f /. (len f)),Q in (L~ f) /\ Q
by Def2;
then A5:
( Last_Point P,(f /. 1),(f /. (len f)),Q in L~ f & Last_Point P,(f /. 1),(f /. (len f)),Q in Q )
by XBOOLE_0:def 4;
set FPO = Last_Point R,(f /. i),(f /. (i + 1)),Q;
set FPG = Last_Point P,(f /. 1),(f /. (len f)),Q;
A6:
( i in dom f & i + 1 in dom f )
by A2, GOBOARD2:3;
A7:
f /. i <> f /. (i + 1)
Last_Point P,(f /. 1),(f /. (len f)),Q = Last_Point R,(f /. i),(f /. (i + 1)),Q
proof
A8:
LSeg f,
i is
closed
by SPPOL_1:40;
A9:
LSeg f,
i = LSeg (f /. i),
(f /. (i + 1))
by A2, TOPREAL1:def 5;
(LSeg f,i) /\ Q <> {}
by A2, A5, XBOOLE_0:def 4;
then A10:
(
LSeg f,
i meets Q &
(LSeg f,i) /\ Q is
closed &
R is_an_arc_of f /. i,
f /. (i + 1) )
by A2, A7, A8, A9, TOPREAL1:15, TOPS_1:35, XBOOLE_0:def 7;
(
Last_Point P,
(f /. 1),
(f /. (len f)),
Q in (L~ f) /\ Q & ( for
g being
Function of
I[01] ,
((TOP-REAL 2) | P) for
s2 being
Real st
g is
being_homeomorphism &
g . 0 = f /. 1 &
g . 1
= f /. (len f) &
g . s2 = Last_Point P,
(f /. 1),
(f /. (len f)),
Q &
0 <= s2 &
s2 <= 1 holds
for
t being
Real st 1
>= t &
t > s2 holds
not
g . t in Q ) )
by A4, Def2;
then A11:
Last_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 A12:
(
F is
being_homeomorphism &
F . 0 = f /. 1 &
F . 1
= f /. (len f) )
by A4, TOPREAL1:def 2;
A13:
dom F =
[#] I[01]
by A12, TOPS_2:def 5
.=
[.0 ,1.]
by BORSUK_1:83
;
rng F =
[#] ((TOP-REAL 2) | P)
by A12, TOPS_2:def 5
.=
L~ f
by PRE_TOPC:def 10
;
then consider s21 being
set such that A14:
(
s21 in dom F &
F . s21 = Last_Point P,
(f /. 1),
(f /. (len f)),
Q )
by A11, FUNCT_1:def 5;
reconsider s21 =
s21 as
Real by A13, A14;
A15:
(
0 <= s21 &
s21 <= 1 )
by A14, BORSUK_1:86;
A16:
Last_Point P,
(f /. 1),
(f /. (len f)),
Q in (LSeg f,i) /\ Q
by A2, A5, XBOOLE_0:def 4;
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 = Last_Point P,
(f /. 1),
(f /. (len f)),
Q &
0 <= s2 &
s2 <= 1 holds
for
t being
Real st 1
>= t &
t > s2 holds
not
g . t in Q
proof
let g be
Function of
I[01] ,
((TOP-REAL 2) | R);
:: thesis: for s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = Last_Point P,(f /. 1),(f /. (len f)),Q & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Qlet s2 be
Real;
:: thesis: ( g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = Last_Point P,(f /. 1),(f /. (len f)),Q & 0 <= s2 & s2 <= 1 implies for t being Real st 1 >= t & t > s2 holds
not g . t in Q )
assume A17:
(
g is
being_homeomorphism &
g . 0 = f /. i &
g . 1
= f /. (i + 1) &
g . s2 = Last_Point P,
(f /. 1),
(f /. (len f)),
Q &
0 <= s2 &
s2 <= 1 )
;
:: thesis: for t being Real st 1 >= t & t > s2 holds
not g . t in Q
consider ppi,
pi1 being
Real such that A18:
(
ppi < pi1 &
0 <= ppi &
ppi <= 1 &
0 <= pi1 &
pi1 <= 1 &
LSeg f,
i = F .: [.ppi,pi1.] &
F . ppi = f /. i &
F . pi1 = f /. (i + 1) )
by A2, A12, JORDAN5B:7;
A19:
(
ppi in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } &
pi1 in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } )
by A18;
then A20:
(
ppi in [.ppi,pi1.] &
pi1 in [.ppi,pi1.] )
by RCOMP_1:def 1;
A21:
[.ppi,pi1.] c= [.0 ,1.]
by A18, XXREAL_1:34;
reconsider Poz =
[.ppi,pi1.] as non
empty Subset of
I[01] by A18, A19, BORSUK_1:83, RCOMP_1:def 1, XXREAL_1:34;
A22: the
carrier of
(I[01] | Poz) =
[#] (I[01] | Poz)
.=
Poz
by PRE_TOPC:def 10
;
set gg =
F | Poz;
reconsider gg =
F | Poz as
Function of
(I[01] | Poz),
((TOP-REAL 2) | P) by A22, FUNCT_2:38;
reconsider Lf =
L~ f as non
empty Subset of
(TOP-REAL 2) by A4;
the
carrier of
((TOP-REAL 2) | Lf) =
[#] ((TOP-REAL 2) | Lf)
.=
Lf
by PRE_TOPC:def 10
;
then reconsider SEG =
LSeg f,
i as non
empty Subset of
((TOP-REAL 2) | Lf) by A2, TOPREAL3:26;
A23: the
carrier of
(((TOP-REAL 2) | Lf) | SEG) =
[#] (((TOP-REAL 2) | Lf) | SEG)
.=
SEG
by PRE_TOPC:def 10
;
A24:
rng gg c= SEG
reconsider SE =
SEG as non
empty Subset of
(TOP-REAL 2) ;
reconsider SEG =
SEG as non
empty Subset of
((TOP-REAL 2) | Lf) ;
A26:
((TOP-REAL 2) | Lf) | SEG = (TOP-REAL 2) | SE
by GOBOARD9:4;
reconsider hh' =
gg as
Function of
(I[01] | Poz),
(((TOP-REAL 2) | Lf) | SEG) by A23, A24, FUNCT_2:8;
A27:
(
F is
continuous &
F is
one-to-one )
by A12, TOPS_2:def 5;
then A28:
gg is
continuous
by TOPMETR:10;
A29:
hh' is
one-to-one
by A27, FUNCT_1:84;
reconsider hh =
hh' as
Function of
(I[01] | Poz),
((TOP-REAL 2) | SE) by A26;
A30:
hh is
one-to-one
by A27, FUNCT_1:84;
A31:
dom hh = [#] (I[01] | Poz)
by FUNCT_2:def 1;
then A32:
dom hh = Poz
by PRE_TOPC:def 10;
A33:
rng hh =
hh .: (dom hh)
by A31, FUNCT_2:45
.=
[#] (((TOP-REAL 2) | Lf) | SEG)
by A18, A23, A32, RELAT_1:162
;
reconsider A =
Closed-Interval-TSpace ppi,
pi1 as
strict SubSpace of
I[01] by A18, TOPMETR:27, TREAL_1:6;
A34:
Poz = [#] A
by A18, TOPMETR:25;
Closed-Interval-TSpace ppi,
pi1 is
compact
by A18, HEINE:11;
then
[#] (Closed-Interval-TSpace ppi,pi1) is
compact
by COMPTS_1:10;
then
for
P being
Subset of
A st
P = Poz holds
P is
compact
by A18, TOPMETR:25;
then
Poz is
compact
by A34, COMPTS_1:11;
then A35:
I[01] | Poz is
compact
by COMPTS_1:12;
TOP-REAL 2 is
T_2
by SPPOL_1:26;
then
(TOP-REAL 2) | SE is
T_2
by TOPMETR:3;
then A36:
hh is
being_homeomorphism
by A26, A28, A29, A31, A33, A35, COMPTS_1:26, TOPMETR:9;
A37:
rng g = [#] ((TOP-REAL 2) | SE)
by A17, TOPS_2:def 5;
A38:
rng (hh " ) =
[#] (I[01] | Poz)
by A26, A29, A33, TOPS_2:62
.=
Poz
by PRE_TOPC:def 10
;
set H =
(hh " ) * g;
A39:
hh = F * (id Poz)
by RELAT_1:94;
A40:
dom g =
[#] I[01]
by A17, TOPS_2:def 5
.=
the
carrier of
I[01]
;
let t be
Real;
:: thesis: ( 1 >= t & t > s2 implies not g . t in Q )
assume A41:
( 1
>= t &
t > s2 )
;
:: thesis: not g . t in Q
then A42:
t in dom g
by A17, A40, BORSUK_1:86;
(
ppi in (dom F) /\ Poz &
pi1 in (dom F) /\ Poz )
by A13, A20, A21, XBOOLE_0:def 4;
then A43:
(
ppi in dom hh &
pi1 in dom hh )
by RELAT_1:90;
then A44:
(
hh . ppi = f /. i &
hh . pi1 = f /. (i + 1) )
by A18, FUNCT_1:70;
0 in dom g
by A40, BORSUK_1:86;
then A45:
((hh " ) * g) . 0 =
(hh " ) . (f /. i)
by A17, FUNCT_1:23
.=
(hh " ) . (f /. i)
by A26, A30, A33, TOPS_2:def 4
.=
ppi
by A30, A43, A44, FUNCT_1:54
;
1
in dom g
by A40, BORSUK_1:86;
then A46:
((hh " ) * g) . 1 =
(hh " ) . (f /. (i + 1))
by A17, FUNCT_1:23
.=
(hh " ) . (f /. (i + 1))
by A26, A30, A33, TOPS_2:def 4
.=
pi1
by A30, A43, A44, FUNCT_1:54
;
set ss =
((hh " ) * g) . t;
A47:
dom (hh " ) = [#] (((TOP-REAL 2) | Lf) | SEG)
by A26, A29, A33, TOPS_2:62;
then A48:
(
dom ((hh " ) * g) = dom g &
rng ((hh " ) * g) = rng (hh " ) )
by A26, A37, RELAT_1:46, RELAT_1:47;
A49:
rng ((hh " ) * g) = Poz
by A37, A38, A47, RELAT_1:47;
((hh " ) * g) . t in Poz
by A38, A42, A48, 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 ss' being
Real such that A50:
(
ss' = ((hh " ) * g) . t &
ppi <= ss' &
ss' <= pi1 )
;
A51:
F is
one-to-one
by A12, TOPS_2:def 5;
A52:
rng F = [#] ((TOP-REAL 2) | P)
by A12, TOPS_2:def 5;
g . t in [#] ((TOP-REAL 2) | SE)
by A37, A42, FUNCT_1:def 5;
then A53:
g . t in SEG
by PRE_TOPC:def 10;
then A54:
g . t in the
carrier of
((TOP-REAL 2) | Lf)
;
A55:
t in dom ((hh " ) * g)
by A26, A37, A42, A47, RELAT_1:46;
A56:
g . t in dom (F " )
by A51, A52, A54, TOPS_2:62;
consider x being
set such that A57:
(
x in dom F &
x in Poz &
g . t = F . x )
by A18, A53, FUNCT_1:def 12;
x = (F " ) . (g . t)
by A27, A57, FUNCT_1:54;
then A58:
(F " ) . (g . t) in Poz
by A51, A52, A57, TOPS_2:def 4;
A59:
(F " ) . (g . t) in Poz
by A27, A57, FUNCT_1:54;
A60:
(F " ) . (g . t) in dom (id Poz)
by A58, FUNCT_1:34;
consider z being
set such that A61:
(
z in dom F &
z in Poz &
F . s21 = F . z )
by A2, A14, A18, FUNCT_1:def 12;
A62:
s21 in Poz
by A14, A27, A61, FUNCT_1:def 8;
A63:
s2 in dom g
by A17, A40, BORSUK_1:86;
hh . s21 = g . s2
by A14, A17, A62, FUNCT_1:72;
then
s21 = (hh " ) . (g . s2)
by A29, A32, A62, FUNCT_1:54;
then A64:
s21 = (hh " ) . (g . s2)
by A26, A29, A33, TOPS_2:def 4;
A65:
dom ((hh " ) * g) = the
carrier of
(Closed-Interval-TSpace 0 ,1)
by A26, A37, A40, A47, RELAT_1:46, TOPMETR:27;
rng ((hh " ) * g) c= the
carrier of
(Closed-Interval-TSpace ppi,pi1)
by A18, A49, TOPMETR:25;
then reconsider H =
(hh " ) * g as
Function of
(Closed-Interval-TSpace 0 ,1),
(Closed-Interval-TSpace ppi,pi1) by A65, FUNCT_2:4;
reconsider w1 =
s2,
w2 =
t as
Point of
(Closed-Interval-TSpace 0 ,1) by A17, A41, BORSUK_1:86, TOPMETR:27;
A66:
(
g is
continuous &
g is
one-to-one )
by A17, TOPS_2:def 5;
hh " is
being_homeomorphism
by A36, TOPS_2:70;
then A67:
(
hh " is
continuous &
hh " is
one-to-one )
by TOPS_2:def 5;
I[01] | Poz = A
by A34, PRE_TOPC:def 10;
then A68:
(
H is
continuous &
H is
one-to-one )
by A66, A67, TOPMETR:27;
(
s21 = H . w1 &
ss' = H . w2 &
t > s2 &
ppi < pi1 )
by A18, A41, A50, A63, A64, FUNCT_1:23;
then A69:
ss' > s21
by A45, A46, A68, JORDAN5A:16;
A70:
1
>= ss'
by A18, A50, XXREAL_0:2;
F . (((hh " ) * g) . t) =
(((hh " ) * g) * F) . t
by A55, FUNCT_1:23
.=
(g * ((hh " ) * F)) . t
by RELAT_1:55
.=
(F * (hh " )) . (g . t)
by A42, FUNCT_1:23
.=
(F * (hh " )) . (g . t)
by A26, A29, A33, TOPS_2:def 4
.=
(F * ((F " ) * ((id Poz) " ))) . (g . t)
by A27, A39, FUNCT_1:66
.=
(((F " ) * ((id Poz) " )) * F) . (g . t)
by A51, 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 A56, FUNCT_1:23
.=
F . ((id Poz) . ((F " ) . (g . t)))
by A60, FUNCT_1:23
.=
F . ((id Poz) . ((F " ) . (g . t)))
by A51, A52, TOPS_2:def 4
.=
F . ((F " ) . (g . t))
by A59, FUNCT_1:34
.=
g . t
by A51, A52, A53, FUNCT_1:57
;
hence
not
g . t in Q
by A4, A12, A14, A15, A50, A69, A70, Def2;
:: thesis: verum
end;
hence
Last_Point P,
(f /. 1),
(f /. (len f)),
Q = Last_Point R,
(f /. i),
(f /. (i + 1)),
Q
by A10, A16, Def2;
:: thesis: verum
end;
hence
Last_Point (L~ f),(f /. 1),(f /. (len f)),Q = Last_Point (LSeg f,i),(f /. i),(f /. (i + 1)),Q
; :: thesis: verum