let p be Point of (); :: thesis: for f, h being FinSequence of ()
for r being Real
for u being Point of () 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 (); :: thesis: for r being Real
for u being Point of () 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 () 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 (); :: 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 ;
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 ;
then A16: h /. (len f) = f /. (len f) by ;
A17: len h = (len f) + () by
.= (len f) + 1 by FINSEQ_1:39 ;
then A18: h /. (len h) = p by ;
then A19: LSeg (h,(len f)) = LSeg ((f /. (len f)),p) by ;
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
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 )
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 ;
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 ;
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
.= h /. k2 by ;
now :: thesis: contradiction
per 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 ;
suppose ( k1 = (len f) + 1 & k2 = (len f) + 1 ) ; :: thesis: contradiction
end;
suppose A33: ( k1 = (len f) + 1 & k2 < (len f) + 1 ) ; :: thesis: contradiction
then A34: k2 + 1 <= k1 by NAT_1:13;
now :: thesis: contradiction
per cases ( k2 + 1 = k1 or k2 + 1 < k1 ) by ;
suppose k2 + 1 < k1 ; :: thesis: contradiction
then A35: k2 < ((len f) + 1) - 1 by ;
reconsider k2 = k2 as Element of NAT by ORDINAL1:def 12;
k2 in dom f by ;
then h /. k2 = f /. k2 by ;
hence contradiction by A5, A13, A6, A27, A32, A33, A35, FINSEQ_4:67, TOPREAL3:39; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose A36: ( k1 < (len f) + 1 & k2 = (len f) + 1 ) ; :: thesis: contradiction
then A37: k1 + 1 <= k2 by NAT_1:13;
now :: thesis: contradiction
per cases ( k1 + 1 = k2 or k1 + 1 < k2 ) by ;
suppose k1 + 1 < k2 ; :: thesis: contradiction
then A38: k1 < ((len f) + 1) - 1 by ;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;
k1 in dom f by ;
then h /. k1 = f /. k1 by ;
hence contradiction by A5, A13, A6, A30, A32, A36, A38, FINSEQ_4:67, TOPREAL3:39; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
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 ;
k1 <= len f by ;
then A41: k1 in dom f by ;
then f . k1 = h . k1 by
.= f . k2 by ;
hence contradiction by A9, A25, A29, A26, A41, A40, FUNCT_1:def 4; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
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 )
2 + 1 <= (len f) + 1 by ;
hence len h >= 2 by ; :: 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
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 ;
now :: thesis: (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))}
per cases ( j + 2 = len h or j + 2 < len h ) by ;
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 ;
then A48: LSeg (h,j) = LSeg (f,j) by ;
LSeg (h,j) in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by ;
then A49: LSeg (h,j) = (LSeg (h,j)) /\ (L~ f) by ;
h /. (j + 1) in LSeg (h,j) by ;
then A50: {(h /. (j + 1))} c= LSeg (h,j) by ZFMISC_1:31;
LSeg (h,(j + 1)) = LSeg ((f /. (len f)),p) by ;
hence (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = (LSeg (h,j)) /\ {(h /. (j + 1))} by
.= {(h /. (j + 1))} by ;
:: thesis: verum
end;
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 ;
then A52: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A8, A42, A43;
1 <= j + 2 by ;
then A53: (j + 1) + 1 in dom f by ;
j + 1 <= j + 2 by ;
then A54: j + 1 <= len f by ;
1 <= j + 1 by NAT_1:11;
then A55: j + 1 in dom f by ;
then A56: h /. (j + 1) = f /. (j + 1) by ;
j <= j + 1 by NAT_1:11;
then j <= len f by ;
then j in dom f by ;
then LSeg (h,j) = LSeg (f,j) by ;
hence (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} by ; :: thesis: verum
end;
end;
end;
hence (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} ; :: thesis: verum
end;
thus h is s.n.c. :: thesis: h is special
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 ;
A59: (n + 1) + 1 = n + (1 + 1) ;
A60: 1 <= n + 1 by NAT_1:11;
LSeg (f,n) misses LSeg (f,m) by ;
then A61: (LSeg (f,n)) /\ (LSeg (f,m)) = {} ;
now :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}
per cases ( m + 1 < len h or m + 1 = len h or m + 1 > len h ) by XXREAL_0:1;
suppose A62: m + 1 < len h ; :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}
then A63: m + 1 <= len f by ;
A64: 1 < m by ;
then 1 <= m + 1 by NAT_1:13;
then A65: m + 1 in dom f by ;
A66: m <= len f by ;
then m in dom f by ;
then A67: LSeg (h,m) = LSeg (f,m) by ;
now :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}
per cases ( 0 < n or 0 = n ) ;
suppose 0 < n ; :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}
then A68: 0 + 1 <= n by NAT_1:13;
n + 1 <= len f by ;
then A69: n + 1 in dom f by ;
n <= len f by ;
then n in dom f by ;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} by ; :: thesis: verum
end;
suppose 0 = n ; :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}
then LSeg (h,n) = {} by TOPREAL1:def 3;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: thesis: verum
end;
end;
end;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: thesis: verum
end;
suppose A70: m + 1 = len h ; :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}
now :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}
per cases ( 0 < n or 0 = n ) ;
suppose A71: 0 < n ; :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}
A72: n + 1 in dom f by ;
A73: 0 + 1 <= n by ;
then n in dom f by ;
then A74: LSeg (h,n) = LSeg (f,n) by ;
now :: thesis: not (LSeg (h,n)) /\ (LSeg (h,m)) <> {}
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: contradiction
then A76: the Element of (LSeg (h,n)) /\ (LSeg (h,m)) in LSeg (f,n) by ;
A77: the Element of (LSeg (h,n)) /\ (LSeg (h,m)) in LSeg ((f /. (len f)),p) by ;
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 ;
then the Element of (LSeg (h,n)) /\ (LSeg (h,m)) in {(f /. (len f))} by ;
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 ;
now :: thesis: contradiction
per cases ) + 1 = len f or (n + 1) + 1 < len f ) by ;
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 ;
(LSeg (f,n)) /\ (LSeg (f,(n + 1))) = {(f /. (n + 1))} by A8, A59, A73, A80;
then f /. (len f) in {(f /. (n + 1))} by ;
then f /. (len f) = f /. (n + 1) by TARSKI:def 1;
then (len f) + 1 = len f by ;
hence contradiction ; :: thesis: verum
end;
suppose A82: (n + 1) + 1 < len f ; :: thesis: contradiction
reconsider j = (len f) - 1 as Element of NAT by ;
(n + 2) + 1 <= len f by ;
then n + 2 <= (len f) - 1 by XREAL_1:19;
then n + 1 < j by ;
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 ;
then f /. (len f) in LSeg (f,j) by TOPREAL1:21;
hence contradiction by A76, A78, A83, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: thesis: verum
end;
suppose 0 = n ; :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}
then LSeg (h,n) = {} by TOPREAL1:def 3;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: thesis: verum
end;
end;
end;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: thesis: verum
end;
suppose m + 1 > len h ; :: thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {}
then LSeg (h,m) = {} by TOPREAL1:def 3;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: thesis: verum
end;
end;
end;
hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: according to XBOOLE_0:def 7 :: thesis: verum
end;
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);
now :: thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )
per cases ( n + 1 = len h or n + 1 < len h ) by ;
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 ; :: 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 ;
n + 1 <= len f by ;
then n + 1 in dom f by ;
then A88: h /. (n + 1) = f /. (n + 1) by ;
n <= len f by ;
then n in dom f by ;
then A89: h /. n = f /. n by ;
n + 1 <= len f by ;
hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) by A20, A84, A89, A88; :: thesis: verum
end;
end;
end;
hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) ; :: thesis: verum
end;
end;
1 in dom f by ;
then h /. 1 = f /. 1 by ;
hence L~ h is_S-P_arc_joining f /. 1,p by ; :: 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 ;
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 ;
hence x in (L~ f) \/ (Ball (u,r)) by ; :: thesis: verum
end;
suppose k + 1 < len h ; :: thesis: x in (L~ f) \/ (Ball (u,r))
then A97: k + 1 <= len f by ;
k <= k + 1 by NAT_1:11;
then k <= len f by ;
then A98: k in dom f by ;
1 <= k + 1 by ;
then k + 1 in dom f by ;
then X = LSeg (f,k) by ;
then X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by ;
then x in union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by ;
hence x in (L~ f) \/ (Ball (u,r)) by XBOOLE_0:def 3; :: thesis: verum
end;
end;