let p be Point of (TOP-REAL 2); :: thesis: for f, h being FinSequence of (TOP-REAL 2)

for r being Real

for u being Point of (Euclid 2) st ( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) ) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} & h = f ^ <*p*> holds

( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

let f, h be FinSequence of (TOP-REAL 2); :: thesis: for r being Real

for u being Point of (Euclid 2) st ( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) ) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} & h = f ^ <*p*> holds

( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

let r be Real; :: thesis: for u being Point of (Euclid 2) st ( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) ) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} & h = f ^ <*p*> holds

( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

let u be Point of (Euclid 2); :: thesis: ( ( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) ) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} & h = f ^ <*p*> implies ( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) )

set p1 = f /. 1;

set p2 = f /. (len f);

assume A1: ( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) ) ; :: thesis: ( not f /. (len f) in Ball (u,r) or not p in Ball (u,r) or not f is being_S-Seq or not (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} or not h = f ^ <*p*> or ( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) )

assume that

A2: ( f /. (len f) in Ball (u,r) & p in Ball (u,r) ) and

A3: f is being_S-Seq and

A4: (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} and

A5: h = f ^ <*p*> ; :: thesis: ( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

A6: not p in L~ f by A1, A4, TOPREAL3:40;

A7: f is one-to-one by A3;

A8: f is unfolded by A3;

A9: f is one-to-one by A3;

A10: f is s.n.c. by A3;

A11: Seg (len h) = dom h by FINSEQ_1:def 3;

set Mf = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;

set Mh = { (LSeg (h,m)) where m is Nat : ( 1 <= m & m + 1 <= len h ) } ;

A12: Seg (len f) = dom f by FINSEQ_1:def 3;

A13: 2 <= len f by A3;

then A14: 1 <= len f by XXREAL_0:2;

then A15: len f in dom f by A12, FINSEQ_1:1;

then A16: h /. (len f) = f /. (len f) by A5, FINSEQ_4:68;

A17: len h = (len f) + (len <*p*>) by A5, FINSEQ_1:22

.= (len f) + 1 by FINSEQ_1:39 ;

then A18: h /. (len h) = p by A5, FINSEQ_4:67;

then A19: LSeg (h,(len f)) = LSeg ((f /. (len f)),p) by A17, A14, A16, TOPREAL1:def 3;

A20: f is special by A3;

thus A21: h is being_S-Seq :: thesis: ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

then h /. 1 = f /. 1 by A5, FINSEQ_4:68;

hence L~ h is_S-P_arc_joining f /. 1,p by A18, A21; :: thesis: L~ h c= (L~ f) \/ (Ball (u,r))

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ h or x in (L~ f) \/ (Ball (u,r)) )

assume x in L~ h ; :: thesis: x in (L~ f) \/ (Ball (u,r))

then consider X being set such that

A90: x in X and

A91: X in { (LSeg (h,m)) where m is Nat : ( 1 <= m & m + 1 <= len h ) } by TARSKI:def 4;

consider k being Nat such that

A92: X = LSeg (h,k) and

A93: 1 <= k and

A94: k + 1 <= len h by A91;

for r being Real

for u being Point of (Euclid 2) st ( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) ) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} & h = f ^ <*p*> holds

( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

let f, h be FinSequence of (TOP-REAL 2); :: thesis: for r being Real

for u being Point of (Euclid 2) st ( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) ) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} & h = f ^ <*p*> holds

( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

let r be Real; :: thesis: for u being Point of (Euclid 2) st ( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) ) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} & h = f ^ <*p*> holds

( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

let u be Point of (Euclid 2); :: thesis: ( ( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) ) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} & h = f ^ <*p*> implies ( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) )

set p1 = f /. 1;

set p2 = f /. (len f);

assume A1: ( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) ) ; :: thesis: ( not f /. (len f) in Ball (u,r) or not p in Ball (u,r) or not f is being_S-Seq or not (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} or not h = f ^ <*p*> or ( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) )

assume that

A2: ( f /. (len f) in Ball (u,r) & p in Ball (u,r) ) and

A3: f is being_S-Seq and

A4: (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} and

A5: h = f ^ <*p*> ; :: thesis: ( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

A6: not p in L~ f by A1, A4, TOPREAL3:40;

A7: f is one-to-one by A3;

A8: f is unfolded by A3;

A9: f is one-to-one by A3;

A10: f is s.n.c. by A3;

A11: Seg (len h) = dom h by FINSEQ_1:def 3;

set Mf = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;

set Mh = { (LSeg (h,m)) where m is Nat : ( 1 <= m & m + 1 <= len h ) } ;

A12: Seg (len f) = dom f by FINSEQ_1:def 3;

A13: 2 <= len f by A3;

then A14: 1 <= len f by XXREAL_0:2;

then A15: len f in dom f by A12, FINSEQ_1:1;

then A16: h /. (len f) = f /. (len f) by A5, FINSEQ_4:68;

A17: len h = (len f) + (len <*p*>) by A5, FINSEQ_1:22

.= (len f) + 1 by FINSEQ_1:39 ;

then A18: h /. (len h) = p by A5, FINSEQ_4:67;

then A19: LSeg (h,(len f)) = LSeg ((f /. (len f)),p) by A17, A14, A16, TOPREAL1:def 3;

A20: f is special by A3;

thus A21: h is being_S-Seq :: thesis: ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

proof

2 + 1 <= (len f) + 1 by A13, XREAL_1:6;

hence len h >= 2 by A17, XXREAL_0:2; :: thesis: ( h is unfolded & h is s.n.c. & h is special )

thus h is unfolded :: thesis: ( h is s.n.c. & h is special )end;

1 in dom f
by A12, A14, FINSEQ_1:1;now :: thesis: for x, y being object holds

( not x in dom h or not y in dom h or not h . x = h . y or not x <> y )

hence
h is one-to-one
by FUNCT_1:def 4; :: according to TOPREAL1:def 8 :: thesis: ( 2 <= len h & h is unfolded & h is s.n.c. & h is special )( not x in dom h or not y in dom h or not h . x = h . y or not x <> y )

set Z = { m where m is Nat : ( 1 <= m & m <= len h ) } ;

given x, y being object such that A22: x in dom h and

A23: y in dom h and

A24: h . x = h . y and

A25: x <> y ; :: thesis: contradiction

y in { m where m is Nat : ( 1 <= m & m <= len h ) } by A11, A23, FINSEQ_1:def 1;

then consider k2 being Nat such that

A26: k2 = y and

A27: 1 <= k2 and

A28: k2 <= len h ;

x in { m where m is Nat : ( 1 <= m & m <= len h ) } by A11, A22, FINSEQ_1:def 1;

then consider k1 being Nat such that

A29: k1 = x and

A30: 1 <= k1 and

A31: k1 <= len h ;

A32: h /. k1 = h . y by A22, A24, A29, PARTFUN1:def 6

.= h /. k2 by A23, A26, PARTFUN1:def 6 ;

end;given x, y being object such that A22: x in dom h and

A23: y in dom h and

A24: h . x = h . y and

A25: x <> y ; :: thesis: contradiction

y in { m where m is Nat : ( 1 <= m & m <= len h ) } by A11, A23, FINSEQ_1:def 1;

then consider k2 being Nat such that

A26: k2 = y and

A27: 1 <= k2 and

A28: k2 <= len h ;

x in { m where m is Nat : ( 1 <= m & m <= len h ) } by A11, A22, FINSEQ_1:def 1;

then consider k1 being Nat such that

A29: k1 = x and

A30: 1 <= k1 and

A31: k1 <= len h ;

A32: h /. k1 = h . y by A22, A24, A29, PARTFUN1:def 6

.= h /. k2 by A23, A26, PARTFUN1:def 6 ;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( ( k1 = (len f) + 1 & k2 = (len f) + 1 ) or ( k1 = (len f) + 1 & k2 < (len f) + 1 ) or ( k1 < (len f) + 1 & k2 = (len f) + 1 ) or ( k1 < (len f) + 1 & k2 < (len f) + 1 ) )
by A17, A31, A28, XXREAL_0:1;

end;

suppose A33:
( k1 = (len f) + 1 & k2 < (len f) + 1 )
; :: thesis: contradiction

then A34:
k2 + 1 <= k1
by NAT_1:13;

end;now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( k2 + 1 = k1 or k2 + 1 < k1 )
by A34, XXREAL_0:1;

end;

suppose
k2 + 1 < k1
; :: thesis: contradiction

then A35:
k2 < ((len f) + 1) - 1
by A33, XREAL_1:20;

reconsider k2 = k2 as Element of NAT by ORDINAL1:def 12;

k2 in dom f by A12, A27, A35, FINSEQ_1:1;

then h /. k2 = f /. k2 by A5, FINSEQ_4:68;

hence contradiction by A5, A13, A6, A27, A32, A33, A35, FINSEQ_4:67, TOPREAL3:39; :: thesis: verum

end;reconsider k2 = k2 as Element of NAT by ORDINAL1:def 12;

k2 in dom f by A12, A27, A35, FINSEQ_1:1;

then h /. k2 = f /. k2 by A5, FINSEQ_4:68;

hence contradiction by A5, A13, A6, A27, A32, A33, A35, FINSEQ_4:67, TOPREAL3:39; :: thesis: verum

suppose A36:
( k1 < (len f) + 1 & k2 = (len f) + 1 )
; :: thesis: contradiction

then A37:
k1 + 1 <= k2
by NAT_1:13;

end;now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( k1 + 1 = k2 or k1 + 1 < k2 )
by A37, XXREAL_0:1;

end;

suppose
k1 + 1 < k2
; :: thesis: contradiction

then A38:
k1 < ((len f) + 1) - 1
by A36, XREAL_1:20;

reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;

k1 in dom f by A12, A30, A38, FINSEQ_1:1;

then h /. k1 = f /. k1 by A5, FINSEQ_4:68;

hence contradiction by A5, A13, A6, A30, A32, A36, A38, FINSEQ_4:67, TOPREAL3:39; :: thesis: verum

end;reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;

k1 in dom f by A12, A30, A38, FINSEQ_1:1;

then h /. k1 = f /. k1 by A5, FINSEQ_4:68;

hence contradiction by A5, A13, A6, A30, A32, A36, A38, FINSEQ_4:67, TOPREAL3:39; :: thesis: verum

suppose A39:
( k1 < (len f) + 1 & k2 < (len f) + 1 )
; :: thesis: contradiction

then
k2 <= len f
by NAT_1:13;

then A40: k2 in dom f by A12, A27, FINSEQ_1:1;

k1 <= len f by A39, NAT_1:13;

then A41: k1 in dom f by A12, A30, FINSEQ_1:1;

then f . k1 = h . k1 by A5, FINSEQ_1:def 7

.= f . k2 by A5, A24, A29, A26, A40, FINSEQ_1:def 7 ;

hence contradiction by A9, A25, A29, A26, A41, A40, FUNCT_1:def 4; :: thesis: verum

end;then A40: k2 in dom f by A12, A27, FINSEQ_1:1;

k1 <= len f by A39, NAT_1:13;

then A41: k1 in dom f by A12, A30, FINSEQ_1:1;

then f . k1 = h . k1 by A5, FINSEQ_1:def 7

.= f . k2 by A5, A24, A29, A26, A40, FINSEQ_1:def 7 ;

hence contradiction by A9, A25, A29, A26, A41, A40, FUNCT_1:def 4; :: thesis: verum

2 + 1 <= (len f) + 1 by A13, XREAL_1:6;

hence len h >= 2 by A17, XXREAL_0:2; :: thesis: ( h is unfolded & h is s.n.c. & h is special )

thus h is unfolded :: thesis: ( h is s.n.c. & h is special )

proof

thus
h is s.n.c.
:: thesis: h is special
let j be Nat; :: according to TOPREAL1:def 6 :: thesis: ( not 1 <= j or not j + 2 <= len h or (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} )

assume that

A42: 1 <= j and

A43: j + 2 <= len h ; :: thesis: (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))}

A44: j + (1 + 1) = (j + 1) + 1 ;

j + 1 <= j + 2 by XREAL_1:6;

then A45: j + 1 <= len h by A43, XXREAL_0:2;

end;assume that

A42: 1 <= j and

A43: j + 2 <= len h ; :: thesis: (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))}

A44: j + (1 + 1) = (j + 1) + 1 ;

j + 1 <= j + 2 by XREAL_1:6;

then A45: j + 1 <= len h by A43, XXREAL_0:2;

now :: thesis: (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))}end;

hence
(LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))}
; :: thesis: verumper cases
( j + 2 = len h or j + 2 < len h )
by A43, XXREAL_0:1;

end;

suppose A46:
j + 2 = len h
; :: thesis: (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))}

then A47:
j + ((1 + 1) - 1) = len f
by A17;

then j <= len f by NAT_1:13;

then j in dom f by A12, A42, FINSEQ_1:1;

then A48: LSeg (h,j) = LSeg (f,j) by A5, A15, A47, TOPREAL3:18;

LSeg (h,j) in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by A42, A47, A48;

then A49: LSeg (h,j) = (LSeg (h,j)) /\ (L~ f) by XBOOLE_1:28, ZFMISC_1:74;

h /. (j + 1) in LSeg (h,j) by A42, A45, TOPREAL1:21;

then A50: {(h /. (j + 1))} c= LSeg (h,j) by ZFMISC_1:31;

LSeg (h,(j + 1)) = LSeg ((f /. (len f)),p) by A17, A14, A18, A16, A46, TOPREAL1:def 3;

hence (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = (LSeg (h,j)) /\ {(h /. (j + 1))} by A4, A17, A16, A46, A49, XBOOLE_1:16

.= {(h /. (j + 1))} by A50, XBOOLE_1:28 ;

:: thesis: verum

end;then j <= len f by NAT_1:13;

then j in dom f by A12, A42, FINSEQ_1:1;

then A48: LSeg (h,j) = LSeg (f,j) by A5, A15, A47, TOPREAL3:18;

LSeg (h,j) in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by A42, A47, A48;

then A49: LSeg (h,j) = (LSeg (h,j)) /\ (L~ f) by XBOOLE_1:28, ZFMISC_1:74;

h /. (j + 1) in LSeg (h,j) by A42, A45, TOPREAL1:21;

then A50: {(h /. (j + 1))} c= LSeg (h,j) by ZFMISC_1:31;

LSeg (h,(j + 1)) = LSeg ((f /. (len f)),p) by A17, A14, A18, A16, A46, TOPREAL1:def 3;

hence (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = (LSeg (h,j)) /\ {(h /. (j + 1))} by A4, A17, A16, A46, A49, XBOOLE_1:16

.= {(h /. (j + 1))} by A50, XBOOLE_1:28 ;

:: thesis: verum

suppose
j + 2 < len h
; :: thesis: (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))}

then A51:
(j + (2 + 1)) - 1 <= len f
by A17, NAT_1:13;

then A52: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A8, A42, A43;

1 <= j + 2 by A44, NAT_1:11;

then A53: (j + 1) + 1 in dom f by A12, A51, FINSEQ_1:1;

j + 1 <= j + 2 by A44, NAT_1:11;

then A54: j + 1 <= len f by A51, XXREAL_0:2;

1 <= j + 1 by NAT_1:11;

then A55: j + 1 in dom f by A12, A54, FINSEQ_1:1;

then A56: h /. (j + 1) = f /. (j + 1) by A5, FINSEQ_4:68;

j <= j + 1 by NAT_1:11;

then j <= len f by A54, XXREAL_0:2;

then j in dom f by A12, A42, FINSEQ_1:1;

then LSeg (h,j) = LSeg (f,j) by A5, A55, TOPREAL3:18;

hence (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} by A5, A52, A55, A53, A56, TOPREAL3:18; :: thesis: verum

end;then A52: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A8, A42, A43;

1 <= j + 2 by A44, NAT_1:11;

then A53: (j + 1) + 1 in dom f by A12, A51, FINSEQ_1:1;

j + 1 <= j + 2 by A44, NAT_1:11;

then A54: j + 1 <= len f by A51, XXREAL_0:2;

1 <= j + 1 by NAT_1:11;

then A55: j + 1 in dom f by A12, A54, FINSEQ_1:1;

then A56: h /. (j + 1) = f /. (j + 1) by A5, FINSEQ_4:68;

j <= j + 1 by NAT_1:11;

then j <= len f by A54, XXREAL_0:2;

then j in dom f by A12, A42, FINSEQ_1:1;

then LSeg (h,j) = LSeg (f,j) by A5, A55, TOPREAL3:18;

hence (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} by A5, A52, A55, A53, A56, TOPREAL3:18; :: thesis: verum

proof

let n, m be Nat; :: according to TOPREAL1:def 7 :: thesis: ( m <= n + 1 or LSeg (h,n) misses LSeg (h,m) )

assume A57: m > n + 1 ; :: thesis: LSeg (h,n) misses LSeg (h,m)

n <= n + 1 by NAT_1:11;

then A58: n <= m by A57, XXREAL_0:2;

A59: (n + 1) + 1 = n + (1 + 1) ;

A60: 1 <= n + 1 by NAT_1:11;

LSeg (f,n) misses LSeg (f,m) by A10, A57;

then A61: (LSeg (f,n)) /\ (LSeg (f,m)) = {} ;

end;assume A57: m > n + 1 ; :: thesis: LSeg (h,n) misses LSeg (h,m)

n <= n + 1 by NAT_1:11;

then A58: n <= m by A57, XXREAL_0:2;

A59: (n + 1) + 1 = n + (1 + 1) ;

A60: 1 <= n + 1 by NAT_1:11;

LSeg (f,n) misses LSeg (f,m) by A10, A57;

then A61: (LSeg (f,n)) /\ (LSeg (f,m)) = {} ;

now :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {} end;

hence
(LSeg (h,n)) /\ (LSeg (h,m)) = {}
; :: according to XBOOLE_0:def 7 :: thesis: verumper cases
( m + 1 < len h or m + 1 = len h or m + 1 > len h )
by XXREAL_0:1;

end;

suppose A62:
m + 1 < len h
; :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}

then A63:
m + 1 <= len f
by A17, NAT_1:13;

A64: 1 < m by A57, A60, XXREAL_0:2;

then 1 <= m + 1 by NAT_1:13;

then A65: m + 1 in dom f by A12, A63, FINSEQ_1:1;

A66: m <= len f by A17, A62, XREAL_1:6;

then m in dom f by A12, A64, FINSEQ_1:1;

then A67: LSeg (h,m) = LSeg (f,m) by A5, A65, TOPREAL3:18;

end;A64: 1 < m by A57, A60, XXREAL_0:2;

then 1 <= m + 1 by NAT_1:13;

then A65: m + 1 in dom f by A12, A63, FINSEQ_1:1;

A66: m <= len f by A17, A62, XREAL_1:6;

then m in dom f by A12, A64, FINSEQ_1:1;

then A67: LSeg (h,m) = LSeg (f,m) by A5, A65, TOPREAL3:18;

now :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {} end;

hence
(LSeg (h,n)) /\ (LSeg (h,m)) = {}
; :: thesis: verumper cases
( 0 < n or 0 = n )
;

end;

suppose
0 < n
; :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}

then A68:
0 + 1 <= n
by NAT_1:13;

n + 1 <= len f by A57, A66, XXREAL_0:2;

then A69: n + 1 in dom f by A12, A60, FINSEQ_1:1;

n <= len f by A58, A66, XXREAL_0:2;

then n in dom f by A12, A68, FINSEQ_1:1;

hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} by A5, A61, A67, A69, TOPREAL3:18; :: thesis: verum

end;n + 1 <= len f by A57, A66, XXREAL_0:2;

then A69: n + 1 in dom f by A12, A60, FINSEQ_1:1;

n <= len f by A58, A66, XXREAL_0:2;

then n in dom f by A12, A68, FINSEQ_1:1;

hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} by A5, A61, A67, A69, TOPREAL3:18; :: thesis: verum

suppose A70:
m + 1 = len h
; :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}

end;

now :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {} end;

hence
(LSeg (h,n)) /\ (LSeg (h,m)) = {}
; :: thesis: verumper cases
( 0 < n or 0 = n )
;

end;

suppose A71:
0 < n
; :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}

A72:
n + 1 in dom f
by A17, A12, A57, A60, A70, FINSEQ_1:1;

A73: 0 + 1 <= n by A71, NAT_1:13;

then n in dom f by A17, A12, A58, A70, FINSEQ_1:1;

then A74: LSeg (h,n) = LSeg (f,n) by A5, A72, TOPREAL3:18;

end;A73: 0 + 1 <= n by A71, NAT_1:13;

then n in dom f by A17, A12, A58, A70, FINSEQ_1:1;

then A74: LSeg (h,n) = LSeg (f,n) by A5, A72, TOPREAL3:18;

now :: thesis: not (LSeg (h,n)) /\ (LSeg (h,m)) <> {}

hence
(LSeg (h,n)) /\ (LSeg (h,m)) = {}
; :: thesis: verumset L = LSeg (f,n);

set x = the Element of (LSeg (h,n)) /\ (LSeg (h,m));

assume A75: (LSeg (h,n)) /\ (LSeg (h,m)) <> {} ; :: thesis: contradiction

then A76: the Element of (LSeg (h,n)) /\ (LSeg (h,m)) in LSeg (f,n) by A74, XBOOLE_0:def 4;

A77: the Element of (LSeg (h,n)) /\ (LSeg (h,m)) in LSeg ((f /. (len f)),p) by A17, A19, A70, A75, XBOOLE_0:def 4;

LSeg (f,n) in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by A17, A57, A70, A73;

then the Element of (LSeg (h,n)) /\ (LSeg (h,m)) in L~ f by A76, TARSKI:def 4;

then the Element of (LSeg (h,n)) /\ (LSeg (h,m)) in {(f /. (len f))} by A4, A77, XBOOLE_0:def 4;

then A78: the Element of (LSeg (h,n)) /\ (LSeg (h,m)) = f /. (len f) by TARSKI:def 1;

A79: (n + 1) + 1 <= len f by A17, A57, A70, NAT_1:13;

end;set x = the Element of (LSeg (h,n)) /\ (LSeg (h,m));

assume A75: (LSeg (h,n)) /\ (LSeg (h,m)) <> {} ; :: thesis: contradiction

then A76: the Element of (LSeg (h,n)) /\ (LSeg (h,m)) in LSeg (f,n) by A74, XBOOLE_0:def 4;

A77: the Element of (LSeg (h,n)) /\ (LSeg (h,m)) in LSeg ((f /. (len f)),p) by A17, A19, A70, A75, XBOOLE_0:def 4;

LSeg (f,n) in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by A17, A57, A70, A73;

then the Element of (LSeg (h,n)) /\ (LSeg (h,m)) in L~ f by A76, TARSKI:def 4;

then the Element of (LSeg (h,n)) /\ (LSeg (h,m)) in {(f /. (len f))} by A4, A77, XBOOLE_0:def 4;

then A78: the Element of (LSeg (h,n)) /\ (LSeg (h,m)) = f /. (len f) by TARSKI:def 1;

A79: (n + 1) + 1 <= len f by A17, A57, A70, NAT_1:13;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( (n + 1) + 1 = len f or (n + 1) + 1 < len f )
by A79, XXREAL_0:1;

end;

suppose A80:
(n + 1) + 1 = len f
; :: thesis: contradiction

1 <= n + 1
by NAT_1:11;

then A81: f /. (len f) in LSeg (f,(n + 1)) by A80, TOPREAL1:21;

(LSeg (f,n)) /\ (LSeg (f,(n + 1))) = {(f /. (n + 1))} by A8, A59, A73, A80;

then f /. (len f) in {(f /. (n + 1))} by A76, A78, A81, XBOOLE_0:def 4;

then f /. (len f) = f /. (n + 1) by TARSKI:def 1;

then (len f) + 1 = len f by A15, A7, A72, A80, PARTFUN2:10;

hence contradiction ; :: thesis: verum

end;then A81: f /. (len f) in LSeg (f,(n + 1)) by A80, TOPREAL1:21;

(LSeg (f,n)) /\ (LSeg (f,(n + 1))) = {(f /. (n + 1))} by A8, A59, A73, A80;

then f /. (len f) in {(f /. (n + 1))} by A76, A78, A81, XBOOLE_0:def 4;

then f /. (len f) = f /. (n + 1) by TARSKI:def 1;

then (len f) + 1 = len f by A15, A7, A72, A80, PARTFUN2:10;

hence contradiction ; :: thesis: verum

suppose A82:
(n + 1) + 1 < len f
; :: thesis: contradiction

reconsider j = (len f) - 1 as Element of NAT by A13, INT_1:5, XXREAL_0:2;

(n + 2) + 1 <= len f by A82, NAT_1:13;

then n + 2 <= (len f) - 1 by XREAL_1:19;

then n + 1 < j by A59, NAT_1:13;

then LSeg (f,n) misses LSeg (f,j) by A10;

then A83: (LSeg (f,n)) /\ (LSeg (f,j)) = {} ;

(1 + 1) - 1 = 1 ;

then ( j + 1 = len f & 1 <= j ) by A13, XREAL_1:13;

then f /. (len f) in LSeg (f,j) by TOPREAL1:21;

hence contradiction by A76, A78, A83, XBOOLE_0:def 4; :: thesis: verum

end;(n + 2) + 1 <= len f by A82, NAT_1:13;

then n + 2 <= (len f) - 1 by XREAL_1:19;

then n + 1 < j by A59, NAT_1:13;

then LSeg (f,n) misses LSeg (f,j) by A10;

then A83: (LSeg (f,n)) /\ (LSeg (f,j)) = {} ;

(1 + 1) - 1 = 1 ;

then ( j + 1 = len f & 1 <= j ) by A13, XREAL_1:13;

then f /. (len f) in LSeg (f,j) by TOPREAL1:21;

hence contradiction by A76, A78, A83, XBOOLE_0:def 4; :: thesis: verum

hereby :: according to TOPREAL1:def 5 :: thesis: verum

let n be Nat; :: thesis: ( 1 <= n & n + 1 <= len h & not (h /. n) `1 = (h /. (n + 1)) `1 implies (h /. n) `2 = (h /. (n + 1)) `2 )

assume that

A84: 1 <= n and

A85: n + 1 <= len h ; :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )

set p3 = h /. n;

set p4 = h /. (n + 1);

end;assume that

A84: 1 <= n and

A85: n + 1 <= len h ; :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )

set p3 = h /. n;

set p4 = h /. (n + 1);

now :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )end;

hence
( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )
; :: thesis: verumper cases
( n + 1 = len h or n + 1 < len h )
by A85, XXREAL_0:1;

end;

suppose
n + 1 = len h
; :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )

hence
( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )
by A1, A5, A17, A16, FINSEQ_4:67; :: thesis: verum

end;suppose A86:
n + 1 < len h
; :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )

A87:
1 <= n + 1
by A84, NAT_1:13;

n + 1 <= len f by A17, A86, NAT_1:13;

then n + 1 in dom f by A12, A87, FINSEQ_1:1;

then A88: h /. (n + 1) = f /. (n + 1) by A5, FINSEQ_4:68;

n <= len f by A17, A86, XREAL_1:6;

then n in dom f by A12, A84, FINSEQ_1:1;

then A89: h /. n = f /. n by A5, FINSEQ_4:68;

n + 1 <= len f by A17, A86, NAT_1:13;

hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) by A20, A84, A89, A88; :: thesis: verum

end;n + 1 <= len f by A17, A86, NAT_1:13;

then n + 1 in dom f by A12, A87, FINSEQ_1:1;

then A88: h /. (n + 1) = f /. (n + 1) by A5, FINSEQ_4:68;

n <= len f by A17, A86, XREAL_1:6;

then n in dom f by A12, A84, FINSEQ_1:1;

then A89: h /. n = f /. n by A5, FINSEQ_4:68;

n + 1 <= len f by A17, A86, NAT_1:13;

hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) by A20, A84, A89, A88; :: thesis: verum

then h /. 1 = f /. 1 by A5, FINSEQ_4:68;

hence L~ h is_S-P_arc_joining f /. 1,p by A18, A21; :: thesis: L~ h c= (L~ f) \/ (Ball (u,r))

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L~ h or x in (L~ f) \/ (Ball (u,r)) )

assume x in L~ h ; :: thesis: x in (L~ f) \/ (Ball (u,r))

then consider X being set such that

A90: x in X and

A91: X in { (LSeg (h,m)) where m is Nat : ( 1 <= m & m + 1 <= len h ) } by TARSKI:def 4;

consider k being Nat such that

A92: X = LSeg (h,k) and

A93: 1 <= k and

A94: k + 1 <= len h by A91;

per cases
( k + 1 = len h or k + 1 < len h )
by A94, XXREAL_0:1;

end;

suppose A95:
k + 1 = len h
; :: thesis: x in (L~ f) \/ (Ball (u,r))

A96:
Ball (u,r) c= (L~ f) \/ (Ball (u,r))
by XBOOLE_1:7;

X c= Ball (u,r) by A2, A17, A19, A92, A95, TOPREAL3:21;

hence x in (L~ f) \/ (Ball (u,r)) by A90, A96; :: thesis: verum

end;X c= Ball (u,r) by A2, A17, A19, A92, A95, TOPREAL3:21;

hence x in (L~ f) \/ (Ball (u,r)) by A90, A96; :: thesis: verum

suppose
k + 1 < len h
; :: thesis: x in (L~ f) \/ (Ball (u,r))

then A97:
k + 1 <= len f
by A17, NAT_1:13;

k <= k + 1 by NAT_1:11;

then k <= len f by A97, XXREAL_0:2;

then A98: k in dom f by A12, A93, FINSEQ_1:1;

1 <= k + 1 by A93, NAT_1:13;

then k + 1 in dom f by A12, A97, FINSEQ_1:1;

then X = LSeg (f,k) by A5, A92, A98, TOPREAL3:18;

then X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by A93, A97;

then x in union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by A90, TARSKI:def 4;

hence x in (L~ f) \/ (Ball (u,r)) by XBOOLE_0:def 3; :: thesis: verum

end;k <= k + 1 by NAT_1:11;

then k <= len f by A97, XXREAL_0:2;

then A98: k in dom f by A12, A93, FINSEQ_1:1;

1 <= k + 1 by A93, NAT_1:13;

then k + 1 in dom f by A12, A97, FINSEQ_1:1;

then X = LSeg (f,k) by A5, A92, A98, TOPREAL3:18;

then X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by A93, A97;

then x in union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by A90, TARSKI:def 4;

hence x in (L~ f) \/ (Ball (u,r)) by XBOOLE_0:def 3; :: thesis: verum