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:47;
A7: f is one-to-one by A3, TOPREAL1:def 10;
A8: f is unfolded by A3, TOPREAL1:def 10;
A9: f is one-to-one by A3, TOPREAL1:def 10;
A10: f is s.n.c. by A3, TOPREAL1:def 10;
A11: Seg (len h) = dom h by FINSEQ_1:def 3;
set Mf = { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
set Mh = { (LSeg h,m) where m is Element of NAT : ( 1 <= m & m + 1 <= len h ) } ;
A12: Seg (len f) = dom f by FINSEQ_1:def 3;
A13: 2 <= len f by A3, TOPREAL1:def 10;
then A14: 1 <= len f by XXREAL_0:2;
then A15: len f in dom f by A12, FINSEQ_1:3;
then A16: h /. (len f) = f /. (len f) by A5, FINSEQ_4:83;
A17: len h = (len f) + (len <*p*>) by A5, FINSEQ_1:35
.= (len f) + 1 by FINSEQ_1:56 ;
then A18: h /. (len h) = p by A5, FINSEQ_4:82;
then A19: LSeg h,(len f) = LSeg (f /. (len f)),p by A17, A14, A16, TOPREAL1:def 5;
A20: f is special by A3, TOPREAL1:def 10;
thus A21: h is being_S-Seq :: thesis:

proof

now

set Z = { m where m is Element of NAT : ( 1 <= m & m <= len h ) } ;
given x, y being set 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 Element of NAT : ( 1 <= m & m <= len h ) } by A11, A23, FINSEQ_1:def 1;
then consider k2 being Element of NAT such that
A26: k2 = y and
A27: 1 <= k2 and
A28: k2 <= len h ;
x in { m where m is Element of NAT : ( 1 <= m & m <= len h ) } by A11, A22, FINSEQ_1:def 1;
then consider k1 being Element of 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 8
.= h /. k2 by A23, A26, PARTFUN1:def 8 ;

now

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

per cases by A34, XXREAL_0:1;

suppose k2 + 1 = k1 ; :: thesis:

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

end;

suppose k2 + 1 < k1 ; :: thesis:

then A35: k2 < ((len f) + 1) - 1 by A33, XREAL_1:22;
then k2 in dom f by A12, A27, FINSEQ_1:3;
then h /. k2 = f /. k2 by A5, FINSEQ_4:83;
hence contradiction by A5, A13, A6, A27, A32, A33, A35, FINSEQ_4:82, TOPREAL3:46; :: 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

per cases by A37, XXREAL_0:1;

suppose k1 + 1 = k2 ; :: thesis:

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

end;

suppose k1 + 1 < k2 ; :: thesis:

then A38: k1 < ((len f) + 1) - 1 by A36, XREAL_1:22;
then k1 in dom f by A12, A30, FINSEQ_1:3;
then h /. k1 = f /. k1 by A5, FINSEQ_4:83;
hence contradiction by A5, A13, A6, A30, A32, A36, A38, FINSEQ_4:82, TOPREAL3:46; :: 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:3;
k1 <= len f by A39, NAT_1:13;
then A41: k1 in dom f by A12, A30, FINSEQ_1:3;
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 8; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

proof

let j be Nat; :: according to TOPREAL1:def 8 :: 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:8;
then A45: j + 1 <= len h by A43, XXREAL_0:2;

now

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:3;
then A48: LSeg h,j = LSeg f,j by A5, A15, A47, TOPREAL3:25;
j in NAT by ORDINAL1:def 13;
then LSeg h,j in { (LSeg f,i) where i is Element of 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:92;
h /. (j + 1) in LSeg h,j by A42, A45, TOPREAL1:27;
then A50: {(h /. (j + 1))} c= LSeg h,j by ZFMISC_1:37;
LSeg h,(j + 1) = LSeg (f /. (len f)),p by A17, A14, A18, A16, A46, TOPREAL1:def 5;
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, TOPREAL1:def 8;
1 <= j + 2 by A44, NAT_1:11;
then A53: (j + 1) + 1 in dom f by A12, A51, FINSEQ_1:3;
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:3;
then A56: h /. (j + 1) = f /. (j + 1) by A5, FINSEQ_4:83;
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:3;
then LSeg h,j = LSeg f,j by A5, A55, TOPREAL3:25;
hence (LSeg h,j) /\ (LSeg h,(j + 1)) = {(h /. (j + 1))} by A5, A52, A55, A53, A56, TOPREAL3:25; :: 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 9 :: 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, TOPREAL1:def 9;
then A61: (LSeg f,n) /\ (LSeg f,m) = {} by XBOOLE_0:def 7;

now

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:3;
A66: m <= len f by A17, A62, XREAL_1:8;
then m in dom f by A12, A64, FINSEQ_1:3;
then A67: LSeg h,m = LSeg f,m by A5, A65, TOPREAL3:25;

now

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:3;
n <= len f by A58, A66, XXREAL_0:2;
then n in dom f by A12, A68, FINSEQ_1:3;
hence (LSeg h,n) /\ (LSeg h,m) = {} by A5, A61, A67, A69, TOPREAL3:25; :: thesis:

end;

suppose 0 = n ; :: thesis:

then LSeg h,n = {} by TOPREAL1:def 5;
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

per cases ;

suppose A71: 0 < n ; :: thesis:

A72: n + 1 in dom f by A17, A12, A57, A60, A70, FINSEQ_1:3;
A73: 0 + 1 <= n by A71, NAT_1:13;
then n in dom f by A17, A12, A58, A70, FINSEQ_1:3;
then A74: LSeg h,n = LSeg f,n by A5, A72, TOPREAL3:25;

now

set L = LSeg f,n;
consider x being Element of (LSeg h,n) /\ (LSeg h,m);
assume A75: (LSeg h,n) /\ (LSeg h,m) <> {} ; :: thesis:
then A76: x in LSeg f,n by A74, XBOOLE_0:def 4;
A77: x in LSeg (f /. (len f)),p by A17, A19, A70, A75, XBOOLE_0:def 4;
n in NAT by ORDINAL1:def 13;
then LSeg f,n in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A17, A57, A70, A73;
then x in L~ f by A76, TARSKI:def 4;
then x in {(f /. (len f))} by A4, A77, XBOOLE_0:def 4;
then A78: x = f /. (len f) by TARSKI:def 1;
A79: (n + 1) + 1 <= len f by A17, A57, A70, NAT_1:13;

now

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:27;
(LSeg f,n) /\ (LSeg f,(n + 1)) = {(f /. (n + 1))} by A8, A59, A73, A80, TOPREAL1:def 8;
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:17;
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:18, XXREAL_0:2;
(n + 2) + 1 <= len f by A82, NAT_1:13;
then n + 2 <= (len f) - 1 by XREAL_1:21;
then n + 1 < j by A59, NAT_1:13;
then LSeg f,n misses LSeg f,j by A10, TOPREAL1:def 9;
then A83: (LSeg f,n) /\ (LSeg f,j) = {} by XBOOLE_0:def 7;
(1 + 1) - 1 = 1 ;
then ( j + 1 = len f & 1 <= j ) by A13, XREAL_1:15;
then f /. (len f) in LSeg f,j by TOPREAL1:27;
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 5;
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 5;
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 7 :: 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

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:82; :: 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:3;
then A88: h /. (n + 1) = f /. (n + 1) by A5, FINSEQ_4:83;
n <= len f by A17, A86, XREAL_1:8;
then n in dom f by A12, A84, FINSEQ_1:3;
then A89: h /. n = f /. n by A5, FINSEQ_4:83;
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, TOPREAL1:def 7; :: 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:3;
then h /. 1 = f /. 1 by A5, FINSEQ_4:83;
hence L~ h is_S-P_arc_joining f /. 1,p by A18, A21, Def1; :: thesis:
let x be set ; :: 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 Element of NAT : ( 1 <= m & m + 1 <= len h ) } by TARSKI:def 4;
consider k being Element of 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:28;
hence x in (L~ f) \/ (Ball u,r) by A90, A96, TARSKI:def 3; :: 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:3;
1 <= k + 1 by A93, NAT_1:13;
then k + 1 in dom f by A12, A97, FINSEQ_1:3;
then X = LSeg f,k by A5, A92, A98, TOPREAL3:25;
then X in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A93, A97;
then x in union { (LSeg f,i) where i is Element of 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;