let f, g be FinSequence of (); :: thesis: for p being Point of () 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 (); :: 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 ;
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 :: 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 ;
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) 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 ;
then j1 + 1 < len g by ;
then A11: LSeg (g,j1) c= LSeg (f,j1) by A2, A4, A9, Th18;
1 + 1 <= j1 + 1 by ;
then 2 <= j2 by ;
then 1 <= j2 by XXREAL_0:2;
then A12: LSeg (g,j2) c= LSeg (f,j2) by A2, A4, A10, Th18;
LSeg (f,j1) misses LSeg (f,j2) by ;
then (LSeg (f,j1)) /\ (LSeg (f,j2)) = {} by XBOOLE_0:def 7;
then (LSeg (g,j1)) /\ (LSeg (g,j2)) = {} by ;
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 3;
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 ;
n1 in dom f by ;
hence n1 = n2 by ; :: thesis: verum
end;
A20: len g = (len (mid (f,1,(Index (p,f))))) + () by
.= (len (mid (f,1,(Index (p,f))))) + 1 by FINSEQ_1:39 ;
consider i being Nat such that
1 <= i and
A21: i + 1 <= len f and
p in LSeg (f,i) by ;
A22: 1 <= Index (p,f) by ;
1 <= 1 + i by NAT_1:12;
then A23: 1 <= len f by ;
then A24: len (mid (f,1,(Index (p,f)))) = ((Index (p,f)) -' 1) + 1 by ;
then A25: len (mid (f,1,(Index (p,f)))) = Index (p,f) by ;
then g . 1 = (mid (f,1,(Index (p,f)))) . 1 by ;
then g . 1 = f . 1 by ;
then A26: g . 1 = f /. 1 by ;
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 ;
then LSeg (g,j) = LSeg ((g /. j),(g /. (j + 1))) by ;
then A31: g /. (j + 1) in LSeg (g,j) by RLTOPSP1:68;
A32: 1 <= j + 1 by ;
then LSeg (g,(j + 1)) = LSeg ((g /. (j + 1)),(g /. ((j + 1) + 1))) by ;
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 ;
then A33: {(g /. (j + 1))} c= (LSeg (g,j)) /\ (LSeg (g,(j + 1))) by ZFMISC_1:31;
j + 1 <= len g by ;
then A34: LSeg (g,j) c= LSeg (f,j) by A2, A4, A28, Th18;
A35: Index (p,f) <= len f by ;
A36: (j + 1) + 1 <= len g by A29;
then LSeg (g,(j + 1)) c= LSeg (f,(j + 1)) by A2, A4, A32, Th18;
then A37: (LSeg (g,j)) /\ (LSeg (g,(j + 1))) c= (LSeg (f,j)) /\ (LSeg (f,(j + 1))) by ;
A38: g /. (j + 1) = g . (j + 1) by ;
now :: thesis: (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))}
A39: len g = (len (mid (f,1,(Index (p,f))))) + 1 by ;
Index (p,f) <= len f by ;
then A40: len g <= (len f) + 1 by ;
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 ;
case len g = (len f) + 1 ; :: thesis: contradiction
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 ;
then A41: (LSeg (g,j)) /\ (LSeg (g,(j + 1))) c= {(f /. (j + 1))} by ;
A42: j + 1 <= Index (p,f) by ;
then j + 1 <= len f by ;
then A43: f . (j + 1) = f /. (j + 1) by ;
g . (j + 1) = (mid (f,1,(Index (p,f)))) . (j + 1) by
.= f . (j + 1) by ;
hence (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} by ; :: 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 ;
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 ;
j + 1 <= (Index (p,f)) + 1 by ;
then j <= Index (p,f) by XREAL_1:6;
then j < len f by ;
then A48: j + 1 <= len f by NAT_1:13;
then A49: LSeg (f,j) = LSeg ((f /. j),(f /. (j + 1))) by ;
A50: ( (f /. j) `1 = (f /. (j + 1)) `1 or (f /. j) `2 = (f /. (j + 1)) `2 ) by ;
LSeg (g,j) c= LSeg (f,j) by A2, A4, A45, A46, Th18;
hence ( (g /. j) `1 = (g /. (j + 1)) `1 or (g /. j) `2 = (g /. (j + 1)) `2 ) by A47, A49, A50, Th3; :: thesis: verum
end;
then A51: ( g is unfolded & g is s.n.c. & g is special ) by ;
1 <= len <*p*> by FINSEQ_1:39;
then A52: 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
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 ;
A56: 1 <= n1 by ;
A57: n2 <= len g by ;
A58: 1 <= n2 by ;
A59: n1 <= len g by ;
now :: thesis: x1 = x2
A60: g . (len g) = <*p*> . 1 by
.= p by FINSEQ_1:def 8 ;
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 A61: n1 = len g ; :: thesis: x1 = x2
now :: thesis: not n2 <> len g
assume A62: n2 <> len g ; :: thesis: contradiction
then n2 < len g by ;
then A63: n2 <= len (mid (f,1,(Index (p,f)))) by ;
then A64: n2 <= len f by ;
g . n2 = (mid (f,1,(Index (p,f)))) . n2 by ;
then g . n2 = f . ((n2 + 1) -' 1) by ;
then A65: p = f . n2 by ;
then 1 < n2 by ;
then (Index (p,f)) + 1 = n2 by A1, A65, A64, Th12;
hence contradiction by A2, A24, A20, A62, Th8, XREAL_1:235; :: thesis: verum
end;
hence x1 = x2 by A61; :: thesis: verum
end;
case A66: n2 = len g ; :: thesis: x1 = x2
now :: thesis: not n1 <> len g
assume A67: n1 <> len g ; :: thesis: contradiction
then n1 < len g by ;
then A68: n1 <= len (mid (f,1,(Index (p,f)))) by ;
then A69: n1 <= len f by ;
g . n1 = (mid (f,1,(Index (p,f)))) . n1 by ;
then g . n1 = f . ((n1 + 1) -' 1) by ;
then A70: p = f . n1 by ;
then 1 < n1 by ;
then (Index (p,f)) + 1 = n1 by A1, A70, A69, Th12;
hence contradiction by A2, A24, A20, A67, Th8, XREAL_1:235; :: 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 ;
then A73: n1 <= len (mid (f,1,(Index (p,f)))) by ;
then A74: n1 <= len f by ;
n2 < len g by ;
then A75: n2 <= len (mid (f,1,(Index (p,f)))) by ;
then A76: g . n2 = (mid (f,1,(Index (p,f)))) . n2 by
.= f . n2 by ;
A77: n2 <= len f by ;
g . n1 = (mid (f,1,(Index (p,f)))) . n1 by
.= f . n1 by ;
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 4;
1 + 1 <= len g by ;
then A79: g is being_S-Seq by ;
g . (len g) = p by ;
hence g is_S-Seq_joining f /. 1,p by ; :: thesis: verum