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
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;
A6: 1 <= Index p,f by A2, Th41;
A7: Index p,f <= len f by A2, Th41;
1 <= 1 + i by NAT_1:12;
then A8: 1 <= len f by A5, XXREAL_0:2;
then A9: len (mid f,1,(Index p,f)) = ((Index p,f) -' 1) + 1 by A6, A7, Th27;
then A10: len (mid f,1,(Index p,f)) = Index p,f by A6, XREAL_1:237;
1 <= len <*p*> by FINSEQ_1:56;
then A11: 1 in dom <*p*> by FINSEQ_3:27;
g . 1 = (mid f,1,(Index p,f)) . 1 by A4, A6, A10, Th17;
then g . 1 = f . 1 by A6, A7, A8, Th27;
then A12: g . 1 = f /. 1 by A8, FINSEQ_4:24;
A13: len g = (len (mid f,1,(Index p,f))) + (len <*p*>) by A4, FINSEQ_1:35
.= (len (mid f,1,(Index p,f))) + 1 by FINSEQ_1:56 ;
then A14: g . (len g) = p by A4, FINSEQ_1:59;
A15: 1 + 1 <= len g by A6, A10, A13, XREAL_1:8;
A16: f is one-to-one by A1;
A17: for n1, n2 being Element of NAT st 1 <= n1 & n1 <= len f & 1 <= n2 & n2 <= len f & f . n1 = f . n2 holds
n1 = n2
proof
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 A18: ( 1 <= n1 & n1 <= len f & 1 <= n2 & n2 <= len f & f . n1 = f . n2 ) ; :: thesis: n1 = n2
then ( n1 in dom f & n2 in dom f ) by FINSEQ_3:27;
hence n1 = n2 by A16, A18, FUNCT_1:def 8; :: thesis: verum
end;
A19: 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 A20: ( 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 ;
A21: ( 1 <= n1 & n1 <= len g & 1 <= n2 & n2 <= len g ) by A20, FINSEQ_3:27;
now
A22: g . (len g) = <*p*> . 1 by A4, A11, A13, FINSEQ_1:def 7
.= p by FINSEQ_1:def 8 ;
now
per cases ( n1 = len g or n2 = len g or ( n1 <> len g & n2 <> len g ) ) ;
case A23: n1 = len g ; :: thesis: x1 = x2
now
assume A24: n2 <> len g ; :: thesis: contradiction
then n2 < len g by A21, XXREAL_0:1;
then A25: n2 <= len (mid f,1,(Index p,f)) by A13, NAT_1:13;
then g . n2 = (mid f,1,(Index p,f)) . n2 by A4, A21, FINSEQ_1:85;
then g . n2 = f . ((n2 + 1) -' 1) by A6, A7, A8, A21, A25, Th27;
then A26: p = f . n2 by A20, A22, A23, NAT_D:34;
A27: n2 <= len f by A7, A10, A25, XXREAL_0:2;
1 < n2 by A3, A21, A26, XXREAL_0:1;
then (Index p,f) + 1 = n2 by A1, A26, A27, Th45;
hence contradiction by A6, A9, A13, A24, XREAL_1:237; :: thesis: verum
end;
hence x1 = x2 by A23; :: thesis: verum
end;
case A28: n2 = len g ; :: thesis: x1 = x2
now
assume A29: n1 <> len g ; :: thesis: contradiction
then n1 < len g by A21, XXREAL_0:1;
then A30: n1 <= len (mid f,1,(Index p,f)) by A13, NAT_1:13;
then g . n1 = (mid f,1,(Index p,f)) . n1 by A4, A21, FINSEQ_1:85;
then g . n1 = f . ((n1 + 1) -' 1) by A6, A7, A8, A21, A30, Th27;
then A31: p = f . n1 by A20, A22, A28, NAT_D:34;
A32: n1 <= len f by A7, A10, A30, XXREAL_0:2;
1 < n1 by A3, A21, A31, XXREAL_0:1;
then (Index p,f) + 1 = n1 by A1, A31, A32, Th45;
hence contradiction by A6, A9, A13, A29, XREAL_1:237; :: thesis: verum
end;
hence x1 = x2 by A28; :: thesis: verum
end;
case that A33: n1 <> len g and
A34: n2 <> len g ; :: thesis: x1 = x2
n1 < len g by A21, A33, XXREAL_0:1;
then A35: n1 <= len (mid f,1,(Index p,f)) by A13, NAT_1:13;
then A36: n1 <= len f by A7, A10, XXREAL_0:2;
A37: g . n1 = (mid f,1,(Index p,f)) . n1 by A4, A21, A35, FINSEQ_1:85
.= f . n1 by A7, A10, A21, A35, Th32 ;
n2 < len g by A21, A34, XXREAL_0:1;
then A38: n2 <= len (mid f,1,(Index p,f)) by A13, NAT_1:13;
then A39: n2 <= len f by A7, A10, XXREAL_0:2;
g . n2 = (mid f,1,(Index p,f)) . n2 by A4, A21, A38, FINSEQ_1:85
.= f . n2 by A7, A10, A21, A38, Th32 ;
hence x1 = x2 by A17, A20, A21, A36, A37, A39; :: thesis: verum
end;
end;
end;
hence x1 = x2 ; :: thesis: verum
end;
hence x1 = x2 ; :: thesis: verum
end;
A40: f is unfolded by A1;
A41: 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 A42: ( 1 <= j & j + 2 <= len g ) ; :: thesis: (LSeg g,j) /\ (LSeg g,(j + 1)) = {(g /. (j + 1))}
then j + 1 <= len g by NAT_D:47;
then A43: LSeg g,j c= LSeg f,j by A2, A4, A42, Th51;
A44: (j + 1) + 1 <= len g by A42;
A45: 1 <= j + 1 by A42, NAT_D:48;
then LSeg g,(j + 1) c= LSeg f,(j + 1) by A2, A4, A44, Th51;
then A46: (LSeg g,j) /\ (LSeg g,(j + 1)) c= (LSeg f,j) /\ (LSeg f,(j + 1)) by A43, XBOOLE_1:27;
A47: j + 1 <= len g by A42, NAT_D:47;
then LSeg g,j = LSeg (g /. j),(g /. (j + 1)) by A42, TOPREAL1:def 5;
then A48: g /. (j + 1) in LSeg g,j by RLTOPSP1:69;
A49: g /. (j + 1) = g . (j + 1) by A45, A47, FINSEQ_4:24;
A50: Index p,f <= len f by A2, Th41;
LSeg g,(j + 1) = LSeg (g /. (j + 1)),(g /. ((j + 1) + 1)) by A42, A45, TOPREAL1:def 5;
then g /. (j + 1) in LSeg g,(j + 1) by RLTOPSP1:69;
then g /. (j + 1) in (LSeg g,j) /\ (LSeg g,(j + 1)) by A48, XBOOLE_0:def 4;
then A51: {(g /. (j + 1))} c= (LSeg g,j) /\ (LSeg g,(j + 1)) by ZFMISC_1:37;
now
A52: len g = (len (mid f,1,(Index p,f))) + 1 by A4, FINSEQ_2:19;
Index p,f <= len f by A2, Th41;
then A53: len g <= (len f) + 1 by A10, A52, XREAL_1:8;
now
per cases ( len g = (len f) + 1 or len g < (len f) + 1 ) by A53, XXREAL_0:1;
case len g = (len f) + 1 ; :: thesis: contradiction
hence contradiction by A2, A10, A52, Th41; :: thesis: verum
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 A54: j + 2 <= len f by A42, XXREAL_0:2;
A55: j + 1 <= Index p,f by A10, A44, A52, XREAL_1:8;
then A56: j + 1 <= len f by A50, XXREAL_0:2;
A57: (LSeg g,j) /\ (LSeg g,(j + 1)) c= {(f /. (j + 1))} by A40, A42, A46, A54, TOPREAL1:def 8;
A58: f . (j + 1) = f /. (j + 1) by A45, A56, FINSEQ_4:24;
g . (j + 1) = (mid f,1,(Index p,f)) . (j + 1) by A4, A10, A45, A55, FINSEQ_1:85
.= f . (j + 1) by A7, A45, A55, Th32 ;
hence (LSeg g,j) /\ (LSeg g,(j + 1)) = {(g /. (j + 1))} by A49, A51, A57, A58, XBOOLE_0:def 10; :: thesis: verum
end;
end;
end;
hence (LSeg g,j) /\ (LSeg g,(j + 1)) = {(g /. (j + 1))} ; :: thesis: verum
end;
hence (LSeg g,j) /\ (LSeg g,(j + 1)) = {(g /. (j + 1))} ; :: thesis: verum
end;
A59: f is s.n.c. by A1;
A60: 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 A61: j1 + 1 < j2 ; :: thesis: LSeg g,j1 misses LSeg g,j2
A62: ( 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 A62, XXREAL_0:1;
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;
A67: 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 A68: ( 1 <= j & j + 1 <= len g ) ; :: thesis: ( (g /. j) `1 = (g /. (j + 1)) `1 or (g /. j) `2 = (g /. (j + 1)) `2 )
A69: now
j + 1 <= (Index p,f) + 1 by A4, A10, A68, FINSEQ_2:19;
then A70: j <= Index p,f by XREAL_1:8;
Index p,f < len f by A2, Th41;
then j < len f by A70, XXREAL_0:2;
hence j + 1 <= len f by NAT_1:13; :: thesis: verum
end;
A71: LSeg g,j c= LSeg f,j by A2, A4, A68, Th51;
A72: LSeg g,j = LSeg (g /. j),(g /. (j + 1)) by A68, TOPREAL1:def 5;
A73: LSeg f,j = LSeg (f /. j),(f /. (j + 1)) by A68, A69, TOPREAL1:def 5;
( (f /. j) `1 = (f /. (j + 1)) `1 or (f /. j) `2 = (f /. (j + 1)) `2 ) by A67, A68, A69, TOPREAL1:def 7;
hence ( (g /. j) `1 = (g /. (j + 1)) `1 or (g /. j) `2 = (g /. (j + 1)) `2 ) by A71, A72, A73, 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 A15, A19, A41, A60, FUNCT_1:def 8, TOPREAL1:def 7, TOPREAL1:def 8, TOPREAL1:def 9;
then g is being_S-Seq by TOPREAL1:def 10;
hence g is_S-Seq_joining f /. 1,p by A12, A14, Def3; :: thesis: verum