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:35;
then A5: len g = 1 + (len (mid f,((Index p,f) + 1),(len f))) by FINSEQ_1:56;
consider i being Element of 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
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 ; :: 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, Th49;
1 <= (Index p,f) + j1 by A2, Th41, NAT_1:12;
then 1 - 1 <= ((Index p,f) + j1) - 1 by XREAL_1:11;
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:8;
then (((Index p,f) + j1) + 1) - 1 < ((Index p,f) + j2) - 1 by XREAL_1:11;
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 9;
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, Th49;
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 5;
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, Th41;
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:11;
then A19: 1 - 1 <= ((len f) - (Index p,f)) - 1 by XREAL_1:11;
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:124;
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, Th49;
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, Th49;
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, Th41;
1 <= Index p,f by A2, Th41;
then 1 + 1 <= (Index p,f) + j by A24, XREAL_1:9;
then 1 <= ((Index p,f) + j) - 1 by XREAL_1:21;
then A31: 1 <= ((Index p,f) + j) -' 1 by NAT_D:39;
1 <= (Index p,f) + j by A2, Th41, NAT_1:12;
then A32: 1 - 1 <= ((Index p,f) + j) - 1 by XREAL_1:11;
((j + 1) + 1) - 1 <= (1 + (len (mid f,((Index p,f) + 1),(len f)))) - 1 by A5, A25, XREAL_1:11;
then A33: (j + 1) + (Index p,f) <= ((len f) - (Index p,f)) + (Index p,f) by A22, A20, XREAL_1:8;
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 8;
A36: 1 < j + 1 by A24, NAT_1:13;
then A37: g /. (j + 1) = g . (j + 1) by A27, FINSEQ_4:24;
A38: g /. (j + 1) in LSeg (g /. (j + 1)),(g /. ((j + 1) + 1)) by RLTOPSP1:69;
g /. (j + 1) in LSeg (g /. j),(g /. (j + 1)) by RLTOPSP1:69;
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 5;
LSeg (g /. (j + 1)),(g /. ((j + 1) + 1)) = LSeg g,(j + 1) by A25, A36, TOPREAL1:def 5;
then A41: {(g /. (j + 1))} c= (LSeg g,j) /\ (LSeg g,(j + 1)) by A40, A39, ZFMISC_1:37;
A42: j + 1 = ((j + 1) - 1) + 1
.= ((j + 1) -' 1) + 1 by A36, XREAL_1:235 ;
then A43: j + 1 = (len <*p*>) + ((j + 1) -' 1) by FINSEQ_1:56;
A44: (j + 1) -' 1 <= len (mid f,((Index p,f) + 1),(len f)) by A5, A27, A42, XREAL_1:8;
then (j + 1) -' 1 in dom (mid f,((Index p,f) + 1),(len f)) by A24, A42, FINSEQ_3:27;
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:124
.= f . (((((j + 1) -' 1) + 1) + (Index p,f)) -' 1)
.= f . (((j + 1) + (Index p,f)) -' 1) by A36, 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 A30, NAT_1:12, XREAL_1:237 ;
then A45: f /. ((((Index p,f) + j) -' 1) + 1) = g /. (j + 1) by A37, A34, FINSEQ_4:24, NAT_1:11;
((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 A30, NAT_1:12, XREAL_1:235 ;
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:35
.= 1 + (len (mid f,((Index p,f) + 1),(len f))) by FINSEQ_1:56 ;
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:27;
A50: (len f) - (Index p,f) >= 0 by A2, Th41, XREAL_1:52;
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:124;
A53: (len g) -' 1 = (len f) -' (Index p,f) by A47, A48, XREAL_0:def 2;
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 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:27;
A58: 1 <= n2 by A55, FINSEQ_3:27;
A59: n2 <= len g by A55, FINSEQ_3:27;
A60: 1 <= n1 by A54, 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 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:11;
n1 <= len <*p*> by A61, FINSEQ_1:56;
then n1 in dom <*p*> by A61, FINSEQ_3:27;
then A64: g . n1 = <*p*> . n1 by A4, FINSEQ_1:def 7;
n2 - 1 > 0 by A62, XREAL_1:52;
then A65: n2 -' 1 = n2 - 1 by XREAL_0:def 2;
then A66: (len <*p*>) + (n2 -' 1) = 1 + (n2 - 1) by FINSEQ_1:56
.= n2 ;
A67: 1 <= n2 -' 1 by A62, A65, SPPOL_1:6;
then n2 -' 1 in dom (mid f,((Index p,f) + 1),(len f)) by A65, A63, FINSEQ_3:27;
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:124
.= f . ((n2 + (Index p,f)) -' 1) by A65 ;
then A68: f . ((n2 + (Index p,f)) -' 1) = p by A56, A61, A64, FINSEQ_1:57;
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:235;
then A69: (n2 - 1) + (Index p,f) <= ((len f) - (Index p,f)) + (Index p,f) by XREAL_1:8;
1 + 1 < n2 + (Index p,f) by A2, A62, Th41, XREAL_1:10;
then A70: 1 < (n2 + (Index p,f)) - 1 by XREAL_1:22;
then (n2 + (Index p,f)) -' 1 = (n2 + (Index p,f)) - 1 by XREAL_0:def 2;
hence contradiction by A1, A3, A70, A68, A69, Th45; :: 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:11;
n2 <= len <*p*> by A72, FINSEQ_1:56;
then n2 in dom <*p*> by A72, FINSEQ_3:27;
then A74: g . n2 = <*p*> . n2 by A4, FINSEQ_1:def 7;
n1 - 1 > 0 by A71, XREAL_1:52;
then A75: n1 -' 1 = n1 - 1 by XREAL_0:def 2;
then A76: (len <*p*>) + (n1 -' 1) = 1 + (n1 - 1) by FINSEQ_1:56
.= n1 ;
A77: 1 <= n1 -' 1 by A71, A75, SPPOL_1:6;
then n1 -' 1 in dom (mid f,((Index p,f) + 1),(len f)) by A75, A73, FINSEQ_3:27;
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:124
.= f . ((n1 + (Index p,f)) -' 1) by A75 ;
then A78: f . ((n1 + (Index p,f)) -' 1) = p by A56, A72, A74, FINSEQ_1:57;
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:235;
then A79: (n1 - 1) + (Index p,f) <= ((len f) - (Index p,f)) + (Index p,f) by XREAL_1:8;
1 + 1 < n1 + (Index p,f) by A2, A71, Th41, XREAL_1:10;
then A80: 1 < (n1 + (Index p,f)) - 1 by XREAL_1:22;
then (n1 + (Index p,f)) -' 1 = (n1 + (Index p,f)) - 1 by XREAL_0:def 2;
hence contradiction by A1, A3, A80, A78, A79, Th45; :: thesis: verum
end;
case that A81: n1 > 1 and
A82: n2 > 1 ; :: thesis: x1 = x2
A83: n2 - 1 > 0 by A82, XREAL_1:52;
then A84: n2 -' 1 = n2 - 1 by XREAL_0:def 2;
then A85: (len <*p*>) + (n2 -' 1) = 1 + (n2 - 1) by FINSEQ_1:56
.= n2 ;
A86: n1 - 1 > 0 by A81, XREAL_1:52;
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:56
.= n1 ;
A92: n1 - 1 <= (1 + (len (mid f,((Index p,f) + 1),(len f)))) - 1 by A5, A57, XREAL_1:11;
then n1 -' 1 in dom (mid f,((Index p,f) + 1),(len f)) by A87, A88, FINSEQ_3:27;
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:124
.= 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:8;
then A94: (n1 + (Index p,f)) -' 1 in dom f by A87, A89, A90, FINSEQ_3:27;
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:11;
then n2 -' 1 in dom (mid f,((Index p,f) + 1),(len f)) by A84, A95, FINSEQ_3:27;
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:124
.= 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:8;
then (n2 + (Index p,f)) -' 1 in dom f by A84, A96, A97, FINSEQ_3:27;
then (n1 + (Index p,f)) -' 1 = (n2 + (Index p,f)) -' 1 by A1, A56, A99, A93, A94, FUNCT_1:def 8;
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 8;
A101: ((len g) - 1) + 1 >= 1 + 1 by A18, A47, XREAL_1:8;
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, Th41;
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 5;
(j + 1) - 1 <= (1 + (len (mid f,((Index p,f) + 1),(len f)))) - 1 by A5, A105, XREAL_1:11;
then (j + 1) - 1 <= (len f) - (Index p,f) by A7, A17, A21, A102, FINSEQ_6:124;
then A107: j + (Index p,f) <= ((len f) - (Index p,f)) + (Index p,f) by XREAL_1:8;
(Index p,f) + 1 <= (Index p,f) + j by A104, XREAL_1:8;
then 1 < (Index p,f) + j by A103, XXREAL_0:2;
then A108: 1 <= ((Index p,f) + j) - 1 by SPPOL_1:6;
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 5;
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 7;
LSeg g,j c= LSeg f,(((Index p,f) + j) -' 1) by A2, A4, A104, A105, Th49;
hence ( (g /. j) `1 = (g /. (j + 1)) `1 or (g /. j) `2 = (g /. (j + 1)) `2 ) by A106, A110, A111, Th36; :: thesis: verum
end;
then ( g is unfolded & g is s.n.c. & g is special ) by A23, A8, TOPREAL1:def 7, TOPREAL1:def 8, TOPREAL1:def 9;
then A112: g is being_S-Seq by A101, A100, TOPREAL1:def 10;
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:56
.= (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:24;
g . 1 = p by A4, FINSEQ_1:58;
hence g is_S-Seq_joining p,f /. (len f) by A112, A114, Def3; :: thesis: verum