let f, g be FinSequence of (TOP-REAL 2); 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); ( 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)))
; 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;
( j1 + 1 < j2 implies LSeg (g,j1) misses LSeg (g,j2) )
assume A9:
j1 + 1
< j2
;
LSeg (g,j1) misses LSeg (g,j2)
A10:
(
j1 = 0 or
j1 >= 0 + 1 )
by NAT_1:13;
now ( ( 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 that A11:
(
j1 = 1 or
j1 > 1 )
and A12:
j2 + 1
<= len g
;
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;
verum end; end; end;
hence
LSeg (
g,
j1)
misses LSeg (
g,
j2)
;
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;
( 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
;
(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;
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 ;
( 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
;
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 ( ( 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 )
;
x1 = x2end; case that A61:
n1 = 1
and A62:
n2 > 1
;
contradictionA63:
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;
verum end; case that A71:
n1 > 1
and A72:
n2 = 1
;
contradictionA73:
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;
verum end; case that A81:
n1 > 1
and A82:
n2 > 1
;
x1 = x2A83:
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;
verum end; end; end;
hence
x1 = x2
;
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;
( 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
;
( (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;
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; verum