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 that
A1: g is_a_part>_of f,i1,i2 and
A2: i1 > i2 ; :: thesis:
A3: 1 <= len g by A1, Def2;
g . (len g) = f . i2 by A1, Def2;
then A4: f . i2 = f . (S_Drop ((i1 + (len g)) -' 1),f) by A1, A3, Def2;
A5: i2 <= i2 + 1 by NAT_1:11;
A6: i1 <= i1 + 1 by NAT_1:12;
A7: 1 <= i1 by A1, Def2;
A8: i1 + 1 <= len f by A1, Def2;
then A9: (i1 + 1) - 1 <= (len f) - 1 by XREAL_1:11;
then A10: 1 <= (len f) - 1 by A7, XXREAL_0:2;
then A11: (len f) - 1 = (len f) -' 1 by NAT_D:39;

A12: now

per cases ) -' 1) mod ((len f) -' 1) <> 0 or ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 ) ;

case A13: ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 ; :: thesis:

A14: i1 <= (len f) -' 1 by A8, NAT_D:49;
then A15: ((i1 + (len g)) -' 1) mod ((len f) -' 1) < (len f) -' 1 by A7, NAT_D:1;
1 <= (len f) -' 1 by A7, A14, XXREAL_0:2;
then A16: (len f) -' 1 < len f by NAT_D:51;
S_Drop ((i1 + (len g)) -' 1),f = ((i1 + (len g)) -' 1) mod ((len f) -' 1) by A13, Def1;
hence S_Drop ((i1 + (len g)) -' 1),f < len f by A15, A16, XXREAL_0:2; :: thesis:

end;

case A17: ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 ; :: thesis:

i1 <= (len f) -' 1 by A8, NAT_D:49;
then A18: 1 <= (len f) -' 1 by A7, XXREAL_0:2;
S_Drop ((i1 + (len g)) -' 1),f = (len f) -' 1 by A17, Def1;
hence S_Drop ((i1 + (len g)) -' 1),f < len f by A18, NAT_D:51; :: thesis:

end;

i1 <= (len f) -' 1 by A8, NAT_D:49;
then 1 <= (len f) -' 1 by A7, XXREAL_0:2;
then A19: (len f) -' 1 < len f by NAT_D:51;

A20: now

per cases ) -' 1) mod ((len f) -' 1) <> 0 or ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 ) ;

case ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 ; :: thesis:

then 0 + 1 <= ((i1 + (len g)) -' 1) mod ((len f) -' 1) by NAT_1:13;
hence 1 <= S_Drop ((i1 + (len g)) -' 1),f by Def1; :: thesis:

end;

case A21: ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 ; :: thesis:

A22: i1 <= (len f) -' 1 by A8, NAT_D:49;
S_Drop ((i1 + (len g)) -' 1),f = (len f) -' 1 by A21, Def1;
hence 1 <= S_Drop ((i1 + (len g)) -' 1),f by A7, A22, XXREAL_0:2; :: thesis:

end;

A23: 1 <= i2 by A1, Def2;
A24: i2 + 1 <= len f by A1, Def2;
then A25: i2 <= (len f) -' 1 by NAT_D:49;
then A26: 1 <= (len f) -' 1 by A23, XXREAL_0:2;
then (len f) -' 1 < len f by NAT_D:51;
then A27: i2 < len f by A25, XXREAL_0:2;
A28: len g < len f by A1, Def2;
A29: 0 <> (len f) -' 1 by A10, NAT_D:39;

now

per cases by XXREAL_0:1;

case A30: i2 < S_Drop ((i1 + (len g)) -' 1),f ; :: thesis:

i2 <= len f by A24, NAT_D:46;
then A31: f /. i2 = f . i2 by A23, FINSEQ_4:24;
A32: 1 <= S_Drop ((i1 + (len g)) -' 1),f by A23, A30, XXREAL_0:2;
f /. i2 <> f /. (S_Drop ((i1 + (len g)) -' 1),f) by A23, A12, A30, GOBOARD7:38;
hence contradiction by A4, A12, A31, A32, FINSEQ_4:24; :: thesis:

end;

case A33: i2 > S_Drop ((i1 + (len g)) -' 1),f ; :: thesis:

i2 <= len f by A24, NAT_D:46;
then A34: f /. i2 = f . i2 by A23, FINSEQ_4:24;
f /. i2 <> f /. (S_Drop ((i1 + (len g)) -' 1),f) by A20, A27, A33, GOBOARD7:38;
hence contradiction by A4, A20, A12, A34, FINSEQ_4:24; :: thesis:

end;

case A35: i2 = S_Drop ((i1 + (len g)) -' 1),f ; :: thesis:

now

per cases ) -' 1) mod ((len f) -' 1) <> 0 or ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 ) ;

case A36: ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 ; :: thesis:

( ex n being Nat st
( (i1 + (len g)) -' 1 = (((len f) -' 1) * n) + (((i1 + (len g)) -' 1) mod ((len f) -' 1)) & ((i1 + (len g)) -' 1) mod ((len f) -' 1) < (len f) -' 1 ) or ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 & (len f) -' 1 = 0 ) ) by NAT_D:def 2;
then consider n being Nat such that
A37: (i1 + (len g)) -' 1 = (((len f) -' 1) * n) + (((i1 + (len g)) -' 1) mod ((len f) -' 1)) by A10, NAT_D:39;
A38: (i1 + (len g)) -' 1 = (((len f) -' 1) * n) + i2 by A35, A36, A37, Def1;

now

per cases ;

case n = 0 ; :: thesis:

then i2 = (i1 + (len g)) -' 1 by A35, A36, A37, Def1;
then i2 + 1 = ((i1 + (len g)) - 1) + 1 by A23, NAT_D:39
.= i1 + (len g) ;
hence contradiction by A2, A3, XREAL_1:10; :: thesis:

end;

case n <> 0 ; :: thesis:

then A39: 0 + 1 <= n by NAT_1:13;

now

per cases by A39, XXREAL_0:1;

case A40: 1 = n ; :: thesis:

(len f) -' 1 = (len f) - 1 by A26, NAT_D:39;
then A41: (i1 + (len g)) - 1 = ((len f) - 1) + i2 by A7, A38, A40, NAT_D:37;
then A42: len g = ((len f) + i2) - i1 ;
A43: (len f) -' 1 <= len f by NAT_D:50;
A44: dom g = Seg (len g) by FINSEQ_1:def 3;
A45: i1 <= len f by A8, A6, XXREAL_0:2;
A46: 1 <= (len f) -' 1 by A10, NAT_D:39;
A47: i1 <= (len f) -' 1 by A9, A10, NAT_D:39;
then A48: len (mid f,i1,((len f) -' 1)) = (((len f) -' 1) -' i1) + 1 by A7, A45, A46, A43, FINSEQ_6:124;
A49: (((len f) -' 1) -' i1) + 1 = (((len f) - 1) - i1) + 1 by A9, A11, XREAL_1:235
.= (len f) - i1 ;
len ((mid f,i1,((len f) -' 1)) ^ (f | i2)) = (len (mid f,i1,((len f) -' 1))) + (len (f | i2)) by FINSEQ_1:35;
then len ((mid f,i1,((len f) -' 1)) ^ (f | i2)) = ((len f) - i1) + i2 by A24, A5, A48, A49, FINSEQ_1:80, XXREAL_0:2
.= ((len f) + i2) - i1
.= ((len f) + i2) -' i1 by A8, A6, NAT_D:37, XXREAL_0:2 ;
then A50: len ((mid f,i1,((len f) -' 1)) ^ (f | i2)) = len g by A8, A6, A42, NAT_D:37, XXREAL_0:2;
A51: ((len f) -' 1) -' i1 = ((len f) -' 1) - i1 by A9, A11, XREAL_1:235;
for j being Nat st j in dom g holds
g . j = ((mid f,i1,((len f) -' 1)) ^ (f | i2)) . j

proof

let j be Nat; :: thesis:
assume A52: j in dom g ; :: thesis:
then A53: 1 <= j by A44, FINSEQ_1:3;
then A54: (i1 + j) -' 1 = (i1 + j) - 1 by NAT_D:37;
i1 + j >= 1 + 1 by A7, A53, XREAL_1:9;
then A55: (i1 + j) -' 1 <> 0 by A54;
A56: j <= len g by A44, A52, FINSEQ_1:3;
then A57: g . j = f . (S_Drop ((i1 + j) -' 1),f) by A1, A53, Def2;
A58: j in NAT by ORDINAL1:def 13;

now

per cases ;

case A59: j <= len (mid f,i1,((len f) -' 1)) ; :: thesis:

then A60: j + i1 <= ((((len f) -' 1) - i1) + 1) + i1 by A48, A51, XREAL_1:8;

A61: now

per cases ;

case A62: i1 + j = len f ; :: thesis:

then ((i1 + j) -' 1) mod ((len f) -' 1) = 0 by NAT_D:25;
hence S_Drop ((i1 + j) -' 1),f = (i1 + j) -' 1 by A62, Def1; :: thesis:

end;

case i1 + j <> len f ; :: thesis:

then i1 + j < len f by A11, A60, XXREAL_0:1;
then (i1 + j) - 1 < (len f) - 1 by XREAL_1:11;
then A63: (i1 + j) -' 1 < (len f) -' 1 by A7, A11, NAT_D:37;
then ((i1 + j) -' 1) mod ((len f) -' 1) <> 0 by A55, NAT_D:24;
then S_Drop ((i1 + j) -' 1),f = ((i1 + j) -' 1) mod ((len f) -' 1) by Def1;
hence S_Drop ((i1 + j) -' 1),f = (i1 + j) -' 1 by A63, NAT_D:24; :: thesis:

end;

A64: (len f) -' 1 <= len f by NAT_D:50;
j in dom (mid f,i1,((len f) -' 1)) by A53, A59, FINSEQ_3:27;
then A65: ((mid f,i1,((len f) -' 1)) ^ (f | i2)) . j = (mid f,i1,((len f) -' 1)) . j by FINSEQ_1:def 7;
A66: 1 <= j by A44, A52, FINSEQ_1:3;
i1 <= (len f) -' 1 by A9, A10, NAT_D:39;
hence g . j = ((mid f,i1,((len f) -' 1)) ^ (f | i2)) . j by A7, A45, A46, A57, A58, A59, A65, A64, A66, A61, FINSEQ_6:124; :: thesis:

end;

case A67: j > len (mid f,i1,((len f) -' 1)) ; :: thesis:

j <= ((len f) + i2) - i1 by A41, A44, A52, FINSEQ_1:3;
then j + i1 <= (((len f) + i2) - i1) + i1 by XREAL_1:8;
then A68: (j + i1) - (len f) <= ((len f) + i2) - (len f) by XREAL_1:11;
j < len f by A28, A56, XXREAL_0:2;
then A69: j <= (len f) - 1 by SPPOL_1:6;
(i1 + 1) - 1 <= (len f) - 1 by A8, XREAL_1:11;
then A70: i1 + j <= ((len f) -' 1) + ((len f) -' 1) by A11, A69, XREAL_1:9;
A71: ((mid f,i1,((len f) -' 1)) ^ (f | i2)) . j = (f | i2) . (j - (len (mid f,i1,((len f) -' 1)))) by A50, A56, A67, FINSEQ_6:114;
A72: (i1 + j) - 1 = (i1 + j) -' 1 by A7, NAT_D:37;
(len (mid f,i1,((len f) -' 1))) + 1 <= j by A67, NAT_1:13;
then ((len (mid f,i1,((len f) -' 1))) + 1) - (len (mid f,i1,((len f) -' 1))) <= j - (len (mid f,i1,((len f) -' 1))) by XREAL_1:11;
then 1 + (len f) <= ((i1 + j) - (len f)) + (len f) by A48, A49, XREAL_1:8;
then (1 + (len f)) - 1 <= (i1 + j) - 1 by XREAL_1:11;
then A73: (len f) -' 1 < (i1 + j) -' 1 by A19, A72, XXREAL_0:2;
j + i1 > ((len f) - i1) + i1 by A48, A49, A67, XREAL_1:8;
then A74: (i1 + j) - (len f) > (len f) - (len f) by XREAL_1:11;
then A75: (i1 + j) -' (len f) = (i1 + j) - (len f) by XREAL_0:def 2;
j - (len (mid f,i1,((len f) -' 1))) = j - ((len f) - i1) by A7, A45, A46, A43, A47, A49, FINSEQ_6:124
.= (j + i1) - (len f) ;
then A76: (f | i2) . (j - (len (mid f,i1,((len f) -' 1)))) = f . ((i1 + j) -' (len f)) by A75, A68, FINSEQ_3:121;
i1 + j < (i1 + j) + 1 by NAT_1:13;
then (i1 + j) - 1 < ((i1 + j) + 1) - 1 by XREAL_1:11;
then A77: (i1 + j) -' 1 < ((len f) -' 1) + ((len f) -' 1) by A72, A70, XXREAL_0:2;

now

per cases ) -' 1) mod ((len f) -' 1) = 0 or ((i1 + j) -' 1) mod ((len f) -' 1) <> 0 ) ;

case ((i1 + j) -' 1) mod ((len f) -' 1) = 0 ; :: thesis:

hence contradiction by A73, A77, Th6; :: thesis:

end;

case A78: ((i1 + j) -' 1) mod ((len f) -' 1) <> 0 ; :: thesis:

((i1 + j) -' (len f)) + ((len f) -' 1) = ((i1 + j) -' (len f)) + ((len f) - 1) by A10, NAT_D:39
.= ((i1 + j) - (len f)) + ((len f) - 1) by A74, XREAL_0:def 2
.= (i1 + j) - 1
.= (i1 + j) -' 1 by A53, NAT_D:37 ;
then A79: ((i1 + j) -' 1) mod ((len f) -' 1) = (((i1 + j) -' (len f)) + (((len f) -' 1) mod ((len f) -' 1))) mod ((len f) -' 1) by NAT_D:23
.= (((i1 + j) -' (len f)) + 0 ) mod ((len f) -' 1) by NAT_D:25
.= ((i1 + j) -' (len f)) mod ((len f) -' 1) ;
(i1 + j) - ((len f) -' 1) <= (((len f) -' 1) + ((len f) -' 1)) - ((len f) -' 1) by A70, XREAL_1:11;
then (i1 + j) - ((len f) - 1) <= (len f) -' 1 by A10, NAT_D:39;
then ((i1 + j) -' (len f)) + 1 <= (len f) -' 1 by A75;
then A80: (i1 + j) -' (len f) < (len f) -' 1 by NAT_1:13;
S_Drop ((i1 + j) -' 1),f = ((i1 + j) -' 1) mod ((len f) -' 1) by A78, Def1;
hence g . j = ((mid f,i1,((len f) -' 1)) ^ (f | i2)) . j by A57, A71, A76, A79, A80, NAT_D:24; :: thesis:

end;

hence g . j = ((mid f,i1,((len f) -' 1)) ^ (f | i2)) . j ; :: thesis:

end;

hence g . j = ((mid f,i1,((len f) -' 1)) ^ (f | i2)) . j ; :: thesis:

end;

hence ( len g = ((len f) + i2) -' i1 & g = (mid f,i1,((len f) -' 1)) ^ (f | i2) ) by A8, A6, A42, A50, FINSEQ_2:10, NAT_D:37, XXREAL_0:2; :: thesis:

end;

case 1 < n ; :: thesis:

then 1 + 1 <= n by NAT_1:13;
then ((len f) -' 1) * n >= ((len f) -' 1) * (1 + 1) by XREAL_1:66;
then A81: (i1 + (len g)) -' 1 >= (((len f) -' 1) * (1 + 1)) + i2 by A38, XREAL_1:8;
A82: ((len f) -' 1) * (1 + 1) <= (((len f) -' 1) * (1 + 1)) + i2 by NAT_1:11;
A83: (i1 + 1) - 1 <= (len f) - 1 by A8, XREAL_1:11;
(len g) - 1 < (len f) -' 1 by A28, A11, XREAL_1:11;
then A84: i1 + ((len g) - 1) < ((len f) -' 1) + ((len f) -' 1) by A11, A83, XREAL_1:10;
(i1 + (len g)) - 1 = (i1 + (len g)) -' 1 by A7, NAT_D:37;
hence contradiction by A81, A84, A82, XXREAL_0:2; :: thesis:

end;

hence ( len g = ((len f) + i2) -' i1 & g = (mid f,i1,((len f) -' 1)) ^ (f | i2) ) ; :: thesis:

end;

hence ( len g = ((len f) + i2) -' i1 & g = (mid f,i1,((len f) -' 1)) ^ (f | i2) ) ; :: thesis:

end;

case A85: ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 ; :: thesis:

ex n being Nat st
( (i1 + (len g)) -' 1 = (((len f) -' 1) * n) + (((i1 + (len g)) -' 1) mod ((len f) -' 1)) & ((i1 + (len g)) -' 1) mod ((len f) -' 1) < (len f) -' 1 ) by A29, NAT_D:def 2;
then consider n being Nat such that
A86: (i1 + (len g)) -' 1 = (((len f) -' 1) * n) + (((i1 + (len g)) -' 1) mod ((len f) -' 1)) ;

A87: now

assume n > 1 ; :: thesis:
then n >= 1 + 1 by NAT_1:13;
then A88: (i1 + (len g)) -' 1 >= ((len f) -' 1) * (1 + 1) by A85, A86, NAT_1:4;
(len g) - 1 < (len f) - 1 by A28, XREAL_1:11;
then i1 + ((len g) - 1) < ((len f) -' 1) + ((len f) -' 1) by A9, A11, XREAL_1:10;
then (i1 + (len g)) - 1 < ((len f) -' 1) + ((len f) -' 1) ;
hence contradiction by A7, A88, NAT_1:12, XREAL_1:235; :: thesis:

end;

now

assume n = 0 ; :: thesis:
then A89: i1 + (len g) <= 1 by A85, A86, NAT_D:36;
i1 + (len g) >= 1 + 1 by A7, A3, XREAL_1:9;
hence contradiction by A89, XXREAL_0:2; :: thesis:

end;

then n >= 0 + 1 by NAT_1:13;
then n = 1 by A87, XXREAL_0:1;
then (i1 + (len g)) -' 1 = i2 by A35, A85, A86, Def1;
then A90: (i1 + (len g)) - 1 = i2 by A23, NAT_D:39;
i2 - i2 < i1 - i2 by A2, XREAL_1:11;
then A91: - 0 > - (i1 - i2) by XREAL_1:26;
1 - 1 <= (len g) - 1 by A3, XREAL_1:11;
hence contradiction by A90, A91; :: thesis:

end;

hence ( len g = ((len f) + i2) -' i1 & g = (mid f,i1,((len f) -' 1)) ^ (f | i2) ) ; :: thesis:

end;

hence ( 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 A23, FINSEQ_6:122; :: thesis: