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 . ((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 (TOP-REAL 2); :: 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 <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) by A4, FINSEQ_1:22;
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 A2, SPPOL_2:13;
1 <= 1 + i by NAT_1:12;
then A7: 1 <= len f by A6, XXREAL_0:2;
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 A10, 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) 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 A11, NAT_1:13;
then 1 <= j2 by A9, XXREAL_0:2;
then A13: LSeg (g,j2) c= LSeg (f,(((Index (p,f)) + j2) -' 1)) by A2, A4, A12, Th16;
1 <= (Index (p,f)) + j1 by A2, Th8, NAT_1:12;
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 A9, XREAL_1:6;
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 A14, XREAL_0:def 2;
then LSeg (f,(((Index (p,f)) + j1) -' 1)) misses LSeg (f,(((Index (p,f)) + j2) -' 1)) by A1, TOPREAL1:def 7;
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 A12, NAT_1:13;
then j1 + 1 <= len g by A9, XXREAL_0:2;
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 A13, A15, 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 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 A2, Th8;
then A17: (Index (p,f)) + 1 <= len f by NAT_1:13;
(Index (p,f)) + 1 <= len f by A16, NAT_1:13;
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 A7, A17, FINSEQ_6:118;
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 A25, NAT_1:13;
then A28: LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1)) by A2, A4, A24, Th16;
1 <= j + 1 by A24, NAT_1:13;
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 A28, XBOOLE_1:27;
A30: 1 <= Index (p,f) by A2, Th8;
1 <= Index (p,f) by A2, Th8;
then 1 + 1 <= (Index (p,f)) + j by A24, XREAL_1:7;
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 A2, Th8, NAT_1:12;
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 A5, A25, XREAL_1:9;
then A33: (j + 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by A22, A20, XREAL_1:6;
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 A32, XREAL_0:def 2;
(((Index (p,f)) + j) - 1) + (1 + 1) <= len f by A33;
then (((Index (p,f)) + j) -' 1) + 2 <= len f by A32, XREAL_0:def 2;
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 A1, A31, TOPREAL1:def 6;
A36: 1 < j + 1 by A24, NAT_1:13;
then A37: g /. (j + 1) = g . (j + 1) by A27, FINSEQ_4:15;
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 A38, XBOOLE_0:def 4;
A40: LSeg (g,j) = LSeg ((g /. j),(g /. (j + 1))) by A24, A27, TOPREAL1:def 3;
LSeg ((g /. (j + 1)),(g /. ((j + 1) + 1))) = LSeg (g,(j + 1)) by A25, A36, TOPREAL1:def 3;
then A41: {(g /. (j + 1))} c= (LSeg (g,j)) /\ (LSeg (g,(j + 1))) by A40, A39, ZFMISC_1:31;
A42: j + 1 = ((j + 1) - 1) + 1
.= ((j + 1) -' 1) + 1 by A36, XREAL_1:233 ;
then A43: j + 1 = (len <*p*>) + ((j + 1) -' 1) by FINSEQ_1:39;
A44: (j + 1) -' 1 <= len (mid (f,((Index (p,f)) + 1),(len f))) by A5, A27, A42, XREAL_1:6;
then (j + 1) -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A24, A42, FINSEQ_3:25;
then g . (j + 1) = (mid (f,((Index (p,f)) + 1),(len f))) . ((j + 1) -' 1) by A4, A43, FINSEQ_1:def 7
.= f . ((((j + 1) -' 1) + ((Index (p,f)) + 1)) -' 1) by A7, A17, A21, A24, A42, A44, FINSEQ_6:118
.= f . (((((j + 1) -' 1) + 1) + (Index (p,f))) -' 1)
.= f . (((j + 1) + (Index (p,f))) -' 1) by A36, XREAL_1:235
.= f . ((((Index (p,f)) + j) + 1) -' 1)
.= f . ((Index (p,f)) + j) by NAT_D:34
.= f . ((((Index (p,f)) + j) -' 1) + 1) by A30, NAT_1:12, XREAL_1:235 ;
then A45: f /. ((((Index (p,f)) + j) -' 1) + 1) = g /. (j + 1) by A37, A34, FINSEQ_4:15, NAT_1:11;
((Index (p,f)) + (j + 1)) -' 1 = (((Index (p,f)) + j) + 1) - 1 by NAT_1:11, XREAL_1:233
.= (((Index (p,f)) + j) - 1) + 1
.= (((Index (p,f)) + j) -' 1) + 1 by A30, NAT_1:12, XREAL_1:233 ;
hence (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} by A29, A35, A45, A41, XBOOLE_0:def 10; :: thesis: verum
end;
A46: len g = (len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) by A4, FINSEQ_1:22
.= 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 A19, A22, XREAL_0:def 2
.= 1 + ((len f) - (Index (p,f))) ;
then A48: (len g) -' 1 = (len g) - 1 by A18, XREAL_0:def 2;
then A49: (len g) -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A18, A22, A47, A20, FINSEQ_3:25;
A50: (len f) - (Index (p,f)) >= 0 by A2, Th8, XREAL_1:50;
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 A7, A18, A17, A21, A22, A20, FINSEQ_6:118;
A53: (len g) -' 1 = (len f) -' (Index (p,f)) by A47, A48, XREAL_0:def 2;
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 A54, A55;
A57: n1 <= len g by A54, FINSEQ_3:25;
A58: 1 <= n2 by A55, FINSEQ_3:25;
A59: n2 <= len g by A55, FINSEQ_3:25;
A60: 1 <= n1 by A54, FINSEQ_3:25;
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 A60, A58, XXREAL_0:1;
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 A5, A59, XREAL_1:9;
n1 <= len <*p*> by A61, FINSEQ_1:39;
then n1 in dom <*p*> by A61, FINSEQ_3:25;
then A64: g . n1 = <*p*> . n1 by A4, FINSEQ_1:def 7;
n2 - 1 > 0 by A62, XREAL_1:50;
then A65: n2 -' 1 = n2 - 1 by XREAL_0:def 2;
then A66: (len <*p*>) + (n2 -' 1) = 1 + (n2 - 1) by FINSEQ_1:39
.= n2 ;
A67: 1 <= n2 -' 1 by A62, A65, SPPOL_1:1;
then n2 -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A65, A63, FINSEQ_3:25;
then g . n2 = (mid (f,((Index (p,f)) + 1),(len f))) . (n2 -' 1) by A4, A66, FINSEQ_1:def 7
.= f . (((n2 -' 1) + ((Index (p,f)) + 1)) -' 1) by A7, A17, A21, A65, A63, A67, FINSEQ_6:118
.= f . ((n2 + (Index (p,f))) -' 1) by A65 ;
then A68: f . ((n2 + (Index (p,f))) -' 1) = p by A56, A61, A64, FINSEQ_1:40;
n2 -' 1 <= (len f) - (Index (p,f)) by A47, A48, A59, NAT_D:42;
then n2 - 1 <= (len f) - (Index (p,f)) by A62, XREAL_1:233;
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 A2, A62, Th8, XREAL_1:8;
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 A5, A57, XREAL_1:9;
n2 <= len <*p*> by A72, FINSEQ_1:39;
then n2 in dom <*p*> by A72, FINSEQ_3:25;
then A74: g . n2 = <*p*> . n2 by A4, FINSEQ_1:def 7;
n1 - 1 > 0 by A71, XREAL_1:50;
then A75: n1 -' 1 = n1 - 1 by XREAL_0:def 2;
then A76: (len <*p*>) + (n1 -' 1) = 1 + (n1 - 1) by FINSEQ_1:39
.= n1 ;
A77: 1 <= n1 -' 1 by A71, A75, SPPOL_1:1;
then n1 -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A75, A73, FINSEQ_3:25;
then g . n1 = (mid (f,((Index (p,f)) + 1),(len f))) . (n1 -' 1) by A4, A76, FINSEQ_1:def 7
.= f . (((n1 -' 1) + ((Index (p,f)) + 1)) -' 1) by A7, A17, A21, A75, A73, A77, FINSEQ_6:118
.= f . ((n1 + (Index (p,f))) -' 1) by A75 ;
then A78: f . ((n1 + (Index (p,f))) -' 1) = p by A56, A72, A74, FINSEQ_1:40;
n1 -' 1 <= (len f) - (Index (p,f)) by A47, A48, A57, NAT_D:42;
then n1 - 1 <= (len f) - (Index (p,f)) by A71, XREAL_1:233;
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 A2, A71, Th8, XREAL_1:8;
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 A82, XREAL_1:50;
then A84: n2 -' 1 = n2 - 1 by XREAL_0:def 2;
then A85: (len <*p*>) + (n2 -' 1) = 1 + (n2 - 1) by FINSEQ_1:39
.= n2 ;
A86: n1 - 1 > 0 by A81, XREAL_1:50;
then A87: n1 -' 1 = n1 - 1 by XREAL_0:def 2;
then A88: 0 + 1 <= n1 -' 1 by A86, NAT_1:13;
then A89: 1 <= (n1 - 1) + (Index (p,f)) by A87, NAT_1:12;
then A90: (n1 + (Index (p,f))) -' 1 = (n1 + (Index (p,f))) - 1 by XREAL_0:def 2;
A91: (len <*p*>) + (n1 -' 1) = 1 + (n1 - 1) by A87, FINSEQ_1:39
.= n1 ;
A92: n1 - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1 by A5, A57, XREAL_1:9;
then n1 -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A87, A88, FINSEQ_3:25;
then A93: g . n1 = (mid (f,((Index (p,f)) + 1),(len f))) . (n1 -' 1) by A4, A91, FINSEQ_1:def 7
.= f . (((n1 -' 1) + ((Index (p,f)) + 1)) -' 1) by A7, A17, A21, A87, A88, A92, FINSEQ_6:118
.= f . ((n1 + (Index (p,f))) -' 1) by A87 ;
n1 -' 1 <= (len f) -' (Index (p,f)) by A53, A57, NAT_D:42;
then (n1 -' 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by A51, XREAL_1:6;
then A94: (n1 + (Index (p,f))) -' 1 in dom f by A87, A89, A90, FINSEQ_3:25;
A95: 0 + 1 <= n2 -' 1 by A83, A84, NAT_1:13;
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 A84, XREAL_0:def 2;
A98: n2 - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1 by A5, A59, XREAL_1:9;
then n2 -' 1 in dom (mid (f,((Index (p,f)) + 1),(len f))) by A84, A95, FINSEQ_3:25;
then A99: g . n2 = (mid (f,((Index (p,f)) + 1),(len f))) . (n2 -' 1) by A4, A85, FINSEQ_1:def 7
.= f . (((n2 -' 1) + ((Index (p,f)) + 1)) -' 1) by A7, A17, A21, A84, A95, A98, FINSEQ_6:118
.= f . ((n2 + (Index (p,f))) -' 1) by A84 ;
n2 -' 1 <= (len f) -' (Index (p,f)) by A53, A59, NAT_D:42;
then (n2 -' 1) + (Index (p,f)) <= ((len f) - (Index (p,f))) + (Index (p,f)) by A51, XREAL_1:6;
then (n2 + (Index (p,f))) -' 1 in dom f by A84, A96, A97, FINSEQ_3:25;
then (n1 + (Index (p,f))) -' 1 = (n2 + (Index (p,f))) -' 1 by A1, A56, A99, A93, A94, FUNCT_1:def 4;
hence x1 = x2 by A97, A90; :: 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 A18, A47, XREAL_1:6;
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 A2, Th8;
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 A104, A105, TOPREAL1:def 3;
(j + 1) - 1 <= (1 + (len (mid (f,((Index (p,f)) + 1),(len f))))) - 1 by A5, A105, XREAL_1:9;
then (j + 1) - 1 <= (len f) - (Index (p,f)) by A7, A17, A21, A102, FINSEQ_6:118;
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 A104, XREAL_1:6;
then 1 < (Index (p,f)) + j by A103, XXREAL_0:2;
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 A108, A107, TOPREAL1:def 3;
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 A1, A108, A109, A107, TOPREAL1:def 5;
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 A106, A110, A111, Th3; :: thesis: verum
end;
then ( g is unfolded & g is s.n.c. & g is special ) by A23, A8, TOPREAL1:def 5, TOPREAL1:def 6, TOPREAL1:def 7;
then A112: g is being_S-Seq by A101, A100, TOPREAL1:def 8;
A113: ((len f) -' (Index (p,f))) + ((Index (p,f)) + 1) = ((len f) - (Index (p,f))) + ((Index (p,f)) + 1) by A50, XREAL_0:def 2
.= (len f) + 1 ;
1 + ((len g) -' 1) = 1 + ((len g) - 1) by A46, XREAL_0:def 2
.= len g ;
then g . (len g) = g . ((len <*p*>) + ((len g) -' 1)) by FINSEQ_1:39
.= (mid (f,((Index (p,f)) + 1),(len f))) . ((len g) -' 1) by A4, A49, FINSEQ_1:def 7 ;
then g . (len g) = f . (len f) by A47, A48, A52, A113, NAT_D:34;
then A114: g . (len g) = f /. (len f) by A7, FINSEQ_4:15;
g . 1 = p by A4, FINSEQ_1:41;
hence g is_S-Seq_joining p,f /. (len f) by A112, A114; :: thesis: verum