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, Th8;

A6: for j1, j2 being Nat st j1 + 1 < j2 holds

LSeg (g,j1) misses LSeg (g,j2)

n1 = n2

.= (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 A2, SPPOL_2:13;

A22: 1 <= Index (p,f) by A2, Th8;

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:118;

then A25: len (mid (f,1,(Index (p,f)))) = Index (p,f) by A2, Th8, XREAL_1:235;

then g . 1 = (mid (f,1,(Index (p,f)))) . 1 by A4, A22, FINSEQ_6:109;

then g . 1 = f . 1 by A22, A5, A23, FINSEQ_6:118;

then A26: g . 1 = f /. 1 by A23, FINSEQ_4:15;

A27: for j being Nat st 1 <= j & j + 2 <= len g holds

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

(g /. j) `2 = (g /. (j + 1)) `2

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

1 + 1 <= len g by A22, A25, A20, XREAL_1:6;

then A79: g is being_S-Seq by A78, A51, TOPREAL1:def 8;

g . (len g) = p by A4, A20, FINSEQ_1:42;

hence g is_S-Seq_joining f /. 1,p by A26, A79; :: thesis: verum

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, Th8;

A6: for j1, j2 being Nat st j1 + 1 < j2 holds

LSeg (g,j1) misses LSeg (g,j2)

proof

A13:
for n1, n2 being Element of NAT st 1 <= n1 & n1 <= len f & 1 <= n2 & n2 <= len f & f . n1 = f . n2 holds
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;

end;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) ) )end;

hence
LSeg (g,j1) misses LSeg (g,j2)
; :: thesis: verumper cases
( j1 = 0 or ( ( j1 = 1 or j1 > 1 ) & j2 + 1 <= len g ) or j2 + 1 > len g )
by A8, XXREAL_0:1;

end;

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;then (LSeg (g,j1)) /\ (LSeg (g,j2)) = {} ;

hence LSeg (g,j1) misses LSeg (g,j2) by XBOOLE_0:def 7; :: thesis: verum

case that A9:
( j1 = 1 or j1 > 1 )
and

A10: j2 + 1 <= len g ; :: thesis: LSeg (g,j1) misses LSeg (g,j2)

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, Th18;

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, Th18;

LSeg (f,j1) misses LSeg (f,j2) by A1, A7, TOPREAL1:def 7;

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;then j1 + 1 < len g by A7, XXREAL_0:2;

then A11: LSeg (g,j1) c= LSeg (f,j1) by A2, A4, A9, Th18;

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, Th18;

LSeg (f,j1) misses LSeg (f,j2) by A1, A7, TOPREAL1:def 7;

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

n1 = n2

proof

A20: len g =
(len (mid (f,1,(Index (p,f))))) + (len <*p*>)
by A4, FINSEQ_1:22
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:25;

n1 in dom f by A14, A15, FINSEQ_3:25;

hence n1 = n2 by A1, A18, A19, FUNCT_1:def 4; :: thesis: verum

end;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:25;

n1 in dom f by A14, A15, FINSEQ_3:25;

hence n1 = n2 by A1, A18, A19, FUNCT_1:def 4; :: thesis: verum

.= (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 A2, SPPOL_2:13;

A22: 1 <= Index (p,f) by A2, Th8;

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:118;

then A25: len (mid (f,1,(Index (p,f)))) = Index (p,f) by A2, Th8, XREAL_1:235;

then g . 1 = (mid (f,1,(Index (p,f)))) . 1 by A4, A22, FINSEQ_6:109;

then g . 1 = f . 1 by A22, A5, A23, FINSEQ_6:118;

then A26: g . 1 = f /. 1 by A23, FINSEQ_4:15;

A27: for j being Nat st 1 <= j & j + 2 <= len g holds

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

proof

for j being Nat st 1 <= j & j + 1 <= len g & not (g /. j) `1 = (g /. (j + 1)) `1 holds
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 3;

then A31: g /. (j + 1) in LSeg (g,j) by RLTOPSP1:68;

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 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 A31, XBOOLE_0:def 4;

then A33: {(g /. (j + 1))} c= (LSeg (g,j)) /\ (LSeg (g,(j + 1))) by ZFMISC_1:31;

j + 1 <= len g by A29, NAT_D:47;

then A34: LSeg (g,j) c= LSeg (f,j) by A2, A4, A28, Th18;

A35: Index (p,f) <= len f by A2, Th8;

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 A34, XBOOLE_1:27;

A38: g /. (j + 1) = g . (j + 1) by A32, A30, FINSEQ_4:15;

end;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 3;

then A31: g /. (j + 1) in LSeg (g,j) by RLTOPSP1:68;

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 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 A31, XBOOLE_0:def 4;

then A33: {(g /. (j + 1))} c= (LSeg (g,j)) /\ (LSeg (g,(j + 1))) by ZFMISC_1:31;

j + 1 <= len g by A29, NAT_D:47;

then A34: LSeg (g,j) c= LSeg (f,j) by A2, A4, A28, Th18;

A35: Index (p,f) <= len f by A2, Th8;

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 A34, XBOOLE_1:27;

A38: g /. (j + 1) = g . (j + 1) by A32, A30, FINSEQ_4:15;

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

hence
(LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))}
; :: thesis: verumA39:
len g = (len (mid (f,1,(Index (p,f))))) + 1
by A4, FINSEQ_2:16;

Index (p,f) <= len f by A2, Th8;

then A40: len g <= (len f) + 1 by A25, A39, XREAL_1:6;

end;Index (p,f) <= len f by A2, Th8;

then A40: len g <= (len f) + 1 by A25, A39, 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))} ) )end;

hence
(LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))}
; :: thesis: verumper cases
( len g = (len f) + 1 or len g < (len f) + 1 )
by A40, XXREAL_0:1;

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 6;

A42: j + 1 <= Index (p,f) by A25, A36, A39, XREAL_1:6;

then j + 1 <= len f by A35, XXREAL_0:2;

then A43: f . (j + 1) = f /. (j + 1) by A32, FINSEQ_4:15;

g . (j + 1) = (mid (f,1,(Index (p,f)))) . (j + 1) by A4, A25, A32, A42, FINSEQ_1:64

.= f . (j + 1) by A5, A32, A42, FINSEQ_6:123 ;

hence (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} by A38, A33, A41, A43, XBOOLE_0:def 10; :: thesis: verum

end;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 6;

A42: j + 1 <= Index (p,f) by A25, A36, A39, XREAL_1:6;

then j + 1 <= len f by A35, XXREAL_0:2;

then A43: f . (j + 1) = f /. (j + 1) by A32, FINSEQ_4:15;

g . (j + 1) = (mid (f,1,(Index (p,f)))) . (j + 1) by A4, A25, A32, A42, FINSEQ_1:64

.= f . (j + 1) by A5, A32, A42, FINSEQ_6:123 ;

hence (LSeg (g,j)) /\ (LSeg (g,(j + 1))) = {(g /. (j + 1))} by A38, A33, A41, A43, XBOOLE_0:def 10; :: thesis: verum

(g /. j) `2 = (g /. (j + 1)) `2

proof

then A51:
( g is unfolded & g is s.n.c. & g is special )
by A27, A6, TOPREAL1:def 5, TOPREAL1:def 6, TOPREAL1:def 7;
A44:
Index (p,f) < len f
by A2, Th8;

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 3;

j + 1 <= (Index (p,f)) + 1 by A4, A25, A46, FINSEQ_2:16;

then j <= Index (p,f) by XREAL_1:6;

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 3;

A50: ( (f /. j) `1 = (f /. (j + 1)) `1 or (f /. j) `2 = (f /. (j + 1)) `2 ) by A1, A45, A48, TOPREAL1:def 5;

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;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 3;

j + 1 <= (Index (p,f)) + 1 by A4, A25, A46, FINSEQ_2:16;

then j <= Index (p,f) by XREAL_1:6;

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 3;

A50: ( (f /. j) `1 = (f /. (j + 1)) `1 or (f /. j) `2 = (f /. (j + 1)) `2 ) by A1, A45, A48, TOPREAL1:def 5;

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

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

then A78:
g is one-to-one
by FUNCT_1:def 4;
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 A53, A54;

A56: 1 <= n1 by A53, FINSEQ_3:25;

A57: n2 <= len g by A54, FINSEQ_3:25;

A58: 1 <= n2 by A54, FINSEQ_3:25;

A59: n1 <= len g by A53, FINSEQ_3:25;

end;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:25;

A57: n2 <= len g by A54, FINSEQ_3:25;

A58: 1 <= n2 by A54, FINSEQ_3:25;

A59: n1 <= len g by A53, FINSEQ_3:25;

now :: thesis: x1 = x2

hence
x1 = x2
; :: thesis: verumA60: g . (len g) =
<*p*> . 1
by A4, A52, A20, FINSEQ_1:def 7

.= p by FINSEQ_1:def 8 ;

end;.= 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 ) )end;

hence
x1 = x2
; :: thesis: verumper cases
( n1 = len g or n2 = len g or ( n1 <> len g & n2 <> len g ) )
;

end;

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

end;

now :: thesis: not n2 <> len g

hence
x1 = x2
by A61; :: thesis: verumassume 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:64;

then g . n2 = f . ((n2 + 1) -' 1) by A22, A5, A23, A58, A63, FINSEQ_6:118;

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, Th12;

hence contradiction by A2, A24, A20, A62, Th8, XREAL_1:235; :: thesis: verum

end;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:64;

then g . n2 = f . ((n2 + 1) -' 1) by A22, A5, A23, A58, A63, FINSEQ_6:118;

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, Th12;

hence contradiction by A2, A24, A20, A62, Th8, XREAL_1:235; :: thesis: verum

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

end;

now :: thesis: not n1 <> len g

hence
x1 = x2
by A66; :: thesis: verumassume 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:64;

then g . n1 = f . ((n1 + 1) -' 1) by A22, A5, A23, A56, A68, FINSEQ_6:118;

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, Th12;

hence contradiction by A2, A24, A20, A67, Th8, XREAL_1:235; :: thesis: verum

end;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:64;

then g . n1 = f . ((n1 + 1) -' 1) by A22, A5, A23, A56, A68, FINSEQ_6:118;

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, Th12;

hence contradiction by A2, A24, A20, A67, Th8, XREAL_1:235; :: thesis: verum

case that A71:
n1 <> len g
and

A72: n2 <> len g ; :: thesis: x1 = x2

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:64

.= f . n2 by A5, A25, A58, A75, FINSEQ_6:123 ;

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:64

.= f . n1 by A5, A25, A56, A73, FINSEQ_6:123 ;

hence x1 = x2 by A13, A55, A56, A58, A74, A77, A76; :: thesis: verum

end;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:64

.= f . n2 by A5, A25, A58, A75, FINSEQ_6:123 ;

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:64

.= f . n1 by A5, A25, A56, A73, FINSEQ_6:123 ;

hence x1 = x2 by A13, A55, A56, A58, A74, A77, A76; :: thesis: verum

1 + 1 <= len g by A22, A25, A20, XREAL_1:6;

then A79: g is being_S-Seq by A78, A51, TOPREAL1:def 8;

g . (len g) = p by A4, A20, FINSEQ_1:42;

hence g is_S-Seq_joining f /. 1,p by A26, A79; :: thesis: verum