let P be non empty Subset of (TOP-REAL 2); for p1, p2, p being Point of (TOP-REAL 2)
for e being Real st P is_S-P_arc_joining p1,p2 & p1 `1 < e & p in P & p `1 = e & not p is_Lin P,p1,p2,e holds
p is_Rin P,p1,p2,e
let p1, p2, p be Point of (TOP-REAL 2); for e being Real st P is_S-P_arc_joining p1,p2 & p1 `1 < e & p in P & p `1 = e & not p is_Lin P,p1,p2,e holds
p is_Rin P,p1,p2,e
let e be Real; ( P is_S-P_arc_joining p1,p2 & p1 `1 < e & p in P & p `1 = e & not p is_Lin P,p1,p2,e implies p is_Rin P,p1,p2,e )
assume that
A1:
P is_S-P_arc_joining p1,p2
and
A2:
p1 `1 < e
and
A3:
p in P
and
A4:
p `1 = e
; ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )
consider f being FinSequence of (TOP-REAL 2) such that
A5:
f is being_S-Seq
and
A6:
P = L~ f
and
A7:
p1 = f /. 1
and
A8:
p2 = f /. (len f)
by A1, TOPREAL4:def 1;
A9:
P is_an_arc_of p1,p2
by A1, TOPREAL4:2;
len f >= 2
by A5, TOPREAL1:def 8;
then A10:
len f > 1
by XXREAL_0:2;
A11:
L~ f = union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
by TOPREAL1:def 4;
then consider Y being set such that
A12:
p in Y
and
A13:
Y in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
by A3, A6, TARSKI:def 4;
consider i being Nat such that
A14:
Y = LSeg (f,i)
and
A15:
1 <= i
and
A16:
i + 1 <= len f
by A13;
A17:
i - 1 >= 0
by A15, XREAL_1:48;
A18:
1 < i + 1
by A15, NAT_1:13;
A19:
Y c= L~ f
by A11, A13, TARSKI:def 4;
defpred S1[ Nat] means for p being Point of (TOP-REAL 2) st p = f . (i -' $1) holds
p `1 <> e;
A20:
i < len f
by A16, NAT_1:13;
then A21:
i in dom f
by A15, FINSEQ_3:25;
A22:
1 < len f
by A15, A20, XXREAL_0:2;
then
1 in dom f
by FINSEQ_3:25;
then
f /. 1 = f . 1
by PARTFUN1:def 6;
then A23:
S1[i -' 1]
by A2, A7, A15, NAT_D:58;
then A24:
ex k being Nat st S1[k]
;
ex k being Nat st
( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) )
from NAT_1:sch 5(A24);
then consider k being Nat such that
A25:
S1[k]
and
A26:
for n being Nat st S1[n] holds
k <= n
;
k <= i -' 1
by A23, A26;
then
k <= i - 1
by A17, XREAL_0:def 2;
then
k + 1 <= (i - 1) + 1
by XREAL_1:7;
then A27:
(1 + k) - k <= i - k
by XREAL_1:9;
then A28:
i -' k >= 1
by XREAL_0:def 2;
i -' k <= i
by NAT_D:35;
then A29:
i -' k < len f
by A20, XXREAL_0:2;
then A30:
i -' k in dom f
by A28, FINSEQ_3:25;
then A31:
f /. (i -' k) = f . (i -' k)
by PARTFUN1:def 6;
then reconsider pk = f . (i -' k) as Point of (TOP-REAL 2) ;
A32:
i -' k = i - k
by A27, XREAL_0:def 2;
now ( ( pk `1 < e & ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) ) or ( pk `1 > e & ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) ) )per cases
( pk `1 < e or pk `1 > e )
by A25, XXREAL_0:1;
case A33:
pk `1 < e
;
( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )now ( ( k = 0 & ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) ) or ( k <> 0 & ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) ) )per cases
( k = 0 or k <> 0 )
;
case A34:
k = 0
;
( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )set p44 =
f /. i;
A35:
pk =
f . i
by A34, NAT_D:40
.=
f /. i
by A21, PARTFUN1:def 6
;
reconsider ia =
i + 1 as
Nat ;
reconsider g =
mid (
f,
i,
(len f)) as
FinSequence of
(TOP-REAL 2) ;
A36:
i <= len f
by A16, NAT_1:13;
ia in Seg (len f)
by A16, A18, FINSEQ_1:1;
then A37:
i + 1
in dom f
by FINSEQ_1:def 3;
1
+ (1 + i) <= 1
+ (len f)
by A16, XREAL_1:7;
then A38:
((1 + 1) + i) - i <= ((len f) + 1) - i
by XREAL_1:9;
then A39:
1
<= ((len f) + 1) - i
by XXREAL_0:2;
A40:
(len f) - i > 0
by A20, XREAL_1:50;
then
(len f) -' i = (len f) - i
by XREAL_0:def 2;
then A41:
((len f) -' i) + 1
> 0 + 1
by A40, XREAL_1:8;
A42:
len g = ((len f) -' i) + 1
by A10, A15, A20, FINSEQ_6:118;
then A43:
1
+ 1
<= len g
by A41, NAT_1:13;
then
1
+ 1
in Seg (len g)
by FINSEQ_1:1;
then
1
+ 1
in dom g
by FINSEQ_1:def 3;
then A44:
g /. (1 + 1) =
g . (1 + 1)
by PARTFUN1:def 6
.=
f . (((1 + 1) - 1) + i)
by A15, A20, A38, FINSEQ_6:122
.=
f /. (i + 1)
by A37, PARTFUN1:def 6
;
1
in dom g
by A42, A41, FINSEQ_3:25;
then A45:
g /. 1 =
g . 1
by PARTFUN1:def 6
.=
f . ((1 - 1) + i)
by A15, A36, A39, FINSEQ_6:122
.=
f /. i
by A21, PARTFUN1:def 6
;
LSeg (
f,
i) =
LSeg (
(f /. i),
(f /. (i + 1)))
by A15, A16, TOPREAL1:def 3
.=
LSeg (
g,1)
by A43, A45, A44, TOPREAL1:def 3
;
then
Y in { (LSeg (g,i2)) where i2 is Nat : ( 1 <= i2 & i2 + 1 <= len g ) }
by A14, A43;
then
p in union { (LSeg (g,i2)) where i2 is Nat : ( 1 <= i2 & i2 + 1 <= len g ) }
by A12, TARSKI:def 4;
then A46:
p in L~ (mid (f,i,(len f)))
by TOPREAL1:def 4;
A47:
LSeg (
f,
i)
= LSeg (
(f /. i),
(f /. (i + 1)))
by A15, A16, TOPREAL1:def 3;
A48:
for
p5 being
Point of
(TOP-REAL 2) st
LE f /. i,
p5,
P,
p1,
p2 &
LE p5,
p,
P,
p1,
p2 holds
p5 `1 <= e
proof
f /. i in LSeg (
(f /. i),
(f /. (i + 1)))
by RLTOPSP1:68;
then
LSeg (
(f /. i),
p)
c= LSeg (
f,
i)
by A12, A14, A47, TOPREAL1:6;
then A49:
LSeg (
(f /. i),
p)
c= P
by A6, A19, A14;
let p5 be
Point of
(TOP-REAL 2);
( LE f /. i,p5,P,p1,p2 & LE p5,p,P,p1,p2 implies p5 `1 <= e )
A50:
Segment (
P,
p1,
p2,
(f /. i),
p)
= { p8 where p8 is Point of (TOP-REAL 2) : ( LE f /. i,p8,P,p1,p2 & LE p8,p,P,p1,p2 ) }
by JORDAN6:26;
assume
(
LE f /. i,
p5,
P,
p1,
p2 &
LE p5,
p,
P,
p1,
p2 )
;
p5 `1 <= e
then A51:
p5 in Segment (
P,
p1,
p2,
(f /. i),
p)
by A50;
now ( ( f /. i <> p & p5 `1 <= e ) or ( f /. i = p & p5 `1 <= e ) )per cases
( f /. i <> p or f /. i = p )
;
case
f /. i <> p
;
p5 `1 <= ethen
LSeg (
(f /. i),
p)
is_an_arc_of f /. i,
p
by TOPREAL1:9;
then
Segment (
P,
p1,
p2,
(f /. i),
p)
= LSeg (
(f /. i),
p)
by A9, A5, A6, A7, A8, A15, A20, A46, A49, Th25, SPRECT_4:3;
hence
p5 `1 <= e
by A4, A33, A35, A51, TOPREAL1:3;
verum end;
hence
p5 `1 <= e
;
verum
end;
LE f /. i,
p,
P,
p1,
p2
by A5, A6, A7, A8, A15, A20, A46, SPRECT_4:3;
hence
(
p is_Lin P,
p1,
p2,
e or
p is_Rin P,
p1,
p2,
e )
by A3, A4, A9, A33, A35, A48;
verum end; case A52:
k <> 0
;
( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )reconsider ia =
i + 1 as
Nat ;
reconsider g =
mid (
f,
i,
(len f)) as
FinSequence of
(TOP-REAL 2) ;
A53:
i <= len f
by A16, NAT_1:13;
ia in Seg (len f)
by A16, A18, FINSEQ_1:1;
then A54:
i + 1
in dom f
by FINSEQ_1:def 3;
1
+ (1 + i) <= 1
+ (len f)
by A16, XREAL_1:7;
then A55:
((1 + 1) + i) - i <= ((len f) + 1) - i
by XREAL_1:9;
then A56:
1
<= ((len f) + 1) - i
by XXREAL_0:2;
A57:
(len f) - i > 0
by A20, XREAL_1:50;
then
(len f) -' i = (len f) - i
by XREAL_0:def 2;
then A58:
((len f) -' i) + 1
> 0 + 1
by A57, XREAL_1:8;
A59:
len g = ((len f) -' i) + 1
by A10, A15, A20, FINSEQ_6:118;
then A60:
1
+ 1
<= len g
by A58, NAT_1:13;
then
1
+ 1
in Seg (len g)
by FINSEQ_1:1;
then
1
+ 1
in dom g
by FINSEQ_1:def 3;
then A61:
g /. (1 + 1) =
g . (1 + 1)
by PARTFUN1:def 6
.=
f . (((1 + 1) - 1) + i)
by A15, A20, A55, FINSEQ_6:122
.=
f /. (i + 1)
by A54, PARTFUN1:def 6
;
1
in dom g
by A59, A58, FINSEQ_3:25;
then A62:
g /. 1 =
g . 1
by PARTFUN1:def 6
.=
f . ((1 - 1) + i)
by A15, A53, A56, FINSEQ_6:122
.=
f /. i
by A21, PARTFUN1:def 6
;
LSeg (
f,
i) =
LSeg (
(f /. i),
(f /. (i + 1)))
by A15, A16, TOPREAL1:def 3
.=
LSeg (
g,1)
by A60, A62, A61, TOPREAL1:def 3
;
then
Y in { (LSeg (g,i2)) where i2 is Nat : ( 1 <= i2 & i2 + 1 <= len g ) }
by A14, A60;
then
p in union { (LSeg (g,i2)) where i2 is Nat : ( 1 <= i2 & i2 + 1 <= len g ) }
by A12, TARSKI:def 4;
then A63:
p in L~ (mid (f,i,(len f)))
by TOPREAL1:def 4;
reconsider g =
mid (
f,1,
i) as
FinSequence of
(TOP-REAL 2) ;
set p44 =
f /. i;
A64:
(
i <= len f & 1
<= i -' k )
by A16, A27, NAT_1:13, XREAL_0:def 2;
A65:
k >= 0 + 1
by A52, NAT_1:13;
then A66:
i -' k <= (i + 1) - 1
by A28, NAT_D:51;
A67:
i > i -' k
by A28, A65, NAT_D:51;
then A68:
i > 1
by A28, XXREAL_0:2;
then
i - 1
> 0
by XREAL_1:50;
then A69:
i -' 1
= i - 1
by XREAL_0:def 2;
A72:
now for p51 being Point of (TOP-REAL 2) st LE pk,p51,P,p1,p2 & LE p51,f /. i,P,p1,p2 holds
p51 `1 <= eassume
ex
p51 being
Point of
(TOP-REAL 2) st
(
LE pk,
p51,
P,
p1,
p2 &
LE p51,
f /. i,
P,
p1,
p2 & not
p51 `1 <= e )
;
contradictionthen consider p51 being
Point of
(TOP-REAL 2) such that A73:
LE pk,
p51,
P,
p1,
p2
and A74:
LE p51,
f /. i,
P,
p1,
p2
and A75:
p51 `1 > e
;
p51 in P
by A73, JORDAN5C:def 3;
then consider Y3 being
set such that A76:
p51 in Y3
and A77:
Y3 in { (LSeg (f,i5)) where i5 is Nat : ( 1 <= i5 & i5 + 1 <= len f ) }
by A6, A11, TARSKI:def 4;
consider kk being
Nat such that A78:
Y3 = LSeg (
f,
kk)
and A79:
1
<= kk
and A80:
kk + 1
<= len f
by A77;
A81:
LSeg (
f,
kk)
= LSeg (
(f /. kk),
(f /. (kk + 1)))
by A79, A80, TOPREAL1:def 3;
1
< kk + 1
by A79, NAT_1:13;
then
kk + 1
in Seg (len f)
by A80, FINSEQ_1:1;
then A82:
kk + 1
in dom f
by FINSEQ_1:def 3;
A83:
kk < len f
by A80, NAT_1:13;
then
kk in Seg (len f)
by A79, FINSEQ_1:1;
then A84:
kk in dom f
by FINSEQ_1:def 3;
A85:
LE p51,
f /. (kk + 1),
L~ f,
f /. 1,
f /. (len f)
by A5, A76, A78, A79, A80, JORDAN5C:26;
now ( ( (f /. kk) `1 > e & contradiction ) or ( (f /. (kk + 1)) `1 > e & (f /. kk) `1 <= e & contradiction ) )per cases
( (f /. kk) `1 > e or ( (f /. (kk + 1)) `1 > e & (f /. kk) `1 <= e ) )
by A75, A76, A78, A81, Th2;
case A86:
(f /. kk) `1 > e
;
contradictionA87:
LSeg (
(f /. kk),
(f /. (kk + 1)))
c= L~ f
f is
special
by A5, TOPREAL1:def 8;
then A89:
(
(f /. kk) `1 = (f /. (kk + 1)) `1 or
(f /. kk) `2 = (f /. (kk + 1)) `2 )
by A79, A80, TOPREAL1:def 5;
(
f is
one-to-one &
kk < kk + 1 )
by A5, NAT_1:13, TOPREAL1:def 8;
then A90:
f . kk <> f . (kk + 1)
by A84, A82, FUNCT_1:def 4;
A91:
LE f /. (i -' k),
p51,
L~ f,
f /. 1,
f /. (len f)
by A6, A7, A8, A30, A73, PARTFUN1:def 6;
A92:
LE f /. (i -' k),
f /. (kk + 1),
L~ f,
f /. 1,
f /. (len f)
by A6, A7, A8, A31, A73, A85, JORDAN5C:13;
set k2 =
i -' kk;
LE f /. kk,
p51,
L~ f,
f /. 1,
f /. (len f)
by A5, A76, A78, A79, A80, JORDAN5C:25;
then A93:
LE f /. kk,
f /. i,
L~ f,
f /. 1,
f /. (len f)
by A6, A7, A8, A74, JORDAN5C:13;
now not i - kk <= 0 assume
i - kk <= 0
;
contradictionthen
(i - kk) + kk <= 0 + kk
by XREAL_1:7;
then
LE f /. i,
f /. kk,
L~ f,
f /. 1,
f /. (len f)
by A5, A68, A83, JORDAN5C:24;
hence
contradiction
by A1, A6, A7, A8, A70, A86, A93, JORDAN5C:12, TOPREAL4:2;
verum end; then A94:
i -' kk = i - kk
by XREAL_0:def 2;
then A95:
i - (i -' kk) = i -' (i -' kk)
by XREAL_0:def 2;
i - (i -' kk) > 0
by A79, A94;
then
i -' (i -' kk) > 0
by XREAL_0:def 2;
then
i -' (i -' kk) >= 0 + 1
by NAT_1:13;
then
S1[
i -' kk]
by A20, A86, A94, A95, FINSEQ_4:15, NAT_D:50;
then
i -' kk >= k
by A26;
then
i - (i -' kk) <= i - k
by XREAL_1:10;
then A96:
LE f /. (i -' (i -' kk)),
f /. (i -' k),
L~ f,
f /. 1,
f /. (len f)
by A5, A29, A32, A79, A94, A95, JORDAN5C:24;
(
f /. kk = f . kk &
f /. (kk + 1) = f . (kk + 1) )
by A84, A82, PARTFUN1:def 6;
then
LSeg (
(f /. kk),
(f /. (kk + 1)))
is_an_arc_of f /. kk,
f /. (kk + 1)
by A90, TOPREAL1:9;
then A97:
Segment (
(L~ f),
(f /. 1),
(f /. (len f)),
(f /. kk),
(f /. (kk + 1)))
= LSeg (
(f /. kk),
(f /. (kk + 1)))
by A9, A6, A7, A8, A94, A95, A96, A92, A87, Th25, JORDAN5C:13;
Segment (
(L~ f),
(f /. 1),
(f /. (len f)),
(f /. kk),
(f /. (kk + 1)))
= { p8 where p8 is Point of (TOP-REAL 2) : ( LE f /. kk,p8, L~ f,f /. 1,f /. (len f) & LE p8,f /. (kk + 1), L~ f,f /. 1,f /. (len f) ) }
by JORDAN6:26;
then A98:
f /. (i -' k) in Segment (
(L~ f),
(f /. 1),
(f /. (len f)),
(f /. kk),
(f /. (kk + 1)))
by A94, A95, A96, A92;
then
(f /. (kk + 1)) `1 < e
by A31, A33, A86, A97, Th3;
then
(f /. kk) `1 > (f /. (kk + 1)) `1
by A86, XXREAL_0:2;
then
(f /. (i -' k)) `1 >= p51 `1
by A5, A76, A78, A79, A83, A81, A91, A98, A97, A89, Th6;
hence
contradiction
by A31, A33, A75, XXREAL_0:2;
verum end; case A99:
(
(f /. (kk + 1)) `1 > e &
(f /. kk) `1 <= e )
;
contradictionset k2 =
(i -' kk) -' 1;
A100:
LSeg (
(f /. kk),
(f /. (kk + 1)))
c= L~ f
(
f is
one-to-one &
kk < kk + 1 )
by A5, NAT_1:13, TOPREAL1:def 8;
then A102:
f . kk <> f . (kk + 1)
by A84, A82, FUNCT_1:def 4;
A103:
(f /. kk) `1 < (f /. (kk + 1)) `1
by A99, XXREAL_0:2;
LE f /. kk,
p51,
L~ f,
f /. 1,
f /. (len f)
by A5, A76, A78, A79, A80, JORDAN5C:25;
then A104:
LE f /. kk,
f /. i,
L~ f,
f /. 1,
f /. (len f)
by A6, A7, A8, A74, JORDAN5C:13;
(
f /. kk = f . kk &
f /. (kk + 1) = f . (kk + 1) )
by A84, A82, PARTFUN1:def 6;
then
LSeg (
(f /. kk),
(f /. (kk + 1)))
is_an_arc_of f /. kk,
f /. (kk + 1)
by A102, TOPREAL1:9;
then A105:
(
Segment (
(L~ f),
(f /. 1),
(f /. (len f)),
(f /. kk),
(f /. (kk + 1)))
= { p8 where p8 is Point of (TOP-REAL 2) : ( LE f /. kk,p8, L~ f,f /. 1,f /. (len f) & LE p8,f /. (kk + 1), L~ f,f /. 1,f /. (len f) ) } &
Segment (
(L~ f),
(f /. 1),
(f /. (len f)),
(f /. kk),
(f /. (kk + 1)))
= LSeg (
(f /. kk),
(f /. (kk + 1))) )
by A9, A5, A6, A7, A8, A79, A80, A100, Th25, JORDAN5C:23, JORDAN6:26;
A106:
now not (i - kk) - 1 <= 0 assume
(i - kk) - 1
<= 0
;
contradictionthen
(i - (kk + 1)) + (kk + 1) <= 0 + (kk + 1)
by XREAL_1:7;
then
LE f /. i,
f /. (kk + 1),
L~ f,
f /. 1,
f /. (len f)
by A5, A68, A80, JORDAN5C:24;
then A107:
f /. i in LSeg (
(f /. kk),
(f /. (kk + 1)))
by A105, A104;
f is
special
by A5, TOPREAL1:def 8;
then A108:
(
(f /. kk) `1 = (f /. (kk + 1)) `1 or
(f /. kk) `2 = (f /. (kk + 1)) `2 )
by A79, A80, TOPREAL1:def 5;
LSeg (
f,
kk)
= LSeg (
(f /. kk),
(f /. (kk + 1)))
by A79, A80, TOPREAL1:def 3;
hence
contradiction
by A5, A6, A7, A8, A70, A74, A75, A76, A78, A79, A83, A103, A107, A108, Th7;
verum end; then
((i - kk) - 1) + 1
>= 0 + 1
by XREAL_1:7;
then
i -' kk = i - kk
by XREAL_0:def 2;
then A109:
i - ((i -' kk) -' 1) =
i - ((i - kk) - 1)
by A106, XREAL_0:def 2
.=
kk + 1
;
then
i -' ((i -' kk) -' 1) > 0
by XREAL_0:def 2;
then A110:
i -' ((i -' kk) -' 1) >= 0 + 1
by NAT_1:13;
A111:
i - ((i -' kk) -' 1) = i -' ((i -' kk) -' 1)
by A109, XREAL_0:def 2;
then
S1[
(i -' kk) -' 1]
by A20, A99, A109, A110, FINSEQ_4:15, NAT_D:50;
then
(i -' kk) -' 1
>= k
by A26;
then
i - ((i -' kk) -' 1) <= i - k
by XREAL_1:10;
then A112:
LE f /. (kk + 1),
f /. (i -' k),
L~ f,
f /. 1,
f /. (len f)
by A5, A29, A32, A109, A111, A110, JORDAN5C:24;
LE f /. (i -' k),
f /. (kk + 1),
L~ f,
f /. 1,
f /. (len f)
by A6, A7, A8, A31, A73, A85, JORDAN5C:13;
hence
contradiction
by A1, A6, A7, A8, A31, A33, A99, A112, JORDAN5C:12, TOPREAL4:2;
verum end; hence
contradiction
;
verum end; A113:
LSeg (
f,
i)
= LSeg (
(f /. i),
(f /. (i + 1)))
by A15, A16, TOPREAL1:def 3;
A114:
for
p5 being
Point of
(TOP-REAL 2) st
LE f /. i,
p5,
P,
p1,
p2 &
LE p5,
p,
P,
p1,
p2 holds
p5 `1 <= e
proof
let p5 be
Point of
(TOP-REAL 2);
( LE f /. i,p5,P,p1,p2 & LE p5,p,P,p1,p2 implies p5 `1 <= e )
A115:
Segment (
P,
p1,
p2,
(f /. i),
p)
= { p8 where p8 is Point of (TOP-REAL 2) : ( LE f /. i,p8,P,p1,p2 & LE p8,p,P,p1,p2 ) }
by JORDAN6:26;
assume
(
LE f /. i,
p5,
P,
p1,
p2 &
LE p5,
p,
P,
p1,
p2 )
;
p5 `1 <= e
then A116:
p5 in Segment (
P,
p1,
p2,
(f /. i),
p)
by A115;
f /. i in LSeg (
(f /. i),
(f /. (i + 1)))
by RLTOPSP1:68;
then
LSeg (
(f /. i),
p)
c= LSeg (
f,
i)
by A12, A14, A113, TOPREAL1:6;
then A117:
LSeg (
(f /. i),
p)
c= P
by A6, A19, A14;
now ( ( f /. i <> p & p5 `1 <= e ) or ( f /. i = p & p5 `1 <= e ) )per cases
( f /. i <> p or f /. i = p )
;
case
f /. i <> p
;
p5 `1 <= ethen
LSeg (
(f /. i),
p)
is_an_arc_of f /. i,
p
by TOPREAL1:9;
then
Segment (
P,
p1,
p2,
(f /. i),
p)
= LSeg (
(f /. i),
p)
by A9, A5, A6, A7, A8, A15, A20, A63, A117, Th25, SPRECT_4:3;
hence
p5 `1 <= e
by A4, A70, A116, TOPREAL1:3;
verum end;
hence
p5 `1 <= e
;
verum
end; A118:
len g = (i -' 1) + 1
by A15, A20, A22, FINSEQ_6:118;
then
(i -' k) + 1
<= len g
by A67, A69, NAT_1:13;
then A119:
LSeg (
g,
(i -' k))
= LSeg (
(g /. (i -' k)),
(g /. ((i -' k) + 1)))
by A28, TOPREAL1:def 3;
i -' k < i
by A28, A65, NAT_D:51;
then
i -' k in Seg (len g)
by A28, A118, A69, FINSEQ_1:1;
then
i -' k in dom g
by FINSEQ_1:def 3;
then g /. (i -' k) =
g . (i -' k)
by PARTFUN1:def 6
.=
f . (((i -' k) - 1) + 1)
by A15, A64, A66, FINSEQ_6:122
.=
f /. (i -' k)
by A30, PARTFUN1:def 6
;
then A120:
pk in LSeg (
g,
(i -' k))
by A31, A119, RLTOPSP1:68;
A121:
(i -' k) + 1
<= i
by A67, NAT_1:13;
1
<= i -' k
by A27, XREAL_0:def 2;
then
LSeg (
g,
(i -' k))
in { (LSeg (g,i2)) where i2 is Nat : ( 1 <= i2 & i2 + 1 <= len g ) }
by A118, A69, A121;
then
pk in union { (LSeg (g,i2)) where i2 is Nat : ( 1 <= i2 & i2 + 1 <= len g ) }
by A120, TARSKI:def 4;
then
pk in L~ (mid (f,1,i))
by TOPREAL1:def 4;
then A122:
LE pk,
f /. i,
P,
p1,
p2
by A5, A6, A7, A8, A20, A68, SPRECT_3:17;
then A123:
f /. i in P
by JORDAN5C:def 3;
A124:
for
p5 being
Point of
(TOP-REAL 2) st
LE pk,
p5,
P,
p1,
p2 &
LE p5,
p,
P,
p1,
p2 holds
p5 `1 <= e
proof
let p5 be
Point of
(TOP-REAL 2);
( LE pk,p5,P,p1,p2 & LE p5,p,P,p1,p2 implies p5 `1 <= e )
assume that A125:
LE pk,
p5,
P,
p1,
p2
and A126:
LE p5,
p,
P,
p1,
p2
;
p5 `1 <= e
A127:
p5 in P
by A125, JORDAN5C:def 3;
now ( ( LE p5,f /. i,P,p1,p2 & p5 `1 <= e ) or ( LE f /. i,p5,P,p1,p2 & p5 `1 <= e ) )per cases
( LE p5,f /. i,P,p1,p2 or LE f /. i,p5,P,p1,p2 )
by A1, A123, A127, Th19, TOPREAL4:2;
end;
hence
p5 `1 <= e
;
verum
end;
LE f /. i,
p,
P,
p1,
p2
by A5, A6, A7, A8, A15, A20, A63, SPRECT_4:3;
then
LE pk,
p,
P,
p1,
p2
by A122, JORDAN5C:13;
hence
(
p is_Lin P,
p1,
p2,
e or
p is_Rin P,
p1,
p2,
e )
by A3, A4, A9, A33, A124;
verum end; hence
(
p is_Lin P,
p1,
p2,
e or
p is_Rin P,
p1,
p2,
e )
;
verum case A128:
pk `1 > e
;
( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )now ( ( k = 0 & ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) ) or ( k <> 0 & ( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e ) ) )per cases
( k = 0 or k <> 0 )
;
case A129:
k = 0
;
( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )set p44 =
f /. i;
A130:
pk =
f . i
by A129, NAT_D:40
.=
f /. i
by A21, PARTFUN1:def 6
;
reconsider ia =
i + 1 as
Nat ;
reconsider g =
mid (
f,
i,
(len f)) as
FinSequence of
(TOP-REAL 2) ;
A131:
i <= len f
by A16, NAT_1:13;
ia in Seg (len f)
by A16, A18, FINSEQ_1:1;
then A132:
i + 1
in dom f
by FINSEQ_1:def 3;
1
+ (1 + i) <= 1
+ (len f)
by A16, XREAL_1:7;
then A133:
((1 + 1) + i) - i <= ((len f) + 1) - i
by XREAL_1:9;
then A134:
1
<= ((len f) + 1) - i
by XXREAL_0:2;
A135:
(len f) - i > 0
by A20, XREAL_1:50;
then
(len f) -' i = (len f) - i
by XREAL_0:def 2;
then A136:
((len f) -' i) + 1
> 0 + 1
by A135, XREAL_1:8;
A137:
len g = ((len f) -' i) + 1
by A10, A15, A20, FINSEQ_6:118;
then A138:
1
+ 1
<= len g
by A136, NAT_1:13;
then
1
+ 1
in Seg (len g)
by FINSEQ_1:1;
then
1
+ 1
in dom g
by FINSEQ_1:def 3;
then A139:
g /. (1 + 1) =
g . (1 + 1)
by PARTFUN1:def 6
.=
f . (((1 + 1) - 1) + i)
by A15, A20, A133, FINSEQ_6:122
.=
f /. (i + 1)
by A132, PARTFUN1:def 6
;
1
in Seg (len g)
by A137, A136, FINSEQ_1:1;
then
1
in dom g
by FINSEQ_1:def 3;
then A140:
g /. 1 =
g . 1
by PARTFUN1:def 6
.=
f . ((1 - 1) + i)
by A15, A131, A134, FINSEQ_6:122
.=
f /. i
by A21, PARTFUN1:def 6
;
LSeg (
f,
i) =
LSeg (
(f /. i),
(f /. (i + 1)))
by A15, A16, TOPREAL1:def 3
.=
LSeg (
g,1)
by A138, A140, A139, TOPREAL1:def 3
;
then
Y in { (LSeg (g,i2)) where i2 is Nat : ( 1 <= i2 & i2 + 1 <= len g ) }
by A14, A138;
then
p in union { (LSeg (g,i2)) where i2 is Nat : ( 1 <= i2 & i2 + 1 <= len g ) }
by A12, TARSKI:def 4;
then A141:
p in L~ (mid (f,i,(len f)))
by TOPREAL1:def 4;
A142:
LSeg (
f,
i)
= LSeg (
(f /. i),
(f /. (i + 1)))
by A15, A16, TOPREAL1:def 3;
A143:
for
p5 being
Point of
(TOP-REAL 2) st
LE f /. i,
p5,
P,
p1,
p2 &
LE p5,
p,
P,
p1,
p2 holds
p5 `1 >= e
proof
f /. i in LSeg (
(f /. i),
(f /. (i + 1)))
by RLTOPSP1:68;
then
LSeg (
(f /. i),
p)
c= LSeg (
f,
i)
by A12, A14, A142, TOPREAL1:6;
then A144:
LSeg (
(f /. i),
p)
c= P
by A6, A19, A14;
let p5 be
Point of
(TOP-REAL 2);
( LE f /. i,p5,P,p1,p2 & LE p5,p,P,p1,p2 implies p5 `1 >= e )
A145:
Segment (
P,
p1,
p2,
(f /. i),
p)
= { p8 where p8 is Point of (TOP-REAL 2) : ( LE f /. i,p8,P,p1,p2 & LE p8,p,P,p1,p2 ) }
by JORDAN6:26;
assume
(
LE f /. i,
p5,
P,
p1,
p2 &
LE p5,
p,
P,
p1,
p2 )
;
p5 `1 >= e
then A146:
p5 in Segment (
P,
p1,
p2,
(f /. i),
p)
by A145;
now ( ( f /. i <> p & p5 `1 >= e ) or ( f /. i = p & p5 `1 >= e ) )per cases
( f /. i <> p or f /. i = p )
;
case
f /. i <> p
;
p5 `1 >= ethen
LSeg (
(f /. i),
p)
is_an_arc_of f /. i,
p
by TOPREAL1:9;
then
Segment (
P,
p1,
p2,
(f /. i),
p)
= LSeg (
(f /. i),
p)
by A9, A5, A6, A7, A8, A15, A20, A141, A144, Th25, SPRECT_4:3;
hence
p5 `1 >= e
by A4, A128, A130, A146, TOPREAL1:3;
verum end;
hence
p5 `1 >= e
;
verum
end;
LE f /. i,
p,
P,
p1,
p2
by A5, A6, A7, A8, A15, A20, A141, SPRECT_4:3;
hence
(
p is_Lin P,
p1,
p2,
e or
p is_Rin P,
p1,
p2,
e )
by A3, A4, A9, A128, A130, A143;
verum end; case A147:
k <> 0
;
( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )reconsider ia =
i + 1 as
Nat ;
reconsider g =
mid (
f,
i,
(len f)) as
FinSequence of
(TOP-REAL 2) ;
A148:
i <= len f
by A16, NAT_1:13;
ia in Seg (len f)
by A16, A18, FINSEQ_1:1;
then A149:
i + 1
in dom f
by FINSEQ_1:def 3;
1
+ (1 + i) <= 1
+ (len f)
by A16, XREAL_1:7;
then A150:
((1 + 1) + i) - i <= ((len f) + 1) - i
by XREAL_1:9;
then A151:
1
<= ((len f) + 1) - i
by XXREAL_0:2;
A152:
(len f) - i > 0
by A20, XREAL_1:50;
then
(len f) -' i = (len f) - i
by XREAL_0:def 2;
then A153:
((len f) -' i) + 1
> 0 + 1
by A152, XREAL_1:8;
A154:
len g = ((len f) -' i) + 1
by A10, A15, A20, FINSEQ_6:118;
then A155:
1
+ 1
<= len g
by A153, NAT_1:13;
then
1
+ 1
in Seg (len g)
by FINSEQ_1:1;
then
1
+ 1
in dom g
by FINSEQ_1:def 3;
then A156:
g /. (1 + 1) =
g . (1 + 1)
by PARTFUN1:def 6
.=
f . (((1 + 1) - 1) + i)
by A15, A20, A150, FINSEQ_6:122
.=
f /. (i + 1)
by A149, PARTFUN1:def 6
;
1
in Seg (len g)
by A154, A153, FINSEQ_1:1;
then
1
in dom g
by FINSEQ_1:def 3;
then A157:
g /. 1 =
g . 1
by PARTFUN1:def 6
.=
f . ((1 - 1) + i)
by A15, A148, A151, FINSEQ_6:122
.=
f /. i
by A21, PARTFUN1:def 6
;
LSeg (
f,
i) =
LSeg (
(f /. i),
(f /. (i + 1)))
by A15, A16, TOPREAL1:def 3
.=
LSeg (
g,1)
by A155, A157, A156, TOPREAL1:def 3
;
then
Y in { (LSeg (g,i2)) where i2 is Nat : ( 1 <= i2 & i2 + 1 <= len g ) }
by A14, A155;
then
p in union { (LSeg (g,i2)) where i2 is Nat : ( 1 <= i2 & i2 + 1 <= len g ) }
by A12, TARSKI:def 4;
then A158:
p in L~ (mid (f,i,(len f)))
by TOPREAL1:def 4;
reconsider g =
mid (
f,1,
i) as
FinSequence of
(TOP-REAL 2) ;
set p44 =
f /. i;
A159:
(
i <= len f & 1
<= i -' k )
by A16, A27, NAT_1:13, XREAL_0:def 2;
A160:
k >= 0 + 1
by A147, NAT_1:13;
then A161:
i -' k <= (i + 1) - 1
by A28, NAT_D:51;
A162:
i > i -' k
by A28, A160, NAT_D:51;
then A163:
i > 1
by A28, XXREAL_0:2;
then
i - 1
> 0
by XREAL_1:50;
then A164:
i -' 1
= i - 1
by XREAL_0:def 2;
A167:
now for p51 being Point of (TOP-REAL 2) st LE pk,p51,P,p1,p2 & LE p51,f /. i,P,p1,p2 holds
p51 `1 >= eassume
ex
p51 being
Point of
(TOP-REAL 2) st
(
LE pk,
p51,
P,
p1,
p2 &
LE p51,
f /. i,
P,
p1,
p2 & not
p51 `1 >= e )
;
contradictionthen consider p51 being
Point of
(TOP-REAL 2) such that A168:
LE pk,
p51,
P,
p1,
p2
and A169:
LE p51,
f /. i,
P,
p1,
p2
and A170:
p51 `1 < e
;
p51 in P
by A168, JORDAN5C:def 3;
then consider Y3 being
set such that A171:
p51 in Y3
and A172:
Y3 in { (LSeg (f,i5)) where i5 is Nat : ( 1 <= i5 & i5 + 1 <= len f ) }
by A6, A11, TARSKI:def 4;
consider kk being
Nat such that A173:
Y3 = LSeg (
f,
kk)
and A174:
1
<= kk
and A175:
kk + 1
<= len f
by A172;
A176:
LSeg (
f,
kk)
= LSeg (
(f /. kk),
(f /. (kk + 1)))
by A174, A175, TOPREAL1:def 3;
1
< kk + 1
by A174, NAT_1:13;
then
kk + 1
in Seg (len f)
by A175, FINSEQ_1:1;
then A177:
kk + 1
in dom f
by FINSEQ_1:def 3;
A178:
kk < len f
by A175, NAT_1:13;
then
kk in Seg (len f)
by A174, FINSEQ_1:1;
then A179:
kk in dom f
by FINSEQ_1:def 3;
A180:
LE p51,
f /. (kk + 1),
L~ f,
f /. 1,
f /. (len f)
by A5, A171, A173, A174, A175, JORDAN5C:26;
now ( ( (f /. kk) `1 < e & contradiction ) or ( (f /. (kk + 1)) `1 < e & (f /. kk) `1 >= e & contradiction ) )per cases
( (f /. kk) `1 < e or ( (f /. (kk + 1)) `1 < e & (f /. kk) `1 >= e ) )
by A170, A171, A173, A176, Th3;
case A181:
(f /. kk) `1 < e
;
contradictionset k2 =
i -' kk;
LE f /. kk,
p51,
L~ f,
f /. 1,
f /. (len f)
by A5, A171, A173, A174, A175, JORDAN5C:25;
then A182:
LE f /. kk,
f /. i,
L~ f,
f /. 1,
f /. (len f)
by A6, A7, A8, A169, JORDAN5C:13;
now not i - kk <= 0 assume
i - kk <= 0
;
contradictionthen
(i - kk) + kk <= 0 + kk
by XREAL_1:7;
then
LE f /. i,
f /. kk,
L~ f,
f /. 1,
f /. (len f)
by A5, A163, A178, JORDAN5C:24;
hence
contradiction
by A1, A6, A7, A8, A165, A181, A182, JORDAN5C:12, TOPREAL4:2;
verum end; then A183:
i - (i -' kk) =
i - (i - kk)
by XREAL_0:def 2
.=
kk
;
then A184:
i - (i -' kk) = i -' (i -' kk)
by XREAL_0:def 2;
then
S1[
i -' kk]
by A20, A174, A181, A183, FINSEQ_4:15, NAT_D:50;
then
i -' kk >= k
by A26;
then
i - (i -' kk) <= i - k
by XREAL_1:10;
then A185:
LE f /. (i -' (i -' kk)),
f /. (i -' k),
L~ f,
f /. 1,
f /. (len f)
by A5, A29, A32, A174, A183, A184, JORDAN5C:24;
A186:
LSeg (
(f /. kk),
(f /. (kk + 1)))
c= L~ f
f is
special
by A5, TOPREAL1:def 8;
then A188:
(
(f /. kk) `1 = (f /. (kk + 1)) `1 or
(f /. kk) `2 = (f /. (kk + 1)) `2 )
by A174, A175, TOPREAL1:def 5;
(
f is
one-to-one &
kk < kk + 1 )
by A5, NAT_1:13, TOPREAL1:def 8;
then A189:
f . kk <> f . (kk + 1)
by A179, A177, FUNCT_1:def 4;
A190:
LE f /. (i -' k),
p51,
L~ f,
f /. 1,
f /. (len f)
by A6, A7, A8, A30, A168, PARTFUN1:def 6;
A191:
LE f /. (i -' k),
f /. (kk + 1),
L~ f,
f /. 1,
f /. (len f)
by A6, A7, A8, A31, A168, A180, JORDAN5C:13;
(
f /. kk = f . kk &
f /. (kk + 1) = f . (kk + 1) )
by A179, A177, PARTFUN1:def 6;
then
LSeg (
(f /. kk),
(f /. (kk + 1)))
is_an_arc_of f /. kk,
f /. (kk + 1)
by A189, TOPREAL1:9;
then A192:
Segment (
(L~ f),
(f /. 1),
(f /. (len f)),
(f /. kk),
(f /. (kk + 1)))
= LSeg (
(f /. kk),
(f /. (kk + 1)))
by A9, A6, A7, A8, A183, A184, A185, A191, A186, Th25, JORDAN5C:13;
Segment (
(L~ f),
(f /. 1),
(f /. (len f)),
(f /. kk),
(f /. (kk + 1)))
= { p8 where p8 is Point of (TOP-REAL 2) : ( LE f /. kk,p8, L~ f,f /. 1,f /. (len f) & LE p8,f /. (kk + 1), L~ f,f /. 1,f /. (len f) ) }
by JORDAN6:26;
then A193:
f /. (i -' k) in Segment (
(L~ f),
(f /. 1),
(f /. (len f)),
(f /. kk),
(f /. (kk + 1)))
by A183, A184, A185, A191;
then
(f /. (kk + 1)) `1 > e
by A31, A128, A181, A192, Th2;
then
(f /. kk) `1 < (f /. (kk + 1)) `1
by A181, XXREAL_0:2;
then
(f /. (i -' k)) `1 <= p51 `1
by A5, A171, A173, A174, A178, A176, A190, A193, A192, A188, Th7;
hence
contradiction
by A31, A128, A170, XXREAL_0:2;
verum end; case A194:
(
(f /. (kk + 1)) `1 < e &
(f /. kk) `1 >= e )
;
contradictionset k2 =
(i -' kk) -' 1;
A195:
LSeg (
(f /. kk),
(f /. (kk + 1)))
c= L~ f
(
f is
one-to-one &
kk < kk + 1 )
by A5, NAT_1:13, TOPREAL1:def 8;
then A197:
f . kk <> f . (kk + 1)
by A179, A177, FUNCT_1:def 4;
A198:
(f /. kk) `1 > (f /. (kk + 1)) `1
by A194, XXREAL_0:2;
LE f /. kk,
p51,
L~ f,
f /. 1,
f /. (len f)
by A5, A171, A173, A174, A175, JORDAN5C:25;
then A199:
LE f /. kk,
f /. i,
L~ f,
f /. 1,
f /. (len f)
by A6, A7, A8, A169, JORDAN5C:13;
(
f /. kk = f . kk &
f /. (kk + 1) = f . (kk + 1) )
by A179, A177, PARTFUN1:def 6;
then
LSeg (
(f /. kk),
(f /. (kk + 1)))
is_an_arc_of f /. kk,
f /. (kk + 1)
by A197, TOPREAL1:9;
then A200:
(
Segment (
(L~ f),
(f /. 1),
(f /. (len f)),
(f /. kk),
(f /. (kk + 1)))
= { p8 where p8 is Point of (TOP-REAL 2) : ( LE f /. kk,p8, L~ f,f /. 1,f /. (len f) & LE p8,f /. (kk + 1), L~ f,f /. 1,f /. (len f) ) } &
Segment (
(L~ f),
(f /. 1),
(f /. (len f)),
(f /. kk),
(f /. (kk + 1)))
= LSeg (
(f /. kk),
(f /. (kk + 1))) )
by A9, A5, A6, A7, A8, A174, A175, A195, Th25, JORDAN5C:23, JORDAN6:26;
A201:
now not (i - kk) - 1 <= 0 assume
(i - kk) - 1
<= 0
;
contradictionthen
(i - (kk + 1)) + (kk + 1) <= 0 + (kk + 1)
by XREAL_1:7;
then
LE f /. i,
f /. (kk + 1),
L~ f,
f /. 1,
f /. (len f)
by A5, A163, A175, JORDAN5C:24;
then A202:
f /. i in LSeg (
(f /. kk),
(f /. (kk + 1)))
by A200, A199;
f is
special
by A5, TOPREAL1:def 8;
then A203:
(
(f /. kk) `1 = (f /. (kk + 1)) `1 or
(f /. kk) `2 = (f /. (kk + 1)) `2 )
by A174, A175, TOPREAL1:def 5;
LSeg (
f,
kk)
= LSeg (
(f /. kk),
(f /. (kk + 1)))
by A174, A175, TOPREAL1:def 3;
hence
contradiction
by A5, A6, A7, A8, A165, A169, A170, A171, A173, A174, A178, A198, A202, A203, Th6;
verum end; then
((i - kk) - 1) + 1
>= 0 + 1
by XREAL_1:7;
then
i -' kk = i - kk
by XREAL_0:def 2;
then A204:
i - ((i -' kk) -' 1) =
i - ((i - kk) - 1)
by A201, XREAL_0:def 2
.=
kk + 1
;
then
i -' ((i -' kk) -' 1) > 0
by XREAL_0:def 2;
then A205:
i -' ((i -' kk) -' 1) >= 0 + 1
by NAT_1:13;
A206:
i - ((i -' kk) -' 1) = i -' ((i -' kk) -' 1)
by A204, XREAL_0:def 2;
then
S1[
(i -' kk) -' 1]
by A20, A194, A204, A205, FINSEQ_4:15, NAT_D:50;
then
(i -' kk) -' 1
>= k
by A26;
then
i - ((i -' kk) -' 1) <= i - k
by XREAL_1:10;
then A207:
LE f /. (kk + 1),
f /. (i -' k),
L~ f,
f /. 1,
f /. (len f)
by A5, A29, A32, A204, A206, A205, JORDAN5C:24;
LE f /. (i -' k),
f /. (kk + 1),
L~ f,
f /. 1,
f /. (len f)
by A6, A7, A8, A31, A168, A180, JORDAN5C:13;
hence
contradiction
by A1, A6, A7, A8, A31, A128, A194, A207, JORDAN5C:12, TOPREAL4:2;
verum end; hence
contradiction
;
verum end; A208:
LSeg (
f,
i)
= LSeg (
(f /. i),
(f /. (i + 1)))
by A15, A16, TOPREAL1:def 3;
A209:
for
p5 being
Point of
(TOP-REAL 2) st
LE f /. i,
p5,
P,
p1,
p2 &
LE p5,
p,
P,
p1,
p2 holds
p5 `1 >= e
proof
let p5 be
Point of
(TOP-REAL 2);
( LE f /. i,p5,P,p1,p2 & LE p5,p,P,p1,p2 implies p5 `1 >= e )
A210:
Segment (
P,
p1,
p2,
(f /. i),
p)
= { p8 where p8 is Point of (TOP-REAL 2) : ( LE f /. i,p8,P,p1,p2 & LE p8,p,P,p1,p2 ) }
by JORDAN6:26;
assume
(
LE f /. i,
p5,
P,
p1,
p2 &
LE p5,
p,
P,
p1,
p2 )
;
p5 `1 >= e
then A211:
p5 in Segment (
P,
p1,
p2,
(f /. i),
p)
by A210;
f /. i in LSeg (
(f /. i),
(f /. (i + 1)))
by RLTOPSP1:68;
then
LSeg (
(f /. i),
p)
c= LSeg (
f,
i)
by A12, A14, A208, TOPREAL1:6;
then A212:
LSeg (
(f /. i),
p)
c= P
by A6, A19, A14;
now ( ( f /. i <> p & p5 `1 >= e ) or ( f /. i = p & p5 `1 >= e ) )per cases
( f /. i <> p or f /. i = p )
;
case
f /. i <> p
;
p5 `1 >= ethen
LSeg (
(f /. i),
p)
is_an_arc_of f /. i,
p
by TOPREAL1:9;
then
Segment (
P,
p1,
p2,
(f /. i),
p)
= LSeg (
(f /. i),
p)
by A9, A5, A6, A7, A8, A15, A20, A158, A212, Th25, SPRECT_4:3;
hence
p5 `1 >= e
by A4, A165, A211, TOPREAL1:3;
verum end;
hence
p5 `1 >= e
;
verum
end; A213:
len g = (i -' 1) + 1
by A15, A20, A22, FINSEQ_6:118;
then
(i -' k) + 1
<= len g
by A162, A164, NAT_1:13;
then A214:
LSeg (
g,
(i -' k))
= LSeg (
(g /. (i -' k)),
(g /. ((i -' k) + 1)))
by A28, TOPREAL1:def 3;
i -' k < i
by A28, A160, NAT_D:51;
then
i -' k in Seg (len g)
by A28, A213, A164, FINSEQ_1:1;
then
i -' k in dom g
by FINSEQ_1:def 3;
then g /. (i -' k) =
g . (i -' k)
by PARTFUN1:def 6
.=
f . (((i -' k) - 1) + 1)
by A15, A159, A161, FINSEQ_6:122
.=
f /. (i -' k)
by A30, PARTFUN1:def 6
;
then A215:
pk in LSeg (
g,
(i -' k))
by A31, A214, RLTOPSP1:68;
A216:
(i -' k) + 1
<= i
by A162, NAT_1:13;
1
<= i -' k
by A27, XREAL_0:def 2;
then
LSeg (
g,
(i -' k))
in { (LSeg (g,i2)) where i2 is Nat : ( 1 <= i2 & i2 + 1 <= len g ) }
by A213, A164, A216;
then
pk in union { (LSeg (g,i2)) where i2 is Nat : ( 1 <= i2 & i2 + 1 <= len g ) }
by A215, TARSKI:def 4;
then
pk in L~ (mid (f,1,i))
by TOPREAL1:def 4;
then A217:
LE pk,
f /. i,
P,
p1,
p2
by A5, A6, A7, A8, A20, A163, SPRECT_3:17;
then A218:
f /. i in P
by JORDAN5C:def 3;
A219:
for
p5 being
Point of
(TOP-REAL 2) st
LE pk,
p5,
P,
p1,
p2 &
LE p5,
p,
P,
p1,
p2 holds
p5 `1 >= e
proof
let p5 be
Point of
(TOP-REAL 2);
( LE pk,p5,P,p1,p2 & LE p5,p,P,p1,p2 implies p5 `1 >= e )
assume that A220:
LE pk,
p5,
P,
p1,
p2
and A221:
LE p5,
p,
P,
p1,
p2
;
p5 `1 >= e
A222:
p5 in P
by A220, JORDAN5C:def 3;
now ( ( LE p5,f /. i,P,p1,p2 & p5 `1 >= e ) or ( LE f /. i,p5,P,p1,p2 & p5 `1 >= e ) )per cases
( LE p5,f /. i,P,p1,p2 or LE f /. i,p5,P,p1,p2 )
by A1, A218, A222, Th19, TOPREAL4:2;
end;
hence
p5 `1 >= e
;
verum
end;
LE f /. i,
p,
P,
p1,
p2
by A5, A6, A7, A8, A15, A20, A158, SPRECT_4:3;
then
LE pk,
p,
P,
p1,
p2
by A217, JORDAN5C:13;
hence
(
p is_Lin P,
p1,
p2,
e or
p is_Rin P,
p1,
p2,
e )
by A3, A4, A9, A128, A219;
verum end; hence
(
p is_Lin P,
p1,
p2,
e or
p is_Rin P,
p1,
p2,
e )
;
verum
hence
( p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e )
; verum