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 A2: ( not f /. 1 in Ball u,r & 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*> ) ; :: thesis:
then A3: len h = (len f) + (len <*p*>) by FINSEQ_1:35
.= (len f) + 1 by FINSEQ_1:56 ;
A4: f is s.n.c. by A2, TOPREAL1:def 10;
A5: f is unfolded by A2, TOPREAL1:def 10;
A6: f is special by A2, TOPREAL1:def 10;
A7: ( Seg (len f) = dom f & Seg (len h) = dom h ) by FINSEQ_1:def 3;
A8: 2 <= len f by A2, TOPREAL1:def 10;
then A9: ( 1 <= len f & 2 <= len f ) by XXREAL_0:2;
then 1 in dom f by A7, FINSEQ_1:3;
then A10: ( h /. 1 = f /. 1 & h /. (len h) = p & f is one-to-one & p <> f /. (len f) ) by A1, A2, A3, FINSEQ_4:82, FINSEQ_4:83, TOPREAL1:def 10;
A11: ( not p in L~ f & len f in dom f ) by A1, A2, A7, A9, FINSEQ_1:3, TOPREAL3:47;
then A12: h /. (len f) = f /. (len f) by A2, FINSEQ_4:83;
then A13: LSeg h,(len f) = LSeg (f /. (len f)),p by A3, A9, A10, TOPREAL1:def 5;
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 ) } ;
A14: ( L~ f = union { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } & f is one-to-one ) by A2, TOPREAL1:def 10;
thus 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 A15: ( x in dom h & y in dom h & h . x = h . y & x <> y ) ; :: thesis:
x in { m where m is Element of NAT : ( 1 <= m & m <= len h ) } by A7, A15, FINSEQ_1:def 1;
then consider k1 being Element of NAT such that
A16: ( k1 = x & 1 <= k1 & k1 <= len h ) ;
y in { m where m is Element of NAT : ( 1 <= m & m <= len h ) } by A7, A15, FINSEQ_1:def 1;
then consider k2 being Element of NAT such that
A17: ( k2 = y & 1 <= k2 & k2 <= len h ) ;
A18: h /. k1 = h . y by A15, A16, PARTFUN1:def 8
.= h /. k2 by A15, A17, PARTFUN1:def 8 ;

now

per cases by A3, A16, A17, XXREAL_0:1;

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

hence contradiction by A15, A16, A17; :: thesis:

end;

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

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

now

per cases by A20, XXREAL_0:1;

suppose k2 + 1 = k1 ; :: thesis:

hence contradiction by A1, A2, A12, A18, A19, FINSEQ_4:82; :: thesis:

end;

suppose k2 + 1 < k1 ; :: thesis:

then A21: k2 < ((len f) + 1) - 1 by A19, XREAL_1:22;
then k2 in dom f by A7, A17, FINSEQ_1:3;
then ( f /. k2 <> p & h /. k2 = f /. k2 & h /. k1 = p ) by A2, A8, A11, A17, A19, A21, FINSEQ_4:82, FINSEQ_4:83, TOPREAL3:46;
hence contradiction by A18; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

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

now

per cases by A23, XXREAL_0:1;

suppose k1 + 1 = k2 ; :: thesis:

hence contradiction by A1, A2, A12, A18, A22, FINSEQ_4:82; :: thesis:

end;

suppose k1 + 1 < k2 ; :: thesis:

then A24: k1 < ((len f) + 1) - 1 by A22, XREAL_1:22;
then k1 in dom f by A7, A16, FINSEQ_1:3;
then ( f /. k1 <> p & h /. k1 = f /. k1 & h /. k2 = p ) by A2, A8, A11, A16, A22, A24, FINSEQ_4:82, FINSEQ_4:83, TOPREAL3:46;
hence contradiction by A18; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

then ( k1 <= len f & k2 <= len f ) by NAT_1:13;
then A25: ( k1 in dom f & k2 in dom f ) by A7, A16, A17, FINSEQ_1:3;
then f . k1 = h . k1 by A2, FINSEQ_1:def 7
.= f . k2 by A2, A15, A16, A17, A25, FINSEQ_1:def 7 ;
hence contradiction by A10, A15, A16, A17, A25, 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 A8, XREAL_1:8;
hence len h >= 2 by A3, XXREAL_0:2; :: thesis:
thus h is unfolded :: thesis:

proof

let j be Nat; :: according to TOPREAL1:def 8 :: thesis:
assume A26: ( 1 <= j & j + 2 <= len h ) ; :: thesis:
A27: j + (1 + 1) = (j + 1) + 1 ;
j + 1 <= j + 2 by XREAL_1:8;
then A28: j + 1 <= len h by A26, XXREAL_0:2;

now

per cases by A26, XXREAL_0:1;

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

then A30: j + ((1 + 1) - 1) = len f by A3;
then j <= len f by NAT_1:13;
then j in dom f by A7, A26, FINSEQ_1:3;
then A31: ( LSeg h,j = LSeg f,j & LSeg h,(j + 1) = LSeg (f /. (len f)),p ) by A2, A3, A9, A10, A11, A12, A30, TOPREAL1:def 5, TOPREAL3:25;
h /. (j + 1) in LSeg h,j by A26, A28, TOPREAL1:27;
then A32: {(h /. (j + 1))} c= LSeg h,j by ZFMISC_1:37;
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 A3, A26, A29, A31;
then LSeg h,j = (LSeg h,j) /\ (L~ f) by XBOOLE_1:28, ZFMISC_1:92;
hence (LSeg h,j) /\ (LSeg h,(j + 1)) = (LSeg h,j) /\ {(h /. (j + 1))} by A2, A3, A12, A29, A31, XBOOLE_1:16
.= {(h /. (j + 1))} by A32, XBOOLE_1:28 ;
:: thesis:

end;

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

then A33: (j + (2 + 1)) - 1 <= len f by A3, NAT_1:13;
then A34: (LSeg f,j) /\ (LSeg f,(j + 1)) = {(f /. (j + 1))} by A5, A26, TOPREAL1:def 8;
( j <= j + 1 & j + 1 <= j + 2 ) by A27, NAT_1:11;
then ( 1 <= j + 1 & j <= j + 1 & j + 1 <= j + 2 & j + 1 <= len f ) by A26, A33, XXREAL_0:2;
then ( 1 <= j + 1 & 1 <= j + 2 & j <= len f & j + 1 <= len f ) by XXREAL_0:2;
then A35: ( j in dom f & j + 1 in dom f & (j + 1) + 1 in dom f ) by A7, A26, A33, FINSEQ_1:3;
then ( h /. (j + 1) = f /. (j + 1) & LSeg h,j = LSeg f,j ) by A2, FINSEQ_4:83, TOPREAL3:25;
hence (LSeg h,j) /\ (LSeg h,(j + 1)) = {(h /. (j + 1))} by A2, A34, A35, 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 A36: m > n + 1 ; :: thesis:
A37: (n + 1) + 1 = n + (1 + 1) ;
A38: ( n + 1 < m & n <= n + 1 ) by A36, NAT_1:11;
LSeg f,n misses LSeg f,m by A4, A36, TOPREAL1:def 9;
then A39: ( n <= m & n + 1 <= m & 1 <= n + 1 & (LSeg f,n) /\ (LSeg f,m) = {} ) by A38, NAT_1:11, XBOOLE_0:def 7, XXREAL_0:2;

now

per cases by XXREAL_0:1;

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

then A40: ( m <= len f & m + 1 <= len f & m <= m + 1 & 1 < m ) by A3, A36, A39, NAT_1:13, XREAL_1:8, XXREAL_0:2;
then A41: ( m in dom f & 1 <= m + 1 ) by A7, FINSEQ_1:3, XXREAL_0:2;
then m + 1 in dom f by A7, A40, FINSEQ_1:3;
then A42: LSeg h,m = LSeg f,m by A2, A41, TOPREAL3:25;

now

per cases ;

suppose 0 < n ; :: thesis:

then A43: 0 + 1 <= n by NAT_1:13;
( n <= len f & n + 1 <= len f ) by A39, A40, XXREAL_0:2;
then ( n in dom f & n + 1 in dom f ) by A7, A39, A43, FINSEQ_1:3;
hence (LSeg h,n) /\ (LSeg h,m) = {} by A2, A39, A42, 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 A44: m + 1 = len h ; :: thesis:

now

per cases ;

suppose 0 < n ; :: thesis:

then A45: 0 + 1 <= n by NAT_1:13;
then A46: ( n in dom f & n + 1 in dom f ) by A3, A7, A39, A44, FINSEQ_1:3;
then A47: LSeg h,n = LSeg f,n by A2, TOPREAL3:25;

now

assume A48: (LSeg h,n) /\ (LSeg h,m) <> {} ; :: thesis:
consider x being Element of (LSeg h,n) /\ (LSeg h,m);
set L = LSeg f,n;
A49: ( x in LSeg (f /. (len f)),p & x in LSeg f,n & n + 1 <= len f ) by A3, A13, A36, A44, A47, A48, 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 A3, A36, A44, A45;
then x in L~ f by A49, TARSKI:def 4;
then x in {(f /. (len f))} by A2, A49, XBOOLE_0:def 4;
then A50: ( x = f /. (len f) & (n + 1) + 1 <= len f ) by A3, A36, A44, NAT_1:13, TARSKI:def 1;

now

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

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

then A52: (LSeg f,n) /\ (LSeg f,(n + 1)) = {(f /. (n + 1))} by A5, A37, A45, TOPREAL1:def 8;
1 <= n + 1 by NAT_1:11;
then f /. (len f) in LSeg f,(n + 1) by A51, TOPREAL1:27;
then f /. (len f) in {(f /. (n + 1))} by A49, A50, A52, XBOOLE_0:def 4;
then f /. (len f) = f /. (n + 1) by TARSKI:def 1;
then (len f) + 1 = len f by A11, A14, A46, A51, PARTFUN2:17;
hence contradiction ; :: thesis:

end;

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

then (n + 2) + 1 <= len f by NAT_1:13;
then A53: n + 2 <= (len f) - 1 by XREAL_1:21;
reconsider j = (len f) - 1 as Element of NAT by A8, INT_1:18, XXREAL_0:2;
n + 1 < j by A37, A53, NAT_1:13;
then A54: ( LSeg f,n misses LSeg f,j & j + 1 = len f ) by A4, TOPREAL1:def 9;
then A55: ( (LSeg f,n) /\ (LSeg f,j) = {} & j + 1 = len f ) by XBOOLE_0:def 7;
(1 + 1) - 1 = 1 ;
then 1 <= j by A8, XREAL_1:15;
then f /. (len f) in LSeg f,j by A54, TOPREAL1:27;
hence contradiction by A49, A50, A55, 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 A56: ( 1 <= n & n + 1 <= len h ) ; :: thesis:
set p3 = h /. n;
set p4 = h /. (n + 1);

now

per cases by A56, 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, A2, A3, A12, FINSEQ_4:82; :: thesis:

end;

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

then ( n <= len f & n + 1 <= len f & n <= n + 1 ) by A3, NAT_1:13, XREAL_1:8;
then ( n in dom f & n + 1 <= len f & 1 <= n + 1 ) by A7, A56, FINSEQ_1:3, XXREAL_0:2;
then ( n in dom f & n + 1 in dom f ) by A7, FINSEQ_1:3;
then ( h /. n = f /. n & h /. (n + 1) = f /. (n + 1) & n + 1 <= len f ) by A2, A3, A57, FINSEQ_4:83, NAT_1:13;
hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) by A6, A56, TOPREAL1:def 7; :: thesis:

end;

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

end;

hence L~ h is_S-P_arc_joining f /. 1,p by A10, 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
A58: ( x in X & 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
A59: ( X = LSeg h,k & 1 <= k & k + 1 <= len h ) by A58;

per cases by A59, XXREAL_0:1;

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

then ( X c= Ball u,r & Ball u,r c= (L~ f) \/ (Ball u,r) ) by A2, A3, A13, A59, TOPREAL3:28, XBOOLE_1:7;
hence x in (L~ f) \/ (Ball u,r) by A58, TARSKI:def 3; :: thesis:

end;

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

then A61: ( k + 1 < (len f) + 1 & k <= k + 1 ) by A3, NAT_1:11;
A62: ( k + 1 <= len f & 1 <= k + 1 ) by A3, A59, A60, NAT_1:13;
then A63: ( k + 1 in dom f & k <= len f ) by A7, A61, FINSEQ_1:3, XXREAL_0:2;
then k in dom f by A7, A59, FINSEQ_1:3;
then X = LSeg f,k by A2, A59, A63, TOPREAL3:25;
then X in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A59, A62;
then x in union { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A58, TARSKI:def 4;
hence x in (L~ f) \/ (Ball u,r) by XBOOLE_0:def 3; :: thesis:

end;