let f be non constant standard special_circular_sequence; :: thesis:
let g be FinSequence of (TOP-REAL 2); :: thesis:
let i1, i2 be Element of NAT ; :: thesis:
assume A1: ( g is_a_part>_of f,i1,i2 & i1 > i2 ) ; :: thesis:
then A2: ( len g = ((len f) + i2) -' i1 & g = (mid f,i1,((len f) -' 1)) ^ (f | i2) & g = (mid f,i1,((len f) -' 1)) ^ (mid f,1,i2) ) by Th38;
A3: ( 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & g . (len g) = f . i2 & 1 <= len g & len g < len f & ( for i being Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((i1 + i) -' 1),f) ) ) by A1, Def2;
then A4: 1 < len f by XXREAL_0:2;
then A5: (len f) -' 1 = (len f) - 1 by XREAL_1:235;
A6: i1 - 1 = i1 -' 1 by A3, XREAL_1:235;
A7: ((len f) -' 1) + 1 = len f by A5;
A8: 1 + 1 <= len f by A4, NAT_1:13;
A9: i1 < len f by A3, NAT_1:13;
A10: i2 < len f by A3, NAT_1:13;
(i1 + 1) - i1 <= (len f) - i1 by A3, XREAL_1:11;
then A11: 1 <= (len f) -' i1 by NAT_D:39;
A12: (i1 + 1) - 1 <= (len f) - 1 by A3, XREAL_1:11;
then A13: 1 <= (len f) -' 1 by A3, A5, XXREAL_0:2;
A14: (len f) -' 1 < ((len f) -' 1) + 1 by NAT_1:13;
set f1 = mid f,i1,(len f);
1 < i1 by A1, A3, XXREAL_0:2;
then A15: mid f,i1,(len f) is being_S-Seq by A9, Th52;
A16: (mid f,i1,(len f)) . (len (mid f,i1,(len f))) = f . (len f) by A3, A9, Th22;
A17: (mid f,1,i2) . 1 = f . 1 by A3, A4, A10, JORDAN3:27;
A18: f . (len f) = f /. (len f) by A4, FINSEQ_4:24;
A19: f /. 1 = f /. (len f) by FINSEQ_6:def 1;
f . 1 = f /. 1 by A4, FINSEQ_4:24;
then A20: (mid f,i1,(len f)) . (len (mid f,i1,(len f))) = (mid f,1,i2) . 1 by A16, A17, A18, FINSEQ_6:def 1;
A21: len (mid f,i1,(len f)) = ((len f) -' i1) + 1 by A3, A4, A9, JORDAN3:27;
then A22: 1 <= len (mid f,i1,(len f)) by NAT_1:11;
len (mid f,i1,(len f)) < (len (mid f,i1,(len f))) + 1 by NAT_1:13;
then A23: (len (mid f,i1,(len f))) - 1 < ((len (mid f,i1,(len f))) + 1) - 1 by XREAL_1:11;
(i1 + 1) - i1 <= (len f) - i1 by A3, XREAL_1:11;
then 1 <= (len f) -' i1 by NAT_D:39;
then A24: ( 1 <= len (mid f,i1,(len f)) & 1 <= (len (mid f,i1,(len f))) -' 1 & (len (mid f,i1,(len f))) -' 1 <= len (mid f,i1,(len f)) ) by A21, A23, NAT_1:11, NAT_D:34;
then A25: len (mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) = (((len (mid f,i1,(len f))) -' 1) -' 1) + 1 by JORDAN3:27
.= (((((len f) -' i1) + 1) -' 1) -' 1) + 1 by A3, A4, A9, JORDAN3:27 ;
A26: (((len f) -' i1) -' 1) + 1 = (((len f) -' i1) - 1) + 1 by A11, XREAL_1:235
.= (len f) - i1 by A9, XREAL_1:235 ;
A27: len (mid f,i1,((len f) -' 1)) = (((len f) -' 1) -' i1) + 1 by A3, A5, A9, A12, A13, A14, JORDAN3:27
.= (((len f) - 1) - i1) + 1 by A5, A12, XREAL_1:235
.= (len f) - i1 ;
then A28: len (mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) = len (mid f,i1,((len f) -' 1)) by A25, A26, NAT_D:34;
for k being Nat st 1 <= k & k <= len (mid f,i1,((len f) -' 1)) holds
(mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) . k = (mid f,i1,((len f) -' 1)) . k

proof

let k be Nat; :: thesis:
assume A29: ( 1 <= k & k <= len (mid f,i1,((len f) -' 1)) ) ; :: thesis:
then A30: k <= (len f) -' i1 by A9, A27, XREAL_1:235;
A31: k in NAT by ORDINAL1:def 13;
len (mid f,i1,(len f)) = ((len f) -' i1) + 1 by A3, A4, A9, JORDAN3:27;
then A32: k < len (mid f,i1,(len f)) by A30, NAT_1:13;
(mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) . k = (mid f,i1,(len f)) . ((k + 1) -' 1) by A24, A28, A29, A31, JORDAN3:27
.= (mid f,i1,(len f)) . k by NAT_D:34
.= f . ((k + i1) -' 1) by A3, A4, A9, A29, A31, A32, JORDAN3:27 ;
hence (mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) . k = (mid f,i1,((len f) -' 1)) . k by A3, A5, A9, A12, A13, A14, A29, A31, JORDAN3:27; :: thesis:

end;

then A33: mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1) = mid f,i1,((len f) -' 1) by A28, FINSEQ_1:18;
A34: L~ (f /^ (i1 -' 1)) = union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } by TOPREAL1:def 6;
A35: L~ (f | i2) = union { (LSeg (f | i2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f | i2) ) } by TOPREAL1:def 6;

now

per cases by A3, XXREAL_0:1;

case A36: i2 > 1 ; :: thesis:

(union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg (f | i2),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | i2) ) } ) = {(f . 1)}

proof

A37: len (f /^ (i1 -' 1)) = (len f) -' (i1 -' 1) by JORDAN3:19;
i1 - i1 < (len f) - i1 by A9, XREAL_1:11;
then (i1 - i1) + 1 < ((len f) - i1) + 1 by XREAL_1:8;
then 1 < (len f) - (i1 - 1) ;
then 1 < (len f) - (i1 -' 1) by A3, XREAL_1:235;
then A38: 1 < len (f /^ (i1 -' 1)) by A37, NAT_D:39;
then 1 + 1 <= len (f /^ (i1 -' 1)) by NAT_1:13;
then A39: (1 + 1) - 1 <= (len (f /^ (i1 -' 1))) - 1 by XREAL_1:11;
A40: ((len (f /^ (i1 -' 1))) -' 1) + 1 = ((len (f /^ (i1 -' 1))) - 1) + 1 by A38, XREAL_1:235
.= len (f /^ (i1 -' 1)) ;
then A41: LSeg (f /^ (i1 -' 1)),((len (f /^ (i1 -' 1))) -' 1) = LSeg ((f /^ (i1 -' 1)) /. ((len (f /^ (i1 -' 1))) -' 1)),((f /^ (i1 -' 1)) /. (((len (f /^ (i1 -' 1))) -' 1) + 1)) by A39, TOPREAL1:def 5;
A42: i1 - 1 < (len f) - 1 by A9, XREAL_1:11;
then i1 - 1 < len f by A5, A14, XXREAL_0:2;
then A43: i1 -' 1 < len f by A3, XREAL_1:235;
then A44: (f /^ (i1 -' 1)) /. (((len (f /^ (i1 -' 1))) -' 1) + 1) = f /. (len f) by A40, Th18;
i1 -' 1 <= (len f) - 1 by A3, A42, XREAL_1:235;
then A45: i1 -' 1 <= (len f) -' 1 by A4, XREAL_1:235;
A46: f /. (len f) in LSeg ((f /^ (i1 -' 1)) /. ((len (f /^ (i1 -' 1))) -' 1)),(f /. (len f)) by TOPREAL1:6;
A47: f . 1 = f /. 1 by A4, FINSEQ_4:24;
then ( f . 1 in LSeg (f /^ (i1 -' 1)),((len (f /^ (i1 -' 1))) -' 1) & LSeg (f /^ (i1 -' 1)),((len (f /^ (i1 -' 1))) -' 1) in { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) by A39, A40, A41, A44, A46, FINSEQ_6:def 1;
then A48: f . 1 in union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } by TARSKI:def 4;
A49: len (f | 2) = 2 by A8, FINSEQ_1:80;
then (len (f | 2)) -' 1 = 2 - 1 by NAT_D:39
.= 1 ;
then A50: LSeg (f | 2),((len (f | 2)) -' 1) = LSeg ((f | 2) /. ((len (f | 2)) -' 1)),((f | 2) /. (((len (f | 2)) -' 1) + 1)) by A49, TOPREAL1:def 5;
A51: (len (f | 2)) -' 1 = (1 + 1) -' 1 by A8, FINSEQ_1:80
.= 1 by NAT_D:34 ;
A52: (f | 2) /. 1 = (f | 2) . 1 by A49, FINSEQ_4:24;
A53: (f | 2) . 1 = f . 1 by FINSEQ_3:121;
A54: (f | i2) . 1 = f . 1 by A3, FINSEQ_3:121;
A55: len (f | i2) = i2 by A10, FINSEQ_1:80;
then A56: (f | 2) /. 1 = (f | i2) /. 1 by A3, A52, A53, A54, FINSEQ_4:24;
A57: 1 + 1 <= len (f | i2) by A36, A55, NAT_1:13;
A58: (f | 2) . (1 + 1) = f . (1 + 1) by FINSEQ_3:121;
A59: (f | 2) /. (1 + 1) = (f | 2) . (1 + 1) by A49, FINSEQ_4:24;
(f | i2) . (1 + 1) = f . (1 + 1) by A55, A57, FINSEQ_3:121;
then A60: (f | 2) /. (1 + 1) = (f | i2) /. (1 + 1) by A57, A58, A59, FINSEQ_4:24;
A61: LSeg (f | i2),1 = LSeg ((f | i2) /. 1),((f | i2) /. (1 + 1)) by A57, TOPREAL1:def 5;
A62: (f | 2) /. ((len (f | 2)) -' 1) = f /. 1 by A47, A51, A52, FINSEQ_3:121;
( 1 <= 1 & 1 + 1 <= len (f | i2) ) by A36, A55, NAT_1:13;
then ( f . 1 in LSeg (f | 2),((len (f | 2)) -' 1) & LSeg (f | 2),((len (f | 2)) -' 1) in { (LSeg (f | i2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f | i2) ) } ) by A47, A50, A51, A56, A60, A61, A62, TOPREAL1:6;
then f . 1 in union { (LSeg (f | i2),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | i2) ) } by TARSKI:def 4;
then f . 1 in (union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg (f | i2),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | i2) ) } ) by A48, XBOOLE_0:def 4;
then A63: {(f . 1)} c= (union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg (f | i2),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | i2) ) } ) by ZFMISC_1:37;
(union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg (f | i2),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | i2) ) } ) c= {(f . 1)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A64: x in (union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg (f | i2),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | i2) ) } ) ; :: thesis:
then x in union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } by XBOOLE_0:def 4;
then consider Y1 being set such that
A65: ( x in Y1 & Y1 in { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) by TARSKI:def 4;
consider j1 being Element of NAT such that
A66: ( Y1 = LSeg (f /^ (i1 -' 1)),j1 & 1 <= j1 & j1 + 1 <= len (f /^ (i1 -' 1)) ) by A65;
x in union { (LSeg (f | i2),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | i2) ) } by A64, XBOOLE_0:def 4;
then consider Y2 being set such that
A67: ( x in Y2 & Y2 in { (LSeg (f | i2),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f | i2) ) } ) by TARSKI:def 4;
consider j2 being Element of NAT such that
A68: ( Y2 = LSeg (f | i2),j2 & 1 <= j2 & j2 + 1 <= len (f | i2) ) by A67;
A69: LSeg (f /^ (i1 -' 1)),j1 = LSeg ((f /^ (i1 -' 1)) /. j1),((f /^ (i1 -' 1)) /. (j1 + 1)) by A66, TOPREAL1:def 5;
A70: 0 + 1 <= (i1 -' 1) + j1 by A66, XREAL_1:9;
A71: j1 + 1 <= (len f) -' (i1 -' 1) by A66, JORDAN3:19;
(j1 + 1) + (i1 -' 1) <= ((len f) -' (i1 -' 1)) + (i1 -' 1) by A37, A66, XREAL_1:8;
then A72: (j1 + 1) + (i1 -' 1) <= len f by A43, XREAL_1:237;
then A73: LSeg f,((i1 -' 1) + j1) = LSeg (f /. ((i1 -' 1) + j1)),(f /. (((i1 -' 1) + j1) + 1)) by A70, TOPREAL1:def 5;
j1 <= len (f /^ (i1 -' 1)) by A66, NAT_1:13;
then A74: (f /^ (i1 -' 1)) /. j1 = (f /^ (i1 -' 1)) . j1 by A66, FINSEQ_4:24;
(i1 -' 1) + j1 <= ((i1 -' 1) + j1) + 1 by NAT_1:11;
then A75: ( 1 <= j1 & j1 + (i1 -' 1) <= len f ) by A66, A72, XXREAL_0:2;
then (f /^ (i1 -' 1)) . j1 = f . ((i1 -' 1) + j1) by JORDAN3:23;
then A76: (f /^ (i1 -' 1)) /. j1 = f /. ((i1 -' 1) + j1) by A70, A74, A75, FINSEQ_4:24;
(j1 + 1) + (i1 -' 1) <= ((len f) -' (i1 -' 1)) + (i1 -' 1) by A71, XREAL_1:8;
then (j1 + 1) + (i1 -' 1) <= len f by A43, XREAL_1:237;
then A77: (f /^ (i1 -' 1)) . (j1 + 1) = f . (((i1 -' 1) + j1) + 1) by JORDAN3:23, NAT_1:11;
(f /^ (i1 -' 1)) /. (j1 + 1) = (f /^ (i1 -' 1)) . (j1 + 1) by A66, FINSEQ_4:24, NAT_1:11;
then A78: LSeg (f /^ (i1 -' 1)),j1 = LSeg f,((i1 -' 1) + j1) by A69, A72, A73, A76, A77, FINSEQ_4:24, NAT_1:11;
A79: len (f | i2) <= len f by FINSEQ_5:18;
then A80: j2 + 1 <= len f by A68, XXREAL_0:2;
A81: j2 < len (f | i2) by A68, NAT_1:13;
then A82: j2 < len f by A79, XXREAL_0:2;
A83: (f | i2) /. j2 = (f | i2) . j2 by A68, A81, FINSEQ_4:24
.= f . j2 by A55, A81, FINSEQ_3:121
.= f /. j2 by A68, A82, FINSEQ_4:24 ;
A84: (f | i2) /. (j2 + 1) = (f | i2) . (j2 + 1) by A68, FINSEQ_4:24, NAT_1:11
.= f . (j2 + 1) by A55, A68, FINSEQ_3:121
.= f /. (j2 + 1) by A80, FINSEQ_4:24, NAT_1:11 ;
A85: LSeg (f | i2),j2 = LSeg ((f | i2) /. j2),((f | i2) /. (j2 + 1)) by A68, TOPREAL1:def 5;
( 1 <= j2 & j2 + 1 <= len f ) by A68, A79, XXREAL_0:2;
then A86: LSeg (f | i2),j2 = LSeg f,j2 by A83, A84, A85, TOPREAL1:def 5;

A87: now

assume A88: ( not j2 = 1 or not (i1 -' 1) + j1 = (len f) -' 1 ) ; :: thesis:
len (f /^ (i1 -' 1)) = (len f) - (i1 -' 1) by A9, A37, NAT_D:44, XREAL_1:235;
then A89: (j1 + 1) + (i1 -' 1) <= ((len f) - (i1 -' 1)) + (i1 -' 1) by A66, XREAL_1:8;
then A90: ((i1 -' 1) + j1) + 1 <= len f ;
A91: (((i1 -' 1) + j1) + 1) - 1 <= (len f) - 1 by A89, XREAL_1:11;
A92: j2 + 1 < i2 + 1 by A55, A68, NAT_1:13;
A93: i2 + 1 <= i1 by A1, NAT_1:13;
(i1 -' 1) + 1 = i1 by A3, XREAL_1:237;
then A94: j2 + 1 < (i1 -' 1) + 1 by A92, A93, XXREAL_0:2;
(i1 -' 1) + 1 <= (i1 -' 1) + j1 by A66, XREAL_1:8;
then A95: ( j2 + 1 < (i1 -' 1) + j1 & (i1 -' 1) + j1 < len f ) by A90, A94, NAT_1:13, XXREAL_0:2;

now

per cases by A5, A68, A88, A91, XXREAL_0:1;

case j2 > 1 ; :: thesis:

then LSeg f,((i1 -' 1) + j1) misses LSeg f,j2 by A95, GOBOARD5:def 4;
hence (LSeg f,((i1 -' 1) + j1)) /\ (LSeg f,j2) = {} by XBOOLE_0:def 7; :: thesis:

end;

case (i1 -' 1) + j1 < (len f) -' 1 ; :: thesis:

then ((i1 -' 1) + j1) + 1 < ((len f) -' 1) + 1 by XREAL_1:8;
then LSeg f,((i1 -' 1) + j1) misses LSeg f,j2 by A5, A95, GOBOARD5:def 4;
hence (LSeg f,((i1 -' 1) + j1)) /\ (LSeg f,j2) = {} by XBOOLE_0:def 7; :: thesis:

end;

hence contradiction by A65, A66, A67, A68, A78, A86, XBOOLE_0:def 4; :: thesis:

end;

then A96: j1 = ((len f) -' 1) - (i1 -' 1)
.= ((len f) -' 1) -' (i1 -' 1) by A45, XREAL_1:235 ;
A97: (((len f) -' 1) - (i1 -' 1)) + (i1 -' 1) <= len f by A5, A14;
then A98: (((len f) -' 1) -' (i1 -' 1)) + (i1 -' 1) <= len f by A45, XREAL_1:235;
(i1 + 1) - 1 <= (len f) - 1 by A3, XREAL_1:11;
then A99: i1 - (i1 - 1) <= ((len f) - 1) - (i1 - 1) by XREAL_1:11;
then A100: 1 <= ((len f) -' 1) -' (i1 -' 1) by A5, A6, NAT_D:39;
A101: ( 1 <= ((len f) -' 1) -' (i1 -' 1) & (((len f) -' 1) -' (i1 -' 1)) + (i1 -' 1) <= len f ) by A5, A6, A97, A99, NAT_D:39;
A102: ((len f) -' 1) - (i1 -' 1) < (len f) - (i1 -' 1) by A5, A14, XREAL_1:11;
len (f /^ (i1 -' 1)) = (len f) - (i1 -' 1) by A9, A37, NAT_D:44, XREAL_1:235;
then A103: ((len f) -' 1) -' (i1 -' 1) < len (f /^ (i1 -' 1)) by A45, A102, XREAL_1:235;
then A104: (f /^ (i1 -' 1)) /. (((len f) -' 1) -' (i1 -' 1)) = (f /^ (i1 -' 1)) . (((len f) -' 1) -' (i1 -' 1)) by A100, FINSEQ_4:24
.= f . ((((len f) -' 1) -' (i1 -' 1)) + (i1 -' 1)) by A98, A100, JORDAN3:23
.= f . ((((len f) -' 1) - (i1 -' 1)) + (i1 -' 1)) by A45, XREAL_1:235
.= f /. ((len f) -' 1) by A5, A13, A14, FINSEQ_4:24 ;
A105: ((((len f) -' 1) -' (i1 -' 1)) + 1) + (i1 -' 1) = ((((len f) -' 1) - (i1 -' 1)) + 1) + (i1 -' 1) by A45, XREAL_1:235
.= ((len f) -' 1) + 1
.= ((len f) - 1) + 1 by A4, XREAL_1:235
.= len f ;
A106: 1 < (((len f) -' 1) -' (i1 -' 1)) + 1 by A100, NAT_1:13;
A107: (((len f) -' 1) -' (i1 -' 1)) + 1 <= len (f /^ (i1 -' 1)) by A103, NAT_1:13;
then A108: (f /^ (i1 -' 1)) /. ((((len f) -' 1) -' (i1 -' 1)) + 1) = (f /^ (i1 -' 1)) . ((((len f) -' 1) -' (i1 -' 1)) + 1) by A106, FINSEQ_4:24
.= f . (1 + ((((len f) -' 1) -' (i1 -' 1)) + (i1 -' 1))) by A105, A106, JORDAN3:23
.= f . (((((len f) -' 1) - (i1 -' 1)) + (i1 -' 1)) + 1) by A45, XREAL_1:235
.= f . (len f) by A4, XREAL_1:237
.= f /. (len f) by A4, FINSEQ_4:24 ;
A109: LSeg (f /^ (i1 -' 1)),j1 = LSeg ((f /^ (i1 -' 1)) /. (((len f) -' 1) -' (i1 -' 1))),((f /^ (i1 -' 1)) /. ((((len f) -' 1) -' (i1 -' 1)) + 1)) by A96, A101, A107, TOPREAL1:def 5
.= LSeg f,((len f) -' 1) by A7, A13, A104, A108, TOPREAL1:def 5 ;
LSeg (f | i2),j2 = LSeg f,1 by A57, A87, SPPOL_2:3;
then (LSeg (f /^ (i1 -' 1)),j1) /\ (LSeg (f | i2),j2) = {(f . 1)} by A109, Th54;
hence x in {(f . 1)} by A65, A66, A67, A68, XBOOLE_0:def 4; :: thesis:

end;

hence (union { (LSeg (f /^ (i1 -' 1)),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f /^ (i1 -' 1)) ) } ) /\ (union { (LSeg (f | i2),j) where j is Element of NAT : ( 1 <= j & j + 1 <= len (f | i2) ) } ) = {(f . 1)} by A63, XBOOLE_0:def 10; :: thesis:

end;

then (L~ (f /^ (i1 -' 1))) /\ (L~ (mid f,1,i2)) = {(f . 1)} by A3, A34, A35, JORDAN3:25;
then A110: (L~ (mid f,i1,(len f))) /\ (L~ (mid f,1,i2)) = {((mid f,1,i2) . 1)} by A9, A17, JORDAN3:26;
mid f,1,i2 is being_S-Seq by A3, A36, Th51;
hence (mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) ^ (mid f,1,i2) is being_S-Seq by A15, A20, A110, JORDAN3:80; :: thesis:

end;

case i2 = 1 ; :: thesis:

then A111: mid f,1,i2 = f | 1 by JORDAN3:25
.= <*(f /. 1)*> by FINSEQ_5:23 ;
A112: <*(f /. 1)*> = <*((mid f,i1,(len f)) /. (len (mid f,i1,(len f))))*> by A16, A18, A19, A22, FINSEQ_4:24;
A113: mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1) = (mid f,i1,(len f)) | ((len (mid f,i1,(len f))) -' 1) by A24, JORDAN3:25;
((len (mid f,i1,(len f))) -' 1) + 1 = len (mid f,i1,(len f)) by A21, NAT_D:34;
hence (mid (mid f,i1,(len f)),1,((len (mid f,i1,(len f))) -' 1)) ^ (mid f,1,i2) is being_S-Seq by A15, A111, A112, A113, FINSEQ_5:24; :: thesis:

end;

then A114: g is being_S-Seq by A1, A33, Th38;
A115: i1 < len f by A3, NAT_1:13;
len (mid f,i1,((len f) -' 1)) = (((len f) -' 1) -' i1) + 1 by A3, A5, A9, A12, A13, A14, JORDAN3:27;
then 1 <= len (mid f,i1,((len f) -' 1)) by NAT_1:11;
then 1 in Seg (len (mid f,i1,((len f) -' 1))) by FINSEQ_1:3;
then 1 in dom (mid f,i1,((len f) -' 1)) by FINSEQ_1:def 3;
then g . 1 = (mid f,i1,((len f) -' 1)) . 1 by A2, FINSEQ_1:def 7;
then A116: g . 1 = f . i1 by A3, A5, A9, A13, A14, JORDAN3:27;
A117: g /. (len g) = g . (len g) by A3, FINSEQ_4:24;
f /. i1 = f . i1 by A3, A115, FINSEQ_4:24;
then ( f /. i1 = g /. 1 & f /. i2 = g /. (len g) ) by A3, A10, A116, A117, FINSEQ_4:24;
hence L~ g is_S-P_arc_joining f /. i1,f /. i2 by A114, TOPREAL4:def 1; :: thesis: