let D be non empty set ; :: thesis:
let CR be FinSequence of D; :: thesis:
set p = ovlpart (CR /^ 1),CR;

A1: now

assume A2: CR separates_uniquely ; :: thesis:
set f = (CR | 1) ^ (ovlcon (CR /^ 1),CR);
A3: len (ovlpart (CR /^ 1),CR) <= len (CR /^ 1) by Th16;
A4: (CR | 1) ^ (ovlcon (CR /^ 1),CR) = ((CR | 1) ^ (CR /^ 1)) ^ (CR /^ (len (ovlpart (CR /^ 1),CR))) by FINSEQ_1:45
.= CR ^ (CR /^ (len (ovlpart (CR /^ 1),CR))) by RFINSEQ:21 ;
A5: (CR | 1) ^ (ovlcon (CR /^ 1),CR) = (CR | 1) ^ (((CR /^ 1) | ((len (CR /^ 1)) -' (len (ovlpart (CR /^ 1),CR)))) ^ CR) by Th11
.= ((CR | 1) ^ ((CR /^ 1) | ((len (CR /^ 1)) -' (len (ovlpart (CR /^ 1),CR))))) ^ CR by FINSEQ_1:45 ;
A6: len ((CR | 1) ^ ((CR /^ 1) | ((len (CR /^ 1)) -' (len (ovlpart (CR /^ 1),CR))))) = (len (CR | 1)) + (len ((CR /^ 1) | ((len (CR /^ 1)) -' (len (ovlpart (CR /^ 1),CR))))) by FINSEQ_1:35
.= (len (CR | 1)) + ((len (CR /^ 1)) -' (len (ovlpart (CR /^ 1),CR))) by FINSEQ_1:80, NAT_D:35
.= (len (CR | 1)) + ((len (CR /^ 1)) - (len (ovlpart (CR /^ 1),CR))) by A3, XREAL_1:235
.= ((len (CR | 1)) + (len (CR /^ 1))) - (len (ovlpart (CR /^ 1),CR))
.= (len ((CR | 1) ^ (CR /^ 1))) - (len (ovlpart (CR /^ 1),CR)) by FINSEQ_1:35
.= (len CR) - (len (ovlpart (CR /^ 1),CR)) by RFINSEQ:21 ;
len (ovlpart (CR /^ 1),CR) <= len CR by Th16;
then A7: (len CR) - (len (ovlpart (CR /^ 1),CR)) = (len CR) -' (len (ovlpart (CR /^ 1),CR)) by XREAL_1:235;
A8: ((len CR) + 1) -' 1 = len CR by NAT_D:34;
A9: len (ovlpart (CR /^ 1),CR) <= len CR by Def2;
A10: len ((CR | 1) ^ (ovlcon (CR /^ 1),CR)) = (len (CR | 1)) + (len (ovlcon (CR /^ 1),CR)) by FINSEQ_1:35
.= (len (CR | 1)) + (((len (CR /^ 1)) + (len CR)) - (len (ovlpart (CR /^ 1),CR))) by Th15
.= ((len (CR | 1)) + (len (CR /^ 1))) + ((len CR) - (len (ovlpart (CR /^ 1),CR)))
.= (len ((CR | 1) ^ (CR /^ 1))) + ((len CR) - (len (ovlpart (CR /^ 1),CR))) by FINSEQ_1:35
.= (len CR) + ((len CR) - (len (ovlpart (CR /^ 1),CR))) by RFINSEQ:21 ;
set j = ((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR));
A11: len CR < (len CR) + 1 by XREAL_1:31;
A12: len (ovlpart (CR /^ 1),CR) <= len CR by Def2;
then A13: ((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR)) = (1 + (len CR)) - (len (ovlpart (CR /^ 1),CR)) by A11, XREAL_1:235, XXREAL_0:2
.= 1 + ((len CR) - (len (ovlpart (CR /^ 1),CR)))
.= 1 + ((len CR) -' (len (ovlpart (CR /^ 1),CR))) by A12, XREAL_1:235 ;
then A14: 1 <= ((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR)) by NAT_1:12;
A15: smid ((CR | 1) ^ (ovlcon (CR /^ 1),CR)),1,((1 + (len CR)) -' 1) = (((CR | 1) ^ (ovlcon (CR /^ 1),CR)) /^ ((0 + 1) -' 1)) | (((len CR) + 1) -' 1) by NAT_D:34
.= (((CR | 1) ^ (ovlcon (CR /^ 1),CR)) /^ 0 ) | (len CR) by A8, NAT_D:34
.= ((CR | 1) ^ (ovlcon (CR /^ 1),CR)) | (len CR) by FINSEQ_5:31
.= CR by A4, FINSEQ_5:26 ;
(((((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR))) + (len CR)) -' 1) + 1 = (((((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR))) + (len CR)) - 1) + 1 by A14, NAT_1:12, XREAL_1:235
.= (((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR))) + (len CR) ;
then A16: ((((((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR))) + (len CR)) -' 1) + 1) -' (((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR))) = ((((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR))) + (len CR)) - (((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR))) by NAT_1:12, XREAL_1:235
.= len CR ;
1 <= 1 + ((len CR) -' (len (ovlpart (CR /^ 1),CR))) by NAT_1:12;
then 1 <= 1 + ((len CR) - (len (ovlpart (CR /^ 1),CR))) by A9, XREAL_1:235;
then 1 <= (1 + (len CR)) - (len (ovlpart (CR /^ 1),CR)) ;
then 1 <= ((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR)) by A9, NAT_1:12, XREAL_1:235;
then (((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR))) -' 1 = (((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR))) - 1 by XREAL_1:235;
then (((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR))) -' 1 = (((len CR) + 1) - (len (ovlpart (CR /^ 1),CR))) - 1 by A9, NAT_1:12, XREAL_1:235
.= (((len CR) + 1) - 1) - (len (ovlpart (CR /^ 1),CR))
.= (len CR) -' (len (ovlpart (CR /^ 1),CR)) by A12, XREAL_1:235 ;
then A17: smid ((CR | 1) ^ (ovlcon (CR /^ 1),CR)),(((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR))),(((((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR))) + (len CR)) -' 1) = CR | (len CR) by A5, A6, A7, A16, FINSEQ_5:40
.= smid ((CR | 1) ^ (ovlcon (CR /^ 1),CR)),1,((1 + (len CR)) -' 1) by A15, FINSEQ_1:79 ;
len (ovlpart (CR /^ 1),CR) <= len (CR /^ 1) by Th10;
then len (ovlpart (CR /^ 1),CR) <= (len CR) -' 1 by JORDAN3:19;
then A18: ((len CR) + 1) - (len (ovlpart (CR /^ 1),CR)) >= (1 + (len CR)) - ((len CR) -' 1) by XREAL_1:12;

now

per cases ;

case len CR >= 1 ; :: thesis:

then (1 + (len CR)) - ((len CR) -' 1) = (1 + (len CR)) - ((len CR) - 1) by XREAL_1:235
.= 1 + 1 ;
then 1 < ((len CR) + 1) - (len (ovlpart (CR /^ 1),CR)) by A18, XXREAL_0:2;
then A19: 1 < ((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR)) by A11, A12, XREAL_1:235, XXREAL_0:2;
((((len CR) -' (len (ovlpart (CR /^ 1),CR))) + (len CR)) + 1) -' 1 <= (len CR) + ((len CR) -' (len (ovlpart (CR /^ 1),CR))) by NAT_D:34;
then ((1 + ((len CR) -' (len (ovlpart (CR /^ 1),CR)))) + (len CR)) -' 1 <= (len CR) + ((len CR) - (len (ovlpart (CR /^ 1),CR))) by A12, XREAL_1:235;
then A20: (((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR))) -' 1 >= len CR by A2, A10, A13, A15, A17, A19, Def6;
A21: (((len CR) + 1) -' (len (ovlpart (CR /^ 1),CR))) -' 1 = (1 + ((len CR) -' (len (ovlpart (CR /^ 1),CR)))) - 1 by A13, NAT_1:12, XREAL_1:235
.= (len CR) -' (len (ovlpart (CR /^ 1),CR)) ;
A22: (len CR) -' (len (ovlpart (CR /^ 1),CR)) <= len CR by NAT_D:35;
(len CR) -' (len (ovlpart (CR /^ 1),CR)) = (len CR) - (len (ovlpart (CR /^ 1),CR)) by A12, XREAL_1:235;
then (len CR) - (len (ovlpart (CR /^ 1),CR)) = len CR by A20, A21, A22, XXREAL_0:1;
hence len (ovlpart (CR /^ 1),CR) = 0 ; :: thesis:

end;

case len CR < 1 ; :: thesis:

then len CR < 0 + 1 ;
then A23: len CR <= 0 by NAT_1:13;
len (ovlpart (CR /^ 1),CR) <= len CR by Def2;
hence len (ovlpart (CR /^ 1),CR) = 0 by A23; :: thesis:

end;

hence len (ovlpart (CR /^ 1),CR) = 0 ; :: thesis:

end;

now

assume A24: len (ovlpart (CR /^ 1),CR) = 0 ; :: thesis:
for f being FinSequence of D
for i, j being Element of NAT st 1 <= i & i < j & (j + (len CR)) -' 1 <= len f & smid f,i,((i + (len CR)) -' 1) = smid f,j,((j + (len CR)) -' 1) & smid f,i,((i + (len CR)) -' 1) = CR holds
j -' i >= len CR

proof

let f be FinSequence of D; :: thesis:
let i, j be Element of NAT ; :: thesis:
assume A25: ( 1 <= i & i < j & (j + (len CR)) -' 1 <= len f & smid f,i,((i + (len CR)) -' 1) = smid f,j,((j + (len CR)) -' 1) & smid f,i,((i + (len CR)) -' 1) = CR ) ; :: thesis:
then A26: j - i > 0 by XREAL_1:52;
then A27: j -' i = j - i by XREAL_0:def 2;
A28: i + (j -' i) = (j - i) + i by A26, XREAL_0:def 2
.= j ;

now

per cases ;

case len CR <= 0 ; :: thesis:

hence j -' i >= len CR ; :: thesis:

end;

case A29: len CR > 0 ; :: thesis:

then A30: 0 + 1 <= len CR by NAT_1:13;
then A31: (len CR) -' 1 = (len CR) - 1 by XREAL_1:235;
A32: (i + (len CR)) -' 1 = (i + (len CR)) - 1 by A30, NAT_1:12, XREAL_1:235;
A33: i <= i + ((len CR) -' 1) by NAT_1:12;
then A34: 1 <= (i + (len CR)) -' 1 by A25, A31, A32, XXREAL_0:2;
set k = j -' i;
A35: 0 + 1 <= j -' i by A26, A27, NAT_1:13;
then A36: (j -' i) - 1 = (j -' i) -' 1 by XREAL_1:235;
A37: i + ((j -' i) -' 1) = i + ((j -' i) - 1) by A35, XREAL_1:235
.= i + ((j - i) - 1) by A26, XREAL_0:def 2
.= j - 1 ;
i + 1 <= j by A25, NAT_1:13;
then A38: (i + 1) - 1 <= j - 1 by XREAL_1:11;
then A39: j -' 1 = j - 1 by XREAL_0:def 2;
j - i > 0 by A25, XREAL_1:52;
then j -' i > 0 by XREAL_0:def 2;
then A40: j -' i >= 0 + 1 by NAT_1:13;
A41: j -' 1 <= (j -' 1) + (len CR) by NAT_1:12;
j <= j + (len CR) by NAT_1:12;
then A42: i < j + (len CR) by A25, XXREAL_0:2;
(j -' 1) + (len CR) = (j - 1) + (len CR) by A38, XREAL_0:def 2
.= (j + (len CR)) - 1
.= (j + (len CR)) -' 1 by A25, A42, XREAL_1:235, XXREAL_0:2 ;
then A43: i + ((j -' i) -' 1) <= len f by A25, A37, A39, A41, XXREAL_0:2;

now

assume A44: j -' i < len CR ; :: thesis:
then (j -' i) - 1 < (len CR) - 1 by XREAL_1:11;
then (j -' i) -' 1 < (len CR) - 1 by A40, XREAL_1:235;
then (j -' i) -' 1 < (len CR) -' 1 by A30, XREAL_1:235;
then A45: ((j -' i) -' 1) + 1 <= (len CR) -' 1 by NAT_1:13;
A46: (j -' i) - (j -' i) < (len CR) - (j -' i) by A44, XREAL_1:11;
then 0 < (len CR) -' (j -' i) by XREAL_0:def 2;
then A47: 0 + 1 <= (len CR) -' (j -' i) by NAT_1:13;
A48: (len CR) -' (j -' i) = (len CR) - (j -' i) by A46, XREAL_0:def 2;
1 < len CR by A35, A44, XXREAL_0:2;
then 1 + 1 <= len CR by NAT_1:13;
then A49: (1 + 1) - 1 <= (len CR) - 1 by XREAL_1:11;
A50: (len CR) -' 1 = (len CR) - 1 by A35, A44, XREAL_1:235, XXREAL_0:2;
then A51: (len CR) -' (j -' i) <= (len CR) -' 1 by A35, A48, XREAL_1:12;
i <= i + ((j -' i) -' 1) by NAT_1:12;
then A52: i <= len f by A43, XXREAL_0:2;
(j + (len CR)) -' 1 = (j + (len CR)) - 1 by A25, A42, XREAL_1:235, XXREAL_0:2
.= j + ((len CR) - 1)
.= j + ((len CR) -' 1) by A30, XREAL_1:235 ;
then j <= (j + (len CR)) -' 1 by NAT_1:12;
then A53: j <= len f by A25, XXREAL_0:2;
i + 1 <= j by A25, NAT_1:13;
then (i + 1) + (len CR) <= j + (len CR) by XREAL_1:9;
then A54: ((i + 1) + (len CR)) - 1 <= (j + (len CR)) - 1 by XREAL_1:11;
A55: 1 < j by A25, XXREAL_0:2;
A56: j < j + (len CR) by A29, XREAL_1:31;
then A57: 1 < j + (len CR) by A55, XXREAL_0:2;
A58: (j + (len CR)) -' 1 = (j + (len CR)) - 1 by A55, A56, XREAL_1:235, XXREAL_0:2;
then A59: ((i + 1) - 1) + (len CR) <= len f by A25, A54, XXREAL_0:2;
i + (len CR) <= (i + (len CR)) + 1 by NAT_1:12;
then (i + (len CR)) -' 1 <= i + (len CR) by A32, XREAL_1:22;
then A60: (i + (len CR)) -' 1 <= len f by A59, XXREAL_0:2;
0 < (j + (len CR)) - 1 by A57, XREAL_1:52;
then A61: 0 + 1 <= (j + (len CR)) -' 1 by A58, NAT_1:13;
j + 1 <= j + (len CR) by A56, NAT_1:13;
then A62: (j + 1) - 1 <= (j + (len CR)) - 1 by XREAL_1:11;
A63: len CR <= (len CR) + (j -' i) by NAT_1:12;
then A64: (len CR) - (j -' i) <= len CR by XREAL_1:22;
A65: (len CR) -' (j -' i) <= len CR by A48, A63, XREAL_1:22;
A66: len (smid CR,1,((len CR) -' (j -' i))) = len (mid CR,1,((len CR) -' (j -' i))) by A47, Th4;
A67: len (mid CR,1,((len CR) -' (j -' i))) = (((len CR) -' (j -' i)) -' 1) + 1 by A30, A47, A48, A64, JORDAN3:27
.= (((len CR) -' (j -' i)) - 1) + 1 by A47, XREAL_1:235
.= (len CR) -' (j -' i) ;
A68: ((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1 = (((len CR) -' 1) -' ((len CR) -' (j -' i))) + 1 by JORDAN3:19
.= (((len CR) -' 1) - ((len CR) -' (j -' i))) + 1 by A51, XREAL_1:235
.= (((len CR) - 1) - ((len CR) - (j -' i))) + 1 by A35, A44, A48, XREAL_1:235, XXREAL_0:2
.= j -' i ;
A69: len (CR /^ 1) = (len CR) -' 1 by JORDAN3:19;
then A70: smid (CR /^ 1),(((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1),(len (CR /^ 1)) = mid (CR /^ 1),(j -' i),((len CR) -' 1) by A36, A45, A68, Th4;
A71: len (mid (CR /^ 1),(j -' i),((len CR) -' 1)) = (((len CR) -' 1) -' (j -' i)) + 1 by A35, A36, A45, A49, A50, A69, JORDAN3:27
.= (((len CR) -' 1) - (j -' i)) + 1 by A36, A45, XREAL_1:235
.= (((len CR) - 1) - (j -' i)) + 1 by A35, A44, XREAL_1:235, XXREAL_0:2
.= (len CR) -' (j -' i) by A46, XREAL_0:def 2 ;
for jj being Nat st 1 <= jj & jj <= (len CR) -' (j -' i) holds
(smid CR,1,((len CR) -' (j -' i))) . jj = (smid (CR /^ 1),(((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1),(len (CR /^ 1))) . jj

proof

let jj be Nat; :: thesis:
assume A72: ( 1 <= jj & jj <= (len CR) -' (j -' i) ) ; :: thesis:
then A73: jj + (j -' i) <= ((len CR) -' (j -' i)) + (j -' i) by XREAL_1:9;
then A74: (jj + (j -' i)) - 1 <= (len CR) - 1 by A48, XREAL_1:11;
reconsider j1 = jj as Element of NAT by ORDINAL1:def 13;
A75: len (mid f,i,((i + (len CR)) -' 1)) = (((i + (len CR)) -' 1) -' i) + 1 by A25, A31, A32, A33, A34, A52, A60, JORDAN3:27
.= (((i + (len CR)) - 1) - i) + 1 by A31, A32, A33, XREAL_1:235
.= len CR ;
(len CR) -' (j -' i) <= len CR by NAT_D:35;
then A76: jj <= len CR by A72, XXREAL_0:2;
A77: 1 <= jj + ((j -' i) -' 1) by A72, NAT_1:12;
A78: jj + ((j -' i) -' 1) = jj + ((j -' i) - 1) by A35, XREAL_1:235
.= (jj + (j -' i)) - 1
.= (jj + (j -' i)) -' 1 by A72, NAT_1:12, XREAL_1:235 ;
A79: 1 <= jj + (j -' i) by A72, NAT_1:12;
(jj + (j -' i)) -' 1 <= (len CR) - 1 by A72, A74, NAT_1:12, XREAL_1:235;
then (jj + (j -' i)) -' 1 <= (len CR) -' 1 by A30, XREAL_1:235;
then (jj + (j -' i)) -' 1 in Seg (len (CR /^ 1)) by A69, A77, A78;
then A80: (jj + (j -' i)) -' 1 in dom (CR /^ 1) by FINSEQ_1:def 3;
A81: smid f,j,((j + (len CR)) -' 1) = mid f,j,((j + (len CR)) -' 1) by A58, A62, Th4;
thus (smid (CR /^ 1),(((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1),(len (CR /^ 1))) . jj = (CR /^ 1) . ((j1 + (j -' i)) -' 1) by A35, A36, A45, A49, A50, A69, A70, A71, A72, JORDAN3:27
.= (smid f,i,((i + (len CR)) -' 1)) . (((jj + (j -' i)) -' 1) + 1) by A25, A30, A80, RFINSEQ:def 2
.= (mid f,i,((i + (len CR)) -' 1)) . (((jj + (j -' i)) -' 1) + 1) by A31, A32, A33, Th4
.= (mid f,i,((i + (len CR)) -' 1)) . (((jj + (j -' i)) - 1) + 1) by A72, NAT_1:12, XREAL_1:235
.= f . ((i + (j1 + (j -' i))) -' 1) by A25, A31, A32, A33, A34, A48, A52, A60, A73, A75, A79, JORDAN3:27
.= f . (((i + (j -' i)) + j1) -' 1)
.= CR . jj by A25, A28, A53, A55, A58, A61, A62, A72, A76, A81, JORDAN3:27
.= CR . ((j1 + 1) -' 1) by NAT_D:34
.= (mid CR,1,((len CR) -' (j -' i))) . j1 by A30, A47, A48, A64, A67, A72, JORDAN3:27
.= (smid CR,1,((len CR) -' (j -' i))) . jj by A47, Th4 ; :: thesis:

end;

then smid CR,1,((len CR) -' (j -' i)) = smid (CR /^ 1),(((len (CR /^ 1)) -' ((len CR) -' (j -' i))) + 1),(len (CR /^ 1)) by A66, A67, A70, A71, FINSEQ_1:18;
then (len CR) -' (j -' i) <= len (ovlpart (CR /^ 1),CR) by A65, Def2;
hence contradiction by A24, A46, XREAL_0:def 2; :: thesis:

end;

hence j -' i >= len CR ; :: thesis:

end;

hence j -' i >= len CR ; :: thesis:

end;

hence CR separates_uniquely by Def6; :: thesis:

end;

hence ( CR separates_uniquely iff len (ovlpart (CR /^ 1),CR) = 0 ) by A1; :: thesis: