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