let f, g be FinSequence of (); :: thesis: for p being Point of () st f is being_S-Seq & p in L~ f & p <> f . ((Index (p,f)) + 1) & g = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) holds
g is_S-Seq_joining p,f /. (len f)

let p be Point of (); :: thesis: ( f is being_S-Seq & p in L~ f & p <> f . ((Index (p,f)) + 1) & g = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) implies g is_S-Seq_joining p,f /. (len f) )
assume that
A1: f is being_S-Seq and
A2: p in L~ f and
A3: p <> f . ((Index (p,f)) + 1) and
A4: g = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) ; :: thesis: g is_S-Seq_joining p,f /. (len f)
len g = () + (len (mid (f,((Index (p,f)) + 1),(len f)))) by ;
then A5: len g = 1 + (len (mid (f,((Index (p,f)) + 1),(len f)))) by FINSEQ_1:39;
consider i being Nat such that
1 <= i and
A6: i + 1 <= len f and
p in LSeg (f,i) by ;
1 <= 1 + i by NAT_1:12;
then A7: 1 <= len f by ;
A8: 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 A9: j1 + 1 < j2 ; :: thesis: LSeg (g,j1) misses LSeg (g,j2)
A10: ( 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 A11: ( j1 = 1 or j1 > 1 ) and
A12: j2 + 1 <= len g ; :: thesis: LSeg (g,j1) misses LSeg (g,j2)
1 < j1 + 1 by ;
then 1 <= j2 by ;
then A13: LSeg (g,j2) c= LSeg (f,(((Index (p,f)) + j2) -' 1)) by A2, A4, A12, Th16;
1 <= (Index (p,f)) + j1 by ;
then 1 - 1 <= ((Index (p,f)) + j1) - 1 by XREAL_1:9;
then A14: ((Index (p,f)) + j1) - 1 = ((Index (p,f)) + j1) -' 1 by XREAL_0:def 2;
(Index (p,f)) + (j1 + 1) < (Index (p,f)) + j2 by ;
then (((Index (p,f)) + j1) + 1) - 1 < ((Index (p,f)) + j2) - 1 by XREAL_1:9;
then (((Index (p,f)) + j1) -' 1) + 1 < ((Index (p,f)) + j2) -' 1 by ;
then LSeg (f,(((Index (p,f)) + j1) -' 1)) misses LSeg (f,(((Index (p,f)) + j2) -' 1)) by ;
then A15: (LSeg (f,(((Index (p,f)) + j1) -' 1))) /\ (LSeg (f,(((Index (p,f)) + j2) -' 1))) = {} by XBOOLE_0:def 7;
j2 < len g by ;
then j1 + 1 <= len g by ;
then LSeg (g,j1) c= LSeg (f,(((Index (p,f)) + j1) -' 1)) by A2, A4, A11, Th16;
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;
A16: Index (p,f) < len f by ;
then A17: (Index (p,f)) + 1 <= len f by NAT_1:13;
(Index (p,f)) + 1 <= len f by ;
then A18: ((Index (p,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f)) by XREAL_1:9;
then A19: 1 - 1 <= ((len f) - (Index (p,f))) - 1 by XREAL_1:9;
then A20: (len f) -' ((Index (p,f)) + 1) = (len f) - ((Index (p,f)) + 1) by XREAL_0:def 2
.= ((len f) - (Index (p,f))) - 1 ;
A21: 0 + 1 <= (Index (p,f)) + 1 by NAT_1:11;
then A22: len (mid (f,((Index (p,f)) + 1),(len f))) = ((len f) -' ((Index (p,f)) + 1)) + 1 by ;
A23: 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
A24: 1 <= j and
A25: j + 2 <= len g ; :: thesis: (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))}
A26: j + 2 = (j + 1) + 1 ;
then A27: j + 1 <= len g by ;
then A28: LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1)) by A2, A4, A24, Th16;
1 <= j + 1 by ;
then LSeg (g,(j + 1)) c= LSeg (f,(((Index (p,f)) + (j + 1)) -' 1)) by A2, A4, A25, A26, Th16;
then A29: (LSeg (g,j)) /\ (LSeg (g,(j + 1))) c= (LSeg (f,(((Index (p,f)) + j) -' 1))) /\ (LSeg (f,(((Index (p,f)) + (j + 1)) -' 1))) by ;
A30: 1 <= Index (p,f) by ;
1 <= Index (p,f) by ;
then 1 + 1 <= (Index (p,f)) + j by ;
then 1 <= ((Index (p,f)) + j) - 1 by XREAL_1:19;
then A31: 1 <= ((Index (p,f)) + j) -' 1 by NAT_D:39;
1 <= (Index (p,f)) + j by ;
then A32: 1 - 1 <= ((Index (p,f)) + j) - 1 by XREAL_1:9;
((j + 1) + 1) - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1 by ;
then A33: (j + 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by ;
then ((Index (p,f)) + j) + 1 <= len f ;
then ((Index (p,f)) + (j - 1)) + 1 <= len f by NAT_D:46;
then A34: (((Index (p,f)) + j) -' 1) + 1 <= len f by ;
(((Index (p,f)) + j) - 1) + (1 + 1) <= len f by A33;
then (((Index (p,f)) + j) -' 1) + 2 <= len f by ;
then A35: {(f /. ((((Index (p,f)) + j) -' 1) + 1))} = (LSeg (f,(((Index (p,f)) + j) -' 1))) /\ (LSeg (f,((((Index (p,f)) + j) -' 1) + 1))) by ;
A36: 1 < j + 1 by ;
then A37: g /. (j + 1) = g . (j + 1) by ;
A38: g /. (j + 1) in LSeg ((g /. (j + 1)),(g /. ((j + 1) + 1))) by RLTOPSP1:68;
g /. (j + 1) in LSeg ((g /. j),(g /. (j + 1))) by RLTOPSP1:68;
then A39: g /. (j + 1) in (LSeg ((g /. j),(g /. (j + 1)))) /\ (LSeg ((g /. (j + 1)),(g /. ((j + 1) + 1)))) by ;
A40: LSeg (g,j) = LSeg ((g /. j),(g /. (j + 1))) by ;
LSeg ((g /. (j + 1)),(g /. ((j + 1) + 1))) = LSeg (g,(j + 1)) by ;
then A41: {(g /. (j + 1))} c= (LSeg (g,j)) /\ (LSeg (g,(j + 1))) by ;
A42: j + 1 = ((j + 1) - 1) + 1
.= ((j + 1) -' 1) + 1 by ;
then A43: j + 1 = () + ((j + 1) -' 1) by FINSEQ_1:39;
A44: (j + 1) -' 1 <= len (mid (f,((Index (p,f)) + 1),(len f))) by ;
then (j + 1) -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by ;
then g . (j + 1) = (mid (f,((Index (p,f)) + 1),(len f))) . ((j + 1) -' 1) by
.= f . ((((j + 1) -' 1) + ((Index (p,f)) + 1)) -' 1) by
.= f . (((((j + 1) -' 1) + 1) + (Index (p,f))) -' 1)
.= f . (((j + 1) + (Index (p,f))) -' 1) by
.= f . ((((Index (p,f)) + j) + 1) -' 1)
.= f . ((Index (p,f)) + j) by NAT_D:34
.= f . ((((Index (p,f)) + j) -' 1) + 1) by ;
then A45: f /. ((((Index (p,f)) + j) -' 1) + 1) = g /. (j + 1) by ;
((Index (p,f)) + (j + 1)) -' 1 = (((Index (p,f)) + j) + 1) - 1 by
.= (((Index (p,f)) + j) - 1) + 1
.= (((Index (p,f)) + j) -' 1) + 1 by ;
hence (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} by ; :: thesis: verum
end;
A46: len g = () + (len (mid (f,((Index (p,f)) + 1),(len f)))) by
.= 1 + (len (mid (f,((Index (p,f)) + 1),(len f)))) by FINSEQ_1:39 ;
then A47: len g = 1 + (((len f) - ((Index (p,f)) + 1)) + 1) by
.= 1 + ((len f) - (Index (p,f))) ;
then A48: (len g) -' 1 = (len g) - 1 by ;
then A49: (len g) -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by ;
A50: (len f) - (Index (p,f)) >= 0 by ;
then A51: (len f) - (Index (p,f)) = (len f) -' (Index (p,f)) by XREAL_0:def 2;
then A52: (mid (f,((Index (p,f)) + 1),(len f))) . ((len f) -' (Index (p,f))) = f . ((((len f) -' (Index (p,f))) + ((Index (p,f)) + 1)) -' 1) by ;
A53: (len g) -' 1 = (len f) -' (Index (p,f)) by ;
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
A54: x1 in dom g and
A55: x2 in dom g and
A56: g . x1 = g . x2 ; :: thesis: x1 = x2
reconsider n1 = x1, n2 = x2 as Element of NAT by ;
A57: n1 <= len g by ;
A58: 1 <= n2 by ;
A59: n2 <= len g by ;
A60: 1 <= n1 by ;
now :: thesis: ( ( n1 = 1 & n2 = 1 & x1 = x2 ) or ( n1 = 1 & n2 > 1 & contradiction ) or ( n1 > 1 & n2 = 1 & contradiction ) or ( n1 > 1 & n2 > 1 & x1 = x2 ) )
per cases ( ( n1 = 1 & n2 = 1 ) or ( n1 = 1 & n2 > 1 ) or ( n1 > 1 & n2 = 1 ) or ( n1 > 1 & n2 > 1 ) ) by ;
case ( n1 = 1 & n2 = 1 ) ; :: thesis: x1 = x2
hence x1 = x2 ; :: thesis: verum
end;
case that A61: n1 = 1 and
A62: n2 > 1 ; :: thesis: contradiction
A63: n2 - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1 by ;
n1 <= len <*p*> by ;
then n1 in dom <*p*> by ;
then A64: g . n1 = <*p*> . n1 by ;
n2 - 1 > 0 by ;
then A65: n2 -' 1 = n2 - 1 by XREAL_0:def 2;
then A66: () + (n2 -' 1) = 1 + (n2 - 1) by FINSEQ_1:39
.= n2 ;
A67: 1 <= n2 -' 1 by ;
then n2 -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by ;
then g . n2 = (mid (f,((Index (p,f)) + 1),(len f))) . (n2 -' 1) by
.= f . (((n2 -' 1) + ((Index (p,f)) + 1)) -' 1) by
.= f . ((n2 + (Index (p,f))) -' 1) by A65 ;
then A68: f . ((n2 + (Index (p,f))) -' 1) = p by ;
n2 -' 1 <= (len f) - (Index (p,f)) by ;
then n2 - 1 <= (len f) - (Index (p,f)) by ;
then A69: (n2 - 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by XREAL_1:6;
1 + 1 < n2 + (Index (p,f)) by ;
then A70: 1 < (n2 + (Index (p,f))) - 1 by XREAL_1:20;
then (n2 + (Index (p,f))) -' 1 = (n2 + (Index (p,f))) - 1 by XREAL_0:def 2;
hence contradiction by A1, A3, A70, A68, A69, Th12; :: thesis: verum
end;
case that A71: n1 > 1 and
A72: n2 = 1 ; :: thesis: contradiction
A73: n1 - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1 by ;
n2 <= len <*p*> by ;
then n2 in dom <*p*> by ;
then A74: g . n2 = <*p*> . n2 by ;
n1 - 1 > 0 by ;
then A75: n1 -' 1 = n1 - 1 by XREAL_0:def 2;
then A76: () + (n1 -' 1) = 1 + (n1 - 1) by FINSEQ_1:39
.= n1 ;
A77: 1 <= n1 -' 1 by ;
then n1 -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by ;
then g . n1 = (mid (f,((Index (p,f)) + 1),(len f))) . (n1 -' 1) by
.= f . (((n1 -' 1) + ((Index (p,f)) + 1)) -' 1) by
.= f . ((n1 + (Index (p,f))) -' 1) by A75 ;
then A78: f . ((n1 + (Index (p,f))) -' 1) = p by ;
n1 -' 1 <= (len f) - (Index (p,f)) by ;
then n1 - 1 <= (len f) - (Index (p,f)) by ;
then A79: (n1 - 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by XREAL_1:6;
1 + 1 < n1 + (Index (p,f)) by ;
then A80: 1 < (n1 + (Index (p,f))) - 1 by XREAL_1:20;
then (n1 + (Index (p,f))) -' 1 = (n1 + (Index (p,f))) - 1 by XREAL_0:def 2;
hence contradiction by A1, A3, A80, A78, A79, Th12; :: thesis: verum
end;
case that A81: n1 > 1 and
A82: n2 > 1 ; :: thesis: x1 = x2
A83: n2 - 1 > 0 by ;
then A84: n2 -' 1 = n2 - 1 by XREAL_0:def 2;
then A85: () + (n2 -' 1) = 1 + (n2 - 1) by FINSEQ_1:39
.= n2 ;
A86: n1 - 1 > 0 by ;
then A87: n1 -' 1 = n1 - 1 by XREAL_0:def 2;
then A88: 0 + 1 <= n1 -' 1 by ;
then A89: 1 <= (n1 - 1) + (Index (p,f)) by ;
then A90: (n1 + (Index (p,f))) -' 1 = (n1 + (Index (p,f))) - 1 by XREAL_0:def 2;
A91: () + (n1 -' 1) = 1 + (n1 - 1) by
.= n1 ;
A92: n1 - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1 by ;
then n1 -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by ;
then A93: g . n1 = (mid (f,((Index (p,f)) + 1),(len f))) . (n1 -' 1) by
.= f . (((n1 -' 1) + ((Index (p,f)) + 1)) -' 1) by
.= f . ((n1 + (Index (p,f))) -' 1) by A87 ;
n1 -' 1 <= (len f) -' (Index (p,f)) by ;
then (n1 -' 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by ;
then A94: (n1 + (Index (p,f))) -' 1 in dom f by ;
A95: 0 + 1 <= n2 -' 1 by ;
then A96: 1 <= (n2 -' 1) + (Index (p,f)) by NAT_1:12;
then A97: (n2 + (Index (p,f))) -' 1 = (n2 + (Index (p,f))) - 1 by ;
A98: n2 - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1 by ;
then n2 -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by ;
then A99: g . n2 = (mid (f,((Index (p,f)) + 1),(len f))) . (n2 -' 1) by
.= f . (((n2 -' 1) + ((Index (p,f)) + 1)) -' 1) by
.= f . ((n2 + (Index (p,f))) -' 1) by A84 ;
n2 -' 1 <= (len f) -' (Index (p,f)) by ;
then (n2 -' 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by ;
then (n2 + (Index (p,f))) -' 1 in dom f by ;
then (n1 + (Index (p,f))) -' 1 = (n2 + (Index (p,f))) -' 1 by ;
hence x1 = x2 by ; :: thesis: verum
end;
end;
end;
hence x1 = x2 ; :: thesis: verum
end;
then A100: g is one-to-one by FUNCT_1:def 4;
A101: ((len g) - 1) + 1 >= 1 + 1 by ;
A102: ((len f) -' ((Index (p,f)) + 1)) + 1 = (len f) - (Index (p,f)) by A20;
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
1 <= Index (p,f) by ;
then A103: 1 < (Index (p,f)) + 1 by NAT_1:13;
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
A104: 1 <= j and
A105: j + 1 <= len g ; :: thesis: ( (g /. j) `1 = (g /. (j + 1)) `1 or (g /. j) `2 = (g /. (j + 1)) `2 )
A106: LSeg (g,j) = LSeg ((g /. j),(g /. (j + 1))) by ;
(j + 1) - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1 by ;
then (j + 1) - 1 <= (len f) - (Index (p,f)) by ;
then A107: j + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by XREAL_1:6;
(Index (p,f)) + 1 <= (Index (p,f)) + j by ;
then 1 < (Index (p,f)) + j by ;
then A108: 1 <= ((Index (p,f)) + j) - 1 by SPPOL_1:1;
then A109: ((Index (p,f)) + j) - 1 = ((Index (p,f)) + j) -' 1 by XREAL_0:def 2;
then A110: LSeg (f,(((Index (p,f)) + j) -' 1)) = LSeg ((f /. (((Index (p,f)) + j) -' 1)),(f /. ((((Index (p,f)) + j) -' 1) + 1))) by ;
A111: ( (f /. (((Index (p,f)) + j) -' 1)) `1 = (f /. ((((Index (p,f)) + j) -' 1) + 1)) `1 or (f /. (((Index (p,f)) + j) -' 1)) `2 = (f /. ((((Index (p,f)) + j) -' 1) + 1)) `2 ) by ;
LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1)) by A2, A4, A104, A105, Th16;
hence ( (g /. j) `1 = (g /. (j + 1)) `1 or (g /. j) `2 = (g /. (j + 1)) `2 ) by ; :: thesis: verum
end;
then ( g is unfolded & g is s.n.c. & g is special ) by ;
then A112: g is being_S-Seq by ;
A113: ((len f) -' (Index (p,f))) + ((Index (p,f)) + 1) = ((len f) - (Index (p,f))) + ((Index (p,f)) + 1) by
.= (len f) + 1 ;
1 + ((len g) -' 1) = 1 + ((len g) - 1) by
.= len g ;
then g . (len g) = g . (() + ((len g) -' 1)) by FINSEQ_1:39
.= (mid (f,((Index (p,f)) + 1),(len f))) . ((len g) -' 1) by ;
then g . (len g) = f . (len f) by ;
then A114: g . (len g) = f /. (len f) by ;
g . 1 = p by ;
hence g is_S-Seq_joining p,f /. (len f) by ; :: thesis: verum