let p be Point of (TOP-REAL 2); :: thesis:
let f, h be FinSequence of (TOP-REAL 2); :: thesis:
let r be Real; :: thesis:
let u be Point of (Euclid 2); :: thesis:
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:
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:
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:

proof

now :: thesis:

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:
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:

per cases by A17, A31, A28, XXREAL_0:1;

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

hence contradiction by A25, A29, A26; :: thesis:

end;

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

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

now :: thesis:

per cases by A34, XXREAL_0:1;

suppose k2 + 1 = k1 ; :: thesis:

hence contradiction by A1, A5, A16, A32, A33, FINSEQ_4:67; :: thesis:

end;

suppose k2 + 1 < k1 ; :: thesis:

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:

end;

hence contradiction ; :: thesis:

end;

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

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

now :: thesis:

per cases by A37, XXREAL_0:1;

suppose k1 + 1 = k2 ; :: thesis:

hence contradiction by A1, A5, A16, A32, A36, FINSEQ_4:67; :: thesis:

end;

suppose k1 + 1 < k2 ; :: thesis:

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:

end;

hence contradiction ; :: thesis:

end;

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

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:

end;

hence contradiction ; :: thesis:

end;

hence h is one-to-one by FUNCT_1:def 4; :: according to TOPREAL1:def 8 :: thesis:
2 + 1 <= (len f) + 1 by A13, XREAL_1:6;
hence len h >= 2 by A17, XXREAL_0:2; :: thesis:
thus h is unfolded :: thesis:

proof

let j be Nat; :: according to TOPREAL1:def 6 :: thesis:
assume that
A42: 1 <= j and
A43: j + 2 <= len h ; :: thesis:
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:

per cases by A43, XXREAL_0:1;

suppose A46: j + 2 = len h ; :: thesis:

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:

end;

suppose j + 2 < len h ; :: thesis:

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:

end;

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

end;

thus h is s.n.c. :: thesis:

proof

let n, m be Nat; :: according to TOPREAL1:def 7 :: thesis:
assume A57: m > n + 1 ; :: thesis:
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:

per cases by XXREAL_0:1;

suppose A62: m + 1 < len h ; :: thesis:

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;

now :: thesis:

per cases ;

suppose 0 < n ; :: thesis:

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:

end;

suppose 0 = n ; :: thesis:

then LSeg (h,n) = {} by TOPREAL1:def 3;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: thesis:

end;

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

end;

suppose A70: m + 1 = len h ; :: thesis:

now :: thesis:

per cases ;

suppose A71: 0 < n ; :: thesis:

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;

now :: thesis:

set L = LSeg (f,n);
set x = the Element of (LSeg (h,n)) /\ (LSeg (h,m));
assume A75: (LSeg (h,n)) /\ (LSeg (h,m)) <> {} ; :: thesis:
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:

per cases ) + 1 = len f or (n + 1) + 1 < len f ) by A79, XXREAL_0:1;

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

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:

end;

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

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:

end;

hence contradiction ; :: thesis:

end;

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

end;

suppose 0 = n ; :: thesis:

then LSeg (h,n) = {} by TOPREAL1:def 3;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: thesis:

end;

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

end;

suppose m + 1 > len h ; :: thesis:

then LSeg (h,m) = {} by TOPREAL1:def 3;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: thesis:

end;

hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: according to XBOOLE_0:def 7 :: thesis:

end;

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

let n be Nat; :: thesis:
assume that
A84: 1 <= n and
A85: n + 1 <= len h ; :: thesis:
set p3 = h /. n;
set p4 = h /. (n + 1);

now :: thesis:

per cases by A85, XXREAL_0:1;

suppose n + 1 = len h ; :: thesis:

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:

end;

suppose A86: n + 1 < len h ; :: thesis:

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:

end;

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

end;

1 in dom f by A12, A14, FINSEQ_1:1;
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:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in L~ h ; :: thesis:
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 by A94, XXREAL_0:1;

suppose A95: k + 1 = len h ; :: thesis:

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:

end;

suppose k + 1 < len h ; :: thesis:

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:

end;