let f, g be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . 1 & g = (mid (f,1,(Index (p,f)))) ^ <*p*> holds
g is_S-Seq_joining f /. 1,p
let p be Point of (TOP-REAL 2); :: thesis: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . 1 & g = (mid (f,1,(Index (p,f)))) ^ <*p*> implies g is_S-Seq_joining f /. 1,p )
assume that
A1: ( f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. ) and
A2: p in L~ f and
A3: p <> f . 1 and
A4: g = (mid (f,1,(Index (p,f)))) ^ <*p*> ; :: thesis: g is_S-Seq_joining f /. 1,p
A5: Index (p,f) < len f by A2, JORDAN3:8;
A6: for j1, j2 being Nat st j1 + 1 < j2 holds
LSeg (g,j1) misses LSeg (g,j2)

proof

let j1, j2 be Nat; :: thesis: ( j1 + 1 < j2 implies LSeg (g,j1) misses LSeg (g,j2) )
assume A7: j1 + 1 < j2 ; :: thesis: LSeg (g,j1) misses LSeg (g,j2)
j1 >= 0 by NAT_1:2;
then A8: ( j1 = 0 or j1 >= 0 + 1 ) by NAT_1:13;

now :: thesis: ( ( j1 = 0 & LSeg (g,j1) misses LSeg (g,j2) ) or ( ( j1 = 1 or j1 > 1 ) & j2 + 1 <= len g & LSeg (g,j1) misses LSeg (g,j2) ) or ( j2 + 1 > len g & LSeg (g,j1) misses LSeg (g,j2) ) )

per cases ( j1 = 0 or ( ( j1 = 1 or j1 > 1 ) & j2 + 1 <= len g ) or j2 + 1 > len g ) by A8, XXREAL_0:1;

case j1 = 0 ; :: thesis: LSeg (g,j1) misses LSeg (g,j2)

then LSeg (g,j1) = {} by TOPREAL1:def 3;
then (LSeg (g,j1)) /\ (LSeg (g,j2)) = {} ;
hence LSeg (g,j1) misses LSeg (g,j2) ; :: thesis: verum

end;

case that A9: ( j1 = 1 or j1 > 1 ) and
A10: j2 + 1 <= len g ; :: thesis: LSeg (g,j1) misses LSeg (g,j2)

j2 < len g by A10, NAT_1:13;
then j1 + 1 < len g by A7, XXREAL_0:2;
then A11: LSeg (g,j1) c= LSeg (f,j1) by A2, A4, A9, JORDAN3:18;
1 + 1 <= j1 + 1 by A9, XREAL_1:6;
then 2 <= j2 by A7, XXREAL_0:2;
then 1 <= j2 by XXREAL_0:2;
then A12: LSeg (g,j2) c= LSeg (f,j2) by A2, A4, A10, JORDAN3:18;
LSeg (f,j1) misses LSeg (f,j2) by A1, A7, TOPREAL1:def 7;
then (LSeg (f,j1)) /\ (LSeg (f,j2)) = {} ;
then (LSeg (g,j1)) /\ (LSeg (g,j2)) = {} by A11, A12, XBOOLE_1:3, XBOOLE_1:27;
hence LSeg (g,j1) misses LSeg (g,j2) ; :: thesis: verum

end;

case j2 + 1 > len g ; :: thesis: LSeg (g,j1) misses LSeg (g,j2)

then LSeg (g,j2) = {} by TOPREAL1:def 3;
then (LSeg (g,j1)) /\ (LSeg (g,j2)) = {} ;
hence LSeg (g,j1) misses LSeg (g,j2) ; :: thesis: verum

end;

end;

end;

hence LSeg (g,j1) misses LSeg (g,j2) ; :: thesis: verum

end;

A13: len g = (len (mid (f,1,(Index (p,f))))) + (len <*p*>) by A4, FINSEQ_1:22
.= (len (mid (f,1,(Index (p,f))))) + 1 by FINSEQ_1:39 ;
consider i being Nat such that
1 <= i and
A14: i + 1 <= len f and
p in LSeg (f,i) by A2, SPPOL_2:13;
A15: 1 <= Index (p,f) by A2, JORDAN3:8;
1 <= 1 + i by NAT_1:12;
then A16: 1 <= len f by A14, XXREAL_0:2;
then A17: len (mid (f,1,(Index (p,f)))) = ((Index (p,f)) -' 1) + 1 by A15, A5, FINSEQ_6:118;
then A18: len (mid (f,1,(Index (p,f)))) = Index (p,f) by A2, JORDAN3:8, XREAL_1:235;
then g . 1 = (mid (f,1,(Index (p,f)))) . 1 by A4, A15, FINSEQ_6:109;
then g . 1 = f . 1 by A15, A5, A16, FINSEQ_6:118;
then A19: g . 1 = f /. 1 by A16, FINSEQ_4:15;
A20: for j being Nat st 1 <= j & j + 2 <= len g holds
(LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))}

proof

let j be Nat; :: thesis: ( 1 <= j & j + 2 <= len g implies (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} )
assume that
A21: 1 <= j and
A22: j + 2 <= len g ; :: thesis: (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))}
A23: j + 1 <= len g by A22, NAT_D:47;
then LSeg (g,j) = LSeg ((g /. j),(g /. (j + 1))) by A21, TOPREAL1:def 3;
then A24: g /. (j + 1) in LSeg (g,j) by RLTOPSP1:68;
A25: 1 <= j + 1 by A21, NAT_D:48;
then LSeg (g,(j + 1)) = LSeg ((g /. (j + 1)),(g /. ((j + 1) + 1))) by A22, TOPREAL1:def 3;
then g /. (j + 1) in LSeg (g,(j + 1)) by RLTOPSP1:68;
then g /. (j + 1) in (LSeg (g,j)) /\ (LSeg (g,(j + 1))) by A24, XBOOLE_0:def 4;
then A26: {(g /. (j + 1))} c= (LSeg (g,j)) /\ (LSeg (g,(j + 1))) by ZFMISC_1:31;
j + 1 <= len g by A22, NAT_D:47;
then A27: LSeg (g,j) c= LSeg (f,j) by A2, A4, A21, JORDAN3:18;
A28: Index (p,f) <= len f by A2, JORDAN3:8;
A29: (j + 1) + 1 <= len g by A22;
then LSeg (g,(j + 1)) c= LSeg (f,(j + 1)) by A2, A4, A25, JORDAN3:18;
then A30: (LSeg (g,j)) /\ (LSeg (g,(j + 1))) c= (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by A27, XBOOLE_1:27;
A31: g /. (j + 1) = g . (j + 1) by A25, A23, FINSEQ_4:15;

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

A32: len g = (len (mid (f,1,(Index (p,f))))) + 1 by A4, FINSEQ_2:16;
Index (p,f) <= len f by A2, JORDAN3:8;
then A33: len g <= (len f) + 1 by A18, A32, XREAL_1:6;

now :: thesis: ( ( len g = (len f) + 1 & contradiction ) or ( len g < (len f) + 1 & (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} ) )

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

case len g = (len f) + 1 ; :: thesis: contradiction

hence contradiction by A2, A18, A32, JORDAN3:8; :: thesis: verum

end;

case len g < (len f) + 1 ; :: thesis: (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))}

then len g <= len f by NAT_1:13;
then j + 2 <= len f by A22, XXREAL_0:2;
then A34: (LSeg (g,j)) /\ (LSeg (g,(j + 1))) c= {(f /. (j + 1))} by A1, A21, A30, TOPREAL1:def 6;
A35: j + 1 <= Index (p,f) by A18, A29, A32, XREAL_1:6;
then j + 1 <= len f by A28, XXREAL_0:2;
then A36: f . (j + 1) = f /. (j + 1) by A25, FINSEQ_4:15;
g . (j + 1) = (mid (f,1,(Index (p,f)))) . (j + 1) by A4, A18, A25, A35, FINSEQ_1:64
.= f . (j + 1) by A5, A25, A35, FINSEQ_6:123 ;
hence (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} by A31, A26, A34, A36; :: thesis: verum

end;

end;

end;

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

end;

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

end;

for j being Nat st 1 <= j & j + 1 <= len g & not (g /. j) `1 = (g /. (j + 1)) `1 holds
(g /. j) `2 = (g /. (j + 1)) `2

proof

A37: Index (p,f) < len f by A2, JORDAN3:8;
let j be Nat; :: thesis: ( 1 <= j & j + 1 <= len g & not (g /. j) `1 = (g /. (j + 1)) `1 implies (g /. j) `2 = (g /. (j + 1)) `2 )
assume that
A38: 1 <= j and
A39: j + 1 <= len g ; :: thesis: ( (g /. j) `1 = (g /. (j + 1)) `1 or (g /. j) `2 = (g /. (j + 1)) `2 )
A40: LSeg (g,j) = LSeg ((g /. j),(g /. (j + 1))) by A38, A39, TOPREAL1:def 3;
j + 1 <= (Index (p,f)) + 1 by A4, A18, A39, FINSEQ_2:16;
then j <= Index (p,f) by XREAL_1:6;
then j < len f by A37, XXREAL_0:2;
then A41: j + 1 <= len f by NAT_1:13;
then A42: LSeg (f,j) = LSeg ((f /. j),(f /. (j + 1))) by A38, TOPREAL1:def 3;
A43: ( (f /. j) `1 = (f /. (j + 1)) `1 or (f /. j) `2 = (f /. (j + 1)) `2 ) by A1, A38, A41, TOPREAL1:def 5;
LSeg (g,j) c= LSeg (f,j) by A2, A4, A38, A39, JORDAN3:18;
hence ( (g /. j) `1 = (g /. (j + 1)) `1 or (g /. j) `2 = (g /. (j + 1)) `2 ) by A40, A42, A43, JORDAN3:3; :: thesis: verum

end;

then A44: ( g is unfolded & g is s.n.c. & g is special ) by A20, A6, TOPREAL1:def 5, TOPREAL1:def 6, TOPREAL1:def 7;
1 <= len <*p*> by FINSEQ_1:39;
then A45: 1 in dom <*p*> by FINSEQ_3:25;
for x1, x2 being object st x1 in dom g & x2 in dom g & g . x1 = g . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 implies x1 = x2 )
assume that
A46: x1 in dom g and
A47: x2 in dom g and
A48: g . x1 = g . x2 ; :: thesis: x1 = x2
reconsider n1 = x1, n2 = x2 as Nat by A46, A47;
A49: 1 <= n1 by A46, FINSEQ_3:25;
A50: n2 <= len g by A47, FINSEQ_3:25;
A51: 1 <= n2 by A47, FINSEQ_3:25;
A52: n1 <= len g by A46, FINSEQ_3:25;

now :: thesis: x1 = x2

A53: g . (len g) = <*p*> . 1 by A4, A45, A13, FINSEQ_1:def 7
.= p ;

now :: thesis: ( ( n1 = len g & x1 = x2 ) or ( n2 = len g & x1 = x2 ) or ( n1 <> len g & n2 <> len g & x1 = x2 ) )

per cases ( n1 = len g or n2 = len g or ( n1 <> len g & n2 <> len g ) ) ;

case A54: n1 = len g ; :: thesis: x1 = x2

now :: thesis: not n2 <> len g

assume A55: n2 <> len g ; :: thesis: contradiction
then n2 < len g by A50, XXREAL_0:1;
then A56: n2 <= len (mid (f,1,(Index (p,f)))) by A13, NAT_1:13;
then A57: n2 < len f by A5, A18, XXREAL_0:2;
g . n2 = (mid (f,1,(Index (p,f)))) . n2 by A4, A51, A56, FINSEQ_1:64;
then g . n2 = f . ((n2 + 1) -' 1) by A15, A5, A16, A51, A56, FINSEQ_6:118;
then A58: p = f . n2 by A48, A53, A54, NAT_D:34;
then 1 < n2 by A3, A51, XXREAL_0:1;
then (Index (p,f)) + 1 = n2 by A1, A58, A57, Th18;
hence contradiction by A2, A17, A13, A55, JORDAN3:8, XREAL_1:235; :: thesis: verum

end;

hence x1 = x2 by A54; :: thesis: verum

end;

case A59: n2 = len g ; :: thesis: x1 = x2

now :: thesis: not n1 <> len g

assume A60: n1 <> len g ; :: thesis: contradiction
then n1 < len g by A52, XXREAL_0:1;
then A61: n1 <= len (mid (f,1,(Index (p,f)))) by A13, NAT_1:13;
then A62: n1 < len f by A5, A18, XXREAL_0:2;
g . n1 = (mid (f,1,(Index (p,f)))) . n1 by A4, A49, A61, FINSEQ_1:64;
then g . n1 = f . ((n1 + 1) -' 1) by A15, A5, A16, A49, A61, FINSEQ_6:118;
then A63: p = f . n1 by A48, A53, A59, NAT_D:34;
then 1 < n1 by A3, A49, XXREAL_0:1;
then (Index (p,f)) + 1 = n1 by A1, A63, A62, Th18;
hence contradiction by A2, A17, A13, A60, JORDAN3:8, XREAL_1:235; :: thesis: verum

end;

hence x1 = x2 by A59; :: thesis: verum

end;

case that A64: n1 <> len g and
A65: n2 <> len g ; :: thesis: x1 = x2

n2 < len g by A50, A65, XXREAL_0:1;
then A66: n2 <= len (mid (f,1,(Index (p,f)))) by A13, NAT_1:13;
then A67: g . n2 = (mid (f,1,(Index (p,f)))) . n2 by A4, A51, FINSEQ_1:64
.= f . n2 by A5, A18, A51, A66, FINSEQ_6:123 ;
n2 < len f by A5, A18, A66, XXREAL_0:2;
then n2 in Seg (len f) by A51, FINSEQ_1:1;
then A68: n2 in dom f by FINSEQ_1:def 3;
n1 < len g by A52, A64, XXREAL_0:1;
then A69: n1 <= len (mid (f,1,(Index (p,f)))) by A13, NAT_1:13;
then n1 < len f by A5, A18, XXREAL_0:2;
then n1 in Seg (len f) by A49, FINSEQ_1:1;
then A70: n1 in dom f by FINSEQ_1:def 3;
g . n1 = (mid (f,1,(Index (p,f)))) . n1 by A4, A49, A69, FINSEQ_1:64
.= f . n1 by A5, A18, A49, A69, FINSEQ_6:123 ;
hence x1 = x2 by A1, A5, A18, A48, A69, A66, A67, A70, A68; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

hence x1 = x2 ; :: thesis: verum

end;

then A71: g is one-to-one ;
1 + 1 <= len g by A15, A18, A13, XREAL_1:6;
then A72: g is being_S-Seq by A71, A44, TOPREAL1:def 8;
g . (len g) = p by A4, A13, FINSEQ_1:42;
hence g is_S-Seq_joining f /. 1,p by A19, A72, JORDAN3:def 2; :: thesis: verum