let f, g be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st f is being_S-Seq & 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 being_S-Seq & 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 being_S-Seq 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, Th41;
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
A8: ( j1 = 0 or j1 >= 0 + 1 ) by NAT_1:13;

now

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 5;
then (LSeg g,j1) /\ (LSeg g,j2) = {} ;
hence LSeg g,j1 misses LSeg g,j2 by XBOOLE_0:def 7; :: 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, Th51;
1 + 1 <= j1 + 1 by A9, XREAL_1:8;
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, Th51;
LSeg f,j1 misses LSeg f,j2 by A1, A7, TOPREAL1:def 9;
then (LSeg f,j1) /\ (LSeg f,j2) = {} by XBOOLE_0:def 7;
then (LSeg g,j1) /\ (LSeg g,j2) = {} by A11, A12, XBOOLE_1:3, XBOOLE_1:27;
hence LSeg g,j1 misses LSeg g,j2 by XBOOLE_0:def 7; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

A13: for n1, n2 being Element of NAT st 1 <= n1 & n1 <= len f & 1 <= n2 & n2 <= len f & f . n1 = f . n2 holds
n1 = n2

proof

let n1, n2 be Element of NAT ; :: thesis: ( 1 <= n1 & n1 <= len f & 1 <= n2 & n2 <= len f & f . n1 = f . n2 implies n1 = n2 )
assume that
A14: 1 <= n1 and
A15: n1 <= len f and
A16: 1 <= n2 and
A17: n2 <= len f and
A18: f . n1 = f . n2 ; :: thesis: n1 = n2
A19: n2 in dom f by A16, A17, FINSEQ_3:27;
n1 in dom f by A14, A15, FINSEQ_3:27;
hence n1 = n2 by A1, A18, A19, FUNCT_1:def 8; :: thesis: verum

end;

A20: len g = (len (mid f,1,(Index p,f))) + (len <*p*>) by A4, FINSEQ_1:35
.= (len (mid f,1,(Index p,f))) + 1 by FINSEQ_1:56 ;
consider i being Element of NAT such that
1 <= i and
A21: i + 1 <= len f and
p in LSeg f,i by A2, SPPOL_2:13;
A22: 1 <= Index p,f by A2, Th41;
1 <= 1 + i by NAT_1:12;
then A23: 1 <= len f by A21, XXREAL_0:2;
then A24: len (mid f,1,(Index p,f)) = ((Index p,f) -' 1) + 1 by A22, A5, FINSEQ_6:124;
then A25: len (mid f,1,(Index p,f)) = Index p,f by A2, Th41, XREAL_1:237;
then g . 1 = (mid f,1,(Index p,f)) . 1 by A4, A22, FINSEQ_6:115;
then g . 1 = f . 1 by A22, A5, A23, FINSEQ_6:124;
then A26: g . 1 = f /. 1 by A23, FINSEQ_4:24;
A27: 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
A28: 1 <= j and
A29: j + 2 <= len g ; :: thesis: (LSeg g,j) /\ (LSeg g,(j + 1)) = {(g /. (j + 1))}
A30: j + 1 <= len g by A29, NAT_D:47;
then LSeg g,j = LSeg (g /. j),(g /. (j + 1)) by A28, TOPREAL1:def 5;
then A31: g /. (j + 1) in LSeg g,j by RLTOPSP1:69;
A32: 1 <= j + 1 by A28, NAT_D:48;
then LSeg g,(j + 1) = LSeg (g /. (j + 1)),(g /. ((j + 1) + 1)) by A29, TOPREAL1:def 5;
then g /. (j + 1) in LSeg g,(j + 1) by RLTOPSP1:69;
then g /. (j + 1) in (LSeg g,j) /\ (LSeg g,(j + 1)) by A31, XBOOLE_0:def 4;
then A33: {(g /. (j + 1))} c= (LSeg g,j) /\ (LSeg g,(j + 1)) by ZFMISC_1:37;
j + 1 <= len g by A29, NAT_D:47;
then A34: LSeg g,j c= LSeg f,j by A2, A4, A28, Th51;
A35: Index p,f <= len f by A2, Th41;
A36: (j + 1) + 1 <= len g by A29;
then LSeg g,(j + 1) c= LSeg f,(j + 1) by A2, A4, A32, Th51;
then A37: (LSeg g,j) /\ (LSeg g,(j + 1)) c= (LSeg f,j) /\ (LSeg f,(j + 1)) by A34, XBOOLE_1:27;
A38: g /. (j + 1) = g . (j + 1) by A32, A30, FINSEQ_4:24;

now

A39: len g = (len (mid f,1,(Index p,f))) + 1 by A4, FINSEQ_2:19;
Index p,f <= len f by A2, Th41;
then A40: len g <= (len f) + 1 by A25, A39, XREAL_1:8;

now

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

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

hence contradiction by A2, A25, A39, Th41; :: 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 A29, XXREAL_0:2;
then A41: (LSeg g,j) /\ (LSeg g,(j + 1)) c= {(f /. (j + 1))} by A1, A28, A37, TOPREAL1:def 8;
A42: j + 1 <= Index p,f by A25, A36, A39, XREAL_1:8;
then j + 1 <= len f by A35, XXREAL_0:2;
then A43: f . (j + 1) = f /. (j + 1) by A32, FINSEQ_4:24;
g . (j + 1) = (mid f,1,(Index p,f)) . (j + 1) by A4, A25, A32, A42, FINSEQ_1:85
.= f . (j + 1) by A5, A32, A42, FINSEQ_6:129 ;
hence (LSeg g,j) /\ (LSeg g,(j + 1)) = {(g /. (j + 1))} by A38, A33, A41, A43, XBOOLE_0:def 10; :: 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

A44: Index p,f < len f by A2, Th41;
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
A45: 1 <= j and
A46: j + 1 <= len g ; :: thesis: ( (g /. j) `1 = (g /. (j + 1)) `1 or (g /. j) `2 = (g /. (j + 1)) `2 )
A47: LSeg g,j = LSeg (g /. j),(g /. (j + 1)) by A45, A46, TOPREAL1:def 5;
j + 1 <= (Index p,f) + 1 by A4, A25, A46, FINSEQ_2:19;
then j <= Index p,f by XREAL_1:8;
then j < len f by A44, XXREAL_0:2;
then A48: j + 1 <= len f by NAT_1:13;
then A49: LSeg f,j = LSeg (f /. j),(f /. (j + 1)) by A45, TOPREAL1:def 5;
A50: ( (f /. j) `1 = (f /. (j + 1)) `1 or (f /. j) `2 = (f /. (j + 1)) `2 ) by A1, A45, A48, TOPREAL1:def 7;
LSeg g,j c= LSeg f,j by A2, A4, A45, A46, Th51;
hence ( (g /. j) `1 = (g /. (j + 1)) `1 or (g /. j) `2 = (g /. (j + 1)) `2 ) by A47, A49, A50, Th36; :: thesis: verum

end;

then A51: ( g is unfolded & g is s.n.c. & g is special ) by A27, A6, TOPREAL1:def 7, TOPREAL1:def 8, TOPREAL1:def 9;
1 <= len <*p*> by FINSEQ_1:56;
then A52: 1 in dom <*p*> by FINSEQ_3:27;
for x1, x2 being set st x1 in dom g & x2 in dom g & g . x1 = g . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 implies x1 = x2 )
assume that
A53: x1 in dom g and
A54: x2 in dom g and
A55: g . x1 = g . x2 ; :: thesis: x1 = x2
reconsider n1 = x1, n2 = x2 as Element of NAT by A53, A54;
A56: 1 <= n1 by A53, FINSEQ_3:27;
A57: n2 <= len g by A54, FINSEQ_3:27;
A58: 1 <= n2 by A54, FINSEQ_3:27;
A59: n1 <= len g by A53, FINSEQ_3:27;

now

A60: g . (len g) = <*p*> . 1 by A4, A52, A20, FINSEQ_1:def 7
.= p by FINSEQ_1:def 8 ;

now

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

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

now

assume A62: n2 <> len g ; :: thesis: contradiction
then n2 < len g by A57, XXREAL_0:1;
then A63: n2 <= len (mid f,1,(Index p,f)) by A20, NAT_1:13;
then A64: n2 <= len f by A5, A25, XXREAL_0:2;
g . n2 = (mid f,1,(Index p,f)) . n2 by A4, A58, A63, FINSEQ_1:85;
then g . n2 = f . ((n2 + 1) -' 1) by A22, A5, A23, A58, A63, FINSEQ_6:124;
then A65: p = f . n2 by A55, A60, A61, NAT_D:34;
then 1 < n2 by A3, A58, XXREAL_0:1;
then (Index p,f) + 1 = n2 by A1, A65, A64, Th45;
hence contradiction by A2, A24, A20, A62, Th41, XREAL_1:237; :: thesis: verum

end;

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

end;

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

now

assume A67: n1 <> len g ; :: thesis: contradiction
then n1 < len g by A59, XXREAL_0:1;
then A68: n1 <= len (mid f,1,(Index p,f)) by A20, NAT_1:13;
then A69: n1 <= len f by A5, A25, XXREAL_0:2;
g . n1 = (mid f,1,(Index p,f)) . n1 by A4, A56, A68, FINSEQ_1:85;
then g . n1 = f . ((n1 + 1) -' 1) by A22, A5, A23, A56, A68, FINSEQ_6:124;
then A70: p = f . n1 by A55, A60, A66, NAT_D:34;
then 1 < n1 by A3, A56, XXREAL_0:1;
then (Index p,f) + 1 = n1 by A1, A70, A69, Th45;
hence contradiction by A2, A24, A20, A67, Th41, XREAL_1:237; :: thesis: verum

end;

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

end;

case that A71: n1 <> len g and
A72: n2 <> len g ; :: thesis: x1 = x2

n1 < len g by A59, A71, XXREAL_0:1;
then A73: n1 <= len (mid f,1,(Index p,f)) by A20, NAT_1:13;
then A74: n1 <= len f by A5, A25, XXREAL_0:2;
n2 < len g by A57, A72, XXREAL_0:1;
then A75: n2 <= len (mid f,1,(Index p,f)) by A20, NAT_1:13;
then A76: g . n2 = (mid f,1,(Index p,f)) . n2 by A4, A58, FINSEQ_1:85
.= f . n2 by A5, A25, A58, A75, FINSEQ_6:129 ;
A77: n2 <= len f by A5, A25, A75, XXREAL_0:2;
g . n1 = (mid f,1,(Index p,f)) . n1 by A4, A56, A73, FINSEQ_1:85
.= f . n1 by A5, A25, A56, A73, FINSEQ_6:129 ;
hence x1 = x2 by A13, A55, A56, A58, A74, A77, A76; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

hence x1 = x2 ; :: thesis: verum

end;

then A78: g is one-to-one by FUNCT_1:def 8;
1 + 1 <= len g by A22, A25, A20, XREAL_1:8;
then A79: g is being_S-Seq by A78, A51, TOPREAL1:def 10;
g . (len g) = p by A4, A20, FINSEQ_1:59;
hence g is_S-Seq_joining f /. 1,p by A26, A79, Def3; :: thesis: verum