let f be non constant standard special_circular_sequence; :: thesis: for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part<_of f,i1,i2 & i1 < i2 holds
( len g = ((len f) + i1) -' i2 & g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) )
let g be FinSequence of (TOP-REAL 2); :: thesis: for i1, i2 being Element of NAT st g is_a_part<_of f,i1,i2 & i1 < i2 holds
( len g = ((len f) + i1) -' i2 & g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) )
let i1, i2 be Element of NAT ; :: thesis: ( g is_a_part<_of f,i1,i2 & i1 < i2 implies ( len g = ((len f) + i1) -' i2 & g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) ) )
assume A1: ( g is_a_part<_of f,i1,i2 & i1 < i2 ) ; :: thesis: ( len g = ((len f) + i1) -' i2 & g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) )
then A2: ( 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 (((len f) + i1) -' i),f) ) ) by Def3;
i1 <= i1 + 1 by NAT_1:12;
then A3: i1 <= len f by A2, XXREAL_0:2;
A4: (i1 + 1) - 1 <= (len f) - 1 by A2, XREAL_1:11;
then A5: 1 <= (len f) - 1 by A2, XXREAL_0:2;
then A6: (len f) - 1 = (len f) -' 1 by NAT_D:39;
A7: 0 <> (len f) -' 1 by A5, NAT_D:39;
A8: (i2 + 1) - 1 <= (len f) - 1 by A2, XREAL_1:11;
i1 <= (len f) -' 1 by A2, NAT_D:49;
then 1 <= (len f) -' 1 by A2, XXREAL_0:2;
then A9: (len f) -' 1 < len f by NAT_D:51;
i1 <= i1 + 1 by NAT_1:11;
then A10: i1 <= len f by A2, XXREAL_0:2;
i2 <= i2 + 1 by NAT_1:11;
then A11: i2 <= len f by A2, XXREAL_0:2;
A12: f . i2 = f . (S_Drop (((len f) + i1) -' (len g)),f) by A2;

A13: now

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

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

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

end;

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

then A14: S_Drop (((len f) + i1) -' (len g)),f = (len f) -' 1 by Def1;
i1 <= (len f) -' 1 by A2, NAT_D:49;
hence 1 <= S_Drop (((len f) + i1) -' (len g)),f by A2, A14, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A15: now

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

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

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

end;

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

then A20: S_Drop (((len f) + i1) -' (len g)),f = (len f) -' 1 by Def1;
i1 <= (len f) -' 1 by A2, NAT_D:49;
then 1 <= (len f) -' 1 by A2, XXREAL_0:2;
hence S_Drop (((len f) + i1) -' (len g)),f < len f by A20, NAT_D:51; :: thesis: verum

end;

end;

end;

A21: i2 <= (len f) -' 1 by A2, NAT_D:49;
then 1 <= (len f) -' 1 by A2, XXREAL_0:2;
then (len f) -' 1 < len f by NAT_D:51;
then A22: i2 < len f by A21, XXREAL_0:2;

now

per cases ( i2 < S_Drop (((len f) + i1) -' (len g)),f or i2 > S_Drop (((len f) + i1) -' (len g)),f or i2 = S_Drop (((len f) + i1) -' (len g)),f ) by XXREAL_0:1;

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

then A24: f /. i2 <> f /. (S_Drop (((len f) + i1) -' (len g)),f) by A2, A15, GOBOARD7:38;
i2 <= len f by A2, NAT_1:13;
then A25: f /. i2 = f . i2 by A2, FINSEQ_4:24;
1 <= S_Drop (((len f) + i1) -' (len g)),f by A2, A23, XXREAL_0:2;
hence contradiction by A12, A15, A24, A25, FINSEQ_4:24; :: thesis: verum

end;

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

then A26: f /. i2 <> f /. (S_Drop (((len f) + i1) -' (len g)),f) by A13, A22, GOBOARD7:38;
i2 <= len f by A2, NAT_1:13;
then f /. i2 = f . i2 by A2, FINSEQ_4:24;
hence contradiction by A12, A13, A15, A26, FINSEQ_4:24; :: thesis: verum

end;

case A27: i2 = S_Drop (((len f) + i1) -' (len g)),f ; :: thesis: ( len g = ((len f) + i1) -' i2 & g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) )

now

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

case A28: (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 ; :: thesis: ( len g = ((len f) + i1) -' i2 & g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) )

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

now

per cases ( n = 0 or n <> 0 ) ;

case n = 0 ; :: thesis: ( len g = ((len f) + i1) -' i2 & g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) )

then A31: i2 = ((len f) + i1) -' (len g) by A27, A28, A29, Def1
.= ((len f) + i1) - (len g) by A2, NAT_D:37
.= ((len f) - (len g)) + i1 ;
then A32: len g = ((len f) + i1) - i2 ;
A33: len ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) = (len (mid f,i1,1)) + (len (mid f,((len f) -' 1),i2)) by FINSEQ_1:35;
A34: len (mid f,i1,1) = (i1 -' 1) + 1 by A2, A3, Th21
.= i1 by A2, XREAL_1:237 ;
len (mid f,((len f) -' 1),i2) = (((len f) -' 1) -' i2) + 1 by A2, A6, A8, A9, Th21;
then len (mid f,((len f) -' 1),i2) = (((len f) -' 1) - i2) + 1 by A6, A8, XREAL_1:235;
then len ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) = (i1 + (len f)) - i2 by A6, A33, A34
.= ((len f) + i1) -' i2 by A11, NAT_D:37 ;
then A35: ( len g = len g & len ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) = len g ) by A11, A32, NAT_D:37;
X: dom g = Seg (len g) by FINSEQ_1:def 3;
for j being Nat st j in dom g holds
g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j

proof

let j be Nat; :: thesis: ( j in dom g implies g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j )
assume A36: j in dom g ; :: thesis: g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j
then A37: ( 1 <= j & j <= len g ) by X, FINSEQ_1:3;
then A38: g . j = f . (S_Drop (((len f) + i1) -' j),f) by A1, Def3;
A39: j in NAT by ORDINAL1:def 13;
A40: j < len f by A2, A37, XXREAL_0:2;
then A41: ((len f) + i1) -' j = ((len f) + i1) - j by NAT_D:37;

now

per cases ( j <= len (mid f,i1,1) or j > len (mid f,i1,1) ) ;

case A42: j <= len (mid f,i1,1) ; :: thesis: g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j

then j in dom (mid f,i1,1) by A37, FINSEQ_3:27;
then A43: ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j = (mid f,i1,1) . j by FINSEQ_1:def 7;
A44: len (mid f,i1,1) = (i1 -' 1) + 1 by A2, A10, Th21;
( 1 <= i1 & i1 <= (len f) -' 1 & (len f) -' 1 <= len f & 1 <= j & j <= i1 ) by A1, A4, A5, A34, A36, A42, Def3, X, FINSEQ_1:3, NAT_D:39, NAT_D:50;
then ((len f) - 1) + j <= (len f) + i1 by A6, XREAL_1:9;
then A45: (((len f) - 1) + j) - j <= ((len f) + i1) - j by XREAL_1:11;

now

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

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

then ((len f) + i1) - j = (len f) - 1 by A6, A34, A42, NAT_D:37;
then i1 + 1 = j ;
hence g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j by A34, A42, NAT_1:13; :: thesis: verum

end;

case ((len f) + i1) -' j <> (len f) -' 1 ; :: thesis: g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j

then A46: ((len f) + i1) -' j > (len f) -' 1 by A6, A41, A45, XXREAL_0:1;
A47: j - 1 >= 0 by A37, XREAL_1:50;
then j - 1 = j -' 1 by XREAL_0:def 2;
then A48: len f <= (len f) + (j - 1) by NAT_1:11;

now

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

case A49: ( i1 + 1 = len f & j - 1 = 0 ) ; :: thesis: g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j

then ((len f) + i1) -' j = (((len f) - 1) + (len f)) - 1 by A2, NAT_D:37
.= ((len f) -' 1) + ((len f) -' 1) by A6 ;
then (((len f) + i1) -' j) mod ((len f) -' 1) = 0 by Th8;
then S_Drop (((len f) + i1) -' j),f = (j + i1) -' 1 by A49, Def1;
then A50: S_Drop (((len f) + i1) -' j),f = (1 + i1) - 1 by A49, NAT_D:37
.= (i1 - j) + 1 by A49 ;
A51: (i1 - j) + 1 = (i1 -' j) + 1 by A34, A42, XREAL_1:235;
A52: 1 <= (i1 -' j) + 1 by NAT_1:11;
A53: j - 1 = j -' 1 by A37, XREAL_1:235;
i1 <= i1 + (j -' 1) by NAT_1:11;
then A54: i1 - (j -' 1) <= i1 by XREAL_1:22;
(mid f,i1,1) . j = (mid f,1,i1) . ((((i1 - 1) + 1) - j) + 1) by A2, A10, A37, A39, A42, A44, Th25
.= f . ((i1 -' j) + 1) by A10, A51, A52, A53, A54, JORDAN3:32 ;
hence g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j by A34, A38, A42, A43, A50, XREAL_1:235; :: thesis: verum

end;

case A55: ( i1 + 1 <> len f or j - 1 <> 0 ) ; :: thesis: g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j

now

per cases ( i1 + 1 <> len f or j - 1 <> 0 ) by A55;

case i1 + 1 <> len f ; :: thesis: i1 + 1 < (len f) + (j - 1)

then i1 + 1 < len f by A2, XXREAL_0:1;
hence i1 + 1 < (len f) + (j - 1) by A48, XXREAL_0:2; :: thesis: verum

end;

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

then len f < (len f) + (j - 1) by A47, XREAL_1:31;
hence i1 + 1 < (len f) + (j - 1) by A2, XXREAL_0:2; :: thesis: verum

end;

end;

end;

then (i1 + 1) - j < (((len f) - 1) + j) - j by XREAL_1:11;
then A56: ((len f) - 1) + ((i1 + 1) - j) < ((len f) - 1) + ((len f) - 1) by XREAL_1:10;
then (((len f) + i1) -' j) mod ((len f) -' 1) <> 0 by A2, A4, A6, A41, A46, Th6;
then A57: S_Drop (((len f) + i1) -' j),f = (((len f) + i1) -' j) mod ((len f) -' 1) by Def1
.= (((len f) + i1) - j) - ((len f) - 1) by A2, A4, A6, A41, A45, A56, Th7
.= (i1 - j) + 1 ;
A58: (i1 - j) + 1 = (i1 -' j) + 1 by A34, A42, XREAL_1:235;
A59: 1 <= (i1 -' j) + 1 by NAT_1:11;
A60: j - 1 = j -' 1 by A37, XREAL_1:235;
i1 <= i1 + (j -' 1) by NAT_1:11;
then A61: i1 - (j -' 1) <= i1 by XREAL_1:22;
(mid f,i1,1) . j = (mid f,1,i1) . ((((i1 - 1) + 1) - j) + 1) by A2, A10, A37, A39, A42, A44, Th25
.= f . ((i1 -' j) + 1) by A10, A58, A59, A60, A61, JORDAN3:32 ;
hence g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j by A34, A38, A42, A43, A57, XREAL_1:235; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

case A62: j > len (mid f,i1,1) ; :: thesis: g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j

then A63: i1 + 1 <= j by A34, NAT_1:13;
A64: ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j = (mid f,((len f) -' 1),i2) . (j - (len (mid f,i1,1))) by A35, A37, A62, JORDAN3:15;
A65: j <= ((len f) + i1) - i2 by A31, A36, X, FINSEQ_1:3;
i2 - i1 >= 0 by A1, XREAL_1:50;
then (len f) + 0 <= (len f) + (i2 - i1) by XREAL_1:9;
then A66: (len f) - (i2 - i1) <= ((len f) + (i2 - i1)) - (i2 - i1) by XREAL_1:11;
then A67: j <= len f by A65, XXREAL_0:2;
i1 + 1 <= j by A34, A62, NAT_1:13;
then A68: (i1 + 1) - i1 <= j - i1 by XREAL_1:11;
(i2 + 1) - 1 <= (len f) - 1 by A2, XREAL_1:11;
then A69: i2 - i2 <= ((len f) - 1) - i2 by XREAL_1:11;
A70: j - i1 <= (((len f) + i1) - i2) - i1 by A31, A37, XREAL_1:11;
(len f) - i2 <= (len f) - 1 by A2, XREAL_1:15;
then j - i1 <= (len f) -' 1 by A6, A70, XXREAL_0:2;
then A71: j -' i1 <= (len f) -' 1 by A34, A62, XREAL_1:235;
A72: (len f) - i2 = (((len f) - 1) - i2) + 1
.= (((len f) -' 1) -' i2) + 1 by A6, A69, XREAL_0:def 2 ;
A73: j - i1 = j -' (len (mid f,i1,1)) by A34, A68, XREAL_0:def 2;
(((len f) -' 1) -' (j -' i1)) + 1 = (((len f) -' 1) - (j -' i1)) + 1 by A71, XREAL_1:235
.= (((len f) - 1) - (j - i1)) + 1 by A6, A34, A62, XREAL_1:235
.= ((len f) + i1) - j
.= ((len f) + i1) -' j by A65, A66, NAT_D:37, XXREAL_0:2 ;
then A74: ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j = f . (((len f) + i1) -' j) by A2, A6, A8, A9, A34, A64, A68, A70, A72, A73, Th24;
A75: ((len f) + i1) - j = ((len f) + i1) -' j by A40, NAT_D:37;
(len f) + 0 < (len f) + i1 by A2, XREAL_1:10;
then j < (len f) + i1 by A67, XXREAL_0:2;
then j - j < ((len f) + i1) - j by XREAL_1:11;
then A76: 0 < ((len f) + i1) -' j by A65, A66, NAT_D:37, XXREAL_0:2;
i1 + 1 <= j by A34, A62, NAT_1:13;
then (len f) + (i1 + 1) <= (len f) + j by XREAL_1:8;
then (((len f) + i1) + 1) - 1 <= ((len f) + j) - 1 by XREAL_1:11;
then ((len f) + i1) - j <= (((len f) + j) - 1) - j by XREAL_1:11;
then A77: (len f) -' 1 >= ((len f) + i1) -' j by A6, A65, A66, NAT_D:37, XXREAL_0:2;

now

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

case A78: (((len f) + i1) -' j) mod ((len f) -' 1) = 0 ; :: thesis: g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j

then ((len f) + i1) -' j = (len f) -' 1 by A76, A77, Th9;
hence g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j by A38, A74, A78, Def1; :: thesis: verum

end;

case A79: (((len f) + i1) -' j) mod ((len f) -' 1) <> 0 ; :: thesis: g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j

then A80: S_Drop (((len f) + i1) -' j),f = (((len f) + i1) -' j) mod ((len f) -' 1) by Def1;
(len f) + (i1 + 1) <= (len f) + j by A63, XREAL_1:9;
then (((len f) + i1) + 1) - j <= ((len f) + j) - j by XREAL_1:11;
then A81: ((((len f) + i1) + 1) - j) - 1 <= (len f) - 1 by XREAL_1:11;
not ((len f) + i1) - j = (len f) -' 1 by A75, A79, NAT_D:25;
then ((len f) + i1) -' j < (len f) -' 1 by A6, A75, A81, XXREAL_0:1;
hence g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j by A38, A74, A80, NAT_D:24; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

hence ( len g = ((len f) + i1) -' i2 & g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) ) by A11, A32, A35, FINSEQ_2:10, NAT_D:37; :: thesis: verum

end;

case n <> 0 ; :: thesis: contradiction

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

now

per cases ( 1 = n or 1 < n ) by A82, XXREAL_0:1;

case A83: 1 = n ; :: thesis: contradiction

A84: ((len f) + i1) -' (len g) = ((len f) + i1) - (len g) by A2, NAT_D:37;
(i1 + 1) + 0 < i2 + (len g) by A1, A2, XREAL_1:10;
hence contradiction by A6, A30, A83, A84; :: thesis: verum

end;

case 1 < n ; :: thesis: contradiction

then 1 + 1 <= n by NAT_1:13;
then ((len f) -' 1) * n >= ((len f) -' 1) * (1 + 1) by XREAL_1:66;
then A85: ((len f) + i1) -' (len g) >= (((len f) -' 1) * (1 + 1)) + i2 by A30, XREAL_1:8;
(i1 + 1) - 1 <= (len f) - 1 by A2, XREAL_1:11;
then 1 + i1 <= (len g) + ((len f) -' 1) by A2, A6, XREAL_1:9;
then ((len f) - 1) + (1 + i1) <= ((len f) - 1) + ((len g) + ((len f) -' 1)) by XREAL_1:8;
then A86: ((len f) + i1) - (len g) <= ((((len f) - 1) + (len g)) + ((len f) -' 1)) - (len g) by XREAL_1:11;
A87: ((len f) + i1) - (len g) = ((len f) + i1) -' (len g) by A2, NAT_D:37;
((len f) -' 1) * (1 + 1) < (((len f) -' 1) * (1 + 1)) + i2 by A1, XREAL_1:31;
hence contradiction by A6, A85, A86, A87, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

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

end;

case A88: (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 ; :: thesis: ( len g = ((len f) + i1) -' i2 & g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) )

ex n being Nat st
( ((len f) + i1) -' (len g) = (((len f) -' 1) * n) + ((((len f) + i1) -' (len g)) mod ((len f) -' 1)) & (((len f) + i1) -' (len g)) mod ((len f) -' 1) < (len f) -' 1 ) by A7, NAT_D:def 2;
then consider n being Nat such that
A89: ((len f) + i1) -' (len g) = (((len f) -' 1) * n) + ((((len f) + i1) -' (len g)) mod ((len f) -' 1)) ;
A90: ((len f) + i1) -' (len g) = i2 * n by A27, A88, A89, Def1;

now

assume n = 0 ; :: thesis: contradiction
then A91: (len f) + i1 <= len g by A88, A89, NAT_D:36;
len f <= (len f) + i1 by NAT_1:11;
hence contradiction by A2, A91, XXREAL_0:2; :: thesis: verum

end;

then n > 0 ;
then A92: n >= 0 + 1 by NAT_1:13;

now

assume n > 1 ; :: thesis: contradiction
then n >= 1 + 1 by NAT_1:13;
then A93: ((len f) + i1) -' (len g) >= ((len f) -' 1) * (1 + 1) by A88, A89, NAT_1:4;

now

assume i1 + 1 < len f ; :: thesis: contradiction
then (i1 + 1) + 1 < (len f) + (len g) by A2, XREAL_1:10;
then ((i1 + 1) + 1) - 1 < ((len f) + (len g)) - 1 by XREAL_1:11;
then (i1 + 1) - (len g) < (((len f) + (len g)) - 1) - (len g) by XREAL_1:11;
then ((len f) - 1) + ((i1 + 1) - (len g)) < ((len f) - 1) + ((len f) - 1) by XREAL_1:8;
then ((len f) + i1) - (len g) < ((len f) - 1) + ((len f) - 1) ;
hence contradiction by A2, A6, A93, NAT_D:37; :: thesis: verum

end;

then i1 + 1 = len f by A2, XXREAL_0:1;
then i2 + 1 > ((len f) - 1) + 1 by A1, XREAL_1:8;
hence contradiction by A1, Def3; :: thesis: verum

end;

then n = 1 by A92, XXREAL_0:1;
then A94: ((len f) + i1) - (len g) = i2 by A2, A90, NAT_D:37;
then A95: ((len f) + i1) - i2 = len g ;
A96: len (mid f,i1,1) = (i1 -' 1) + 1 by A2, A3, Th21
.= i1 by A2, XREAL_1:237 ;
len (mid f,((len f) -' 1),i2) = (((len f) -' 1) -' i2) + 1 by A2, A6, A8, A9, Th21;
then len (mid f,((len f) -' 1),i2) = (((len f) - 1) - i2) + 1 by A6, A8, XREAL_1:235;
then len ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) = i1 + ((len f) - i2) by A96, FINSEQ_1:35
.= (i1 + (len f)) - i2
.= ((len f) + i1) -' i2 by A11, NAT_D:37 ;
then A97: ( len g = len g & len ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) = len g ) by A11, A95, NAT_D:37;
X: dom g = Seg (len g) by FINSEQ_1:def 3;
for j being Nat st j in dom g holds
g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j

proof

let j be Nat; :: thesis: ( j in dom g implies g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j )
assume A98: j in dom g ; :: thesis: g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j
then A99: ( 1 <= j & j <= len g ) by X, FINSEQ_1:3;
then A100: g . j = f . (S_Drop (((len f) + i1) -' j),f) by A1, Def3;
A101: j in NAT by ORDINAL1:def 13;
A102: j < len f by A2, A99, XXREAL_0:2;
then A103: ((len f) + i1) -' j = ((len f) + i1) - j by NAT_D:37;

now

per cases ( j <= len (mid f,i1,1) or j > len (mid f,i1,1) ) ;

case A104: j <= len (mid f,i1,1) ; :: thesis: g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j

then j in dom (mid f,i1,1) by A99, FINSEQ_3:27;
then A105: ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j = (mid f,i1,1) . j by FINSEQ_1:def 7;
A106: len (mid f,i1,1) = (i1 -' 1) + 1 by A2, A10, Th21;
(len f) -' 1 <= len f by NAT_D:50;
then ((len f) - 1) + j <= (len f) + i1 by A6, A96, A104, XREAL_1:9;
then A107: (((len f) - 1) + j) - j <= ((len f) + i1) - j by XREAL_1:11;

now

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

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

then ((len f) + i1) - j = (len f) - 1 by A6, A96, A104, NAT_D:37;
then i1 + 1 = j ;
hence g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j by A96, A104, NAT_1:13; :: thesis: verum

end;

case ((len f) + i1) -' j <> (len f) -' 1 ; :: thesis: g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j

then A108: ((len f) + i1) -' j > (len f) -' 1 by A6, A103, A107, XXREAL_0:1;
A109: j - 1 >= 0 by A99, XREAL_1:50;
then j - 1 = j -' 1 by XREAL_0:def 2;
then A110: len f <= (len f) + (j - 1) by NAT_1:11;

now

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

case A111: ( i1 + 1 = len f & j - 1 = 0 ) ; :: thesis: g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j

then ((len f) + i1) -' j = (((len f) - 1) + (len f)) - 1 by A2, NAT_D:37
.= ((len f) -' 1) + ((len f) -' 1) by A6 ;
then (((len f) + i1) -' j) mod ((len f) -' 1) = 0 by Th8;
then S_Drop (((len f) + i1) -' j),f = (j + i1) -' 1 by A111, Def1;
then A112: S_Drop (((len f) + i1) -' j),f = (i1 + 1) - 1 by A111, NAT_D:37
.= (i1 - j) + 1 by A111 ;
A113: (i1 - j) + 1 = (i1 -' j) + 1 by A96, A104, XREAL_1:235;
A114: f . (S_Drop (((len f) + i1) -' j),f) = f . ((i1 -' j) + 1) by A96, A104, A112, XREAL_1:235;
A115: 1 <= (i1 -' j) + 1 by NAT_1:11;
A116: j - 1 = j -' 1 by A99, XREAL_1:235;
i1 <= i1 + (j -' 1) by NAT_1:11;
then A117: i1 - (j -' 1) <= i1 by XREAL_1:22;
(mid f,i1,1) . j = (mid f,1,i1) . ((((i1 - 1) + 1) - j) + 1) by A2, A10, A99, A101, A104, A106, Th25
.= f . ((i1 -' j) + 1) by A10, A113, A115, A116, A117, JORDAN3:32 ;
hence g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j by A1, A99, A105, A114, Def3; :: thesis: verum

end;

case A118: ( i1 + 1 <> len f or j - 1 <> 0 ) ; :: thesis: g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j

now

per cases ( i1 + 1 <> len f or j - 1 <> 0 ) by A118;

case i1 + 1 <> len f ; :: thesis: i1 + 1 < (len f) + (j - 1)

then i1 + 1 < len f by A2, XXREAL_0:1;
hence i1 + 1 < (len f) + (j - 1) by A110, XXREAL_0:2; :: thesis: verum

end;

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

then len f < (len f) + (j - 1) by A109, XREAL_1:31;
hence i1 + 1 < (len f) + (j - 1) by A2, XXREAL_0:2; :: thesis: verum

end;

end;

end;

then (i1 + 1) - j < (((len f) - 1) + j) - j by XREAL_1:11;
then A119: ((len f) - 1) + ((i1 + 1) - j) < ((len f) - 1) + ((len f) - 1) by XREAL_1:10;
then (((len f) + i1) -' j) mod ((len f) -' 1) <> 0 by A2, A4, A6, A103, A108, Th6;
then A120: S_Drop (((len f) + i1) -' j),f = (((len f) + i1) -' j) mod ((len f) -' 1) by Def1
.= ((len f) + (i1 - j)) - ((len f) - 1) by A2, A4, A6, A103, A107, A119, Th7
.= (i1 - j) + 1 ;
A121: (i1 - j) + 1 = (i1 -' j) + 1 by A96, A104, XREAL_1:235;
A122: 1 <= (i1 -' j) + 1 by NAT_1:11;
A123: j - 1 = j -' 1 by A99, XREAL_1:235;
i1 <= i1 + (j -' 1) by NAT_1:11;
then A124: i1 - (j -' 1) <= i1 by XREAL_1:22;
(mid f,i1,1) . j = (mid f,1,i1) . ((((i1 - 1) + 1) - j) + 1) by A2, A10, A99, A101, A104, A106, Th25
.= f . ((i1 -' j) + 1) by A10, A121, A122, A123, A124, JORDAN3:32 ;
hence g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j by A96, A100, A104, A105, A120, XREAL_1:235; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

case A125: j > len (mid f,i1,1) ; :: thesis: g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j

then A126: i1 + 1 <= j by A96, NAT_1:13;
A127: ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j = (mid f,((len f) -' 1),i2) . (j - (len (mid f,i1,1))) by A97, A99, A125, JORDAN3:15;
A128: j <= ((len f) + i1) - i2 by A94, A98, X, FINSEQ_1:3;
i2 - i1 >= 0 by A1, XREAL_1:50;
then (len f) + 0 <= (len f) + (i2 - i1) by XREAL_1:9;
then A129: (len f) - (i2 - i1) <= ((len f) + (i2 - i1)) - (i2 - i1) by XREAL_1:11;
then A130: j <= len f by A128, XXREAL_0:2;
i1 + 1 <= j by A96, A125, NAT_1:13;
then A131: (i1 + 1) - i1 <= j - i1 by XREAL_1:11;
(i2 + 1) - 1 <= (len f) - 1 by A2, XREAL_1:11;
then A132: i2 - i2 <= ((len f) - 1) - i2 by XREAL_1:11;
A133: j - i1 <= (((len f) + i1) - i2) - i1 by A94, A99, XREAL_1:11;
(len f) - i2 <= (len f) - 1 by A2, XREAL_1:15;
then j - i1 <= (len f) -' 1 by A6, A133, XXREAL_0:2;
then A134: j -' i1 <= (len f) -' 1 by A96, A125, XREAL_1:235;
A135: (len f) - i2 = (((len f) - 1) - i2) + 1
.= (((len f) -' 1) -' i2) + 1 by A6, A132, XREAL_0:def 2 ;
A136: j - i1 = j -' (len (mid f,i1,1)) by A96, A131, XREAL_0:def 2;
(((len f) -' 1) -' (j -' i1)) + 1 = (((len f) -' 1) - (j -' i1)) + 1 by A134, XREAL_1:235
.= (((len f) - 1) - (j - i1)) + 1 by A6, A96, A125, XREAL_1:235
.= ((len f) + i1) - j
.= ((len f) + i1) -' j by A128, A129, NAT_D:37, XXREAL_0:2 ;
then A137: ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j = f . (((len f) + i1) -' j) by A2, A6, A8, A9, A96, A127, A131, A133, A135, A136, Th24;
A138: ((len f) + i1) - j = ((len f) + i1) -' j by A102, NAT_D:37;
(len f) + 0 < (len f) + i1 by A2, XREAL_1:10;
then j < (len f) + i1 by A130, XXREAL_0:2;
then j - j < ((len f) + i1) - j by XREAL_1:11;
then A139: 0 < ((len f) + i1) -' j by A128, A129, NAT_D:37, XXREAL_0:2;
i1 + 1 <= j by A96, A125, NAT_1:13;
then (len f) + (i1 + 1) <= (len f) + j by XREAL_1:8;
then (((len f) + i1) + 1) - 1 <= ((len f) + j) - 1 by XREAL_1:11;
then ((len f) + i1) - j <= (((len f) + j) - 1) - j by XREAL_1:11;
then A140: (len f) -' 1 >= ((len f) + i1) -' j by A6, A128, A129, NAT_D:37, XXREAL_0:2;

now

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

case A141: (((len f) + i1) -' j) mod ((len f) -' 1) = 0 ; :: thesis: g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j

then ((len f) + i1) -' j = (len f) -' 1 by A139, A140, Th9;
hence g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j by A100, A137, A141, Def1; :: thesis: verum

end;

case A142: (((len f) + i1) -' j) mod ((len f) -' 1) <> 0 ; :: thesis: g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j

then A143: S_Drop (((len f) + i1) -' j),f = (((len f) + i1) -' j) mod ((len f) -' 1) by Def1;
(len f) + (i1 + 1) <= (len f) + j by A126, XREAL_1:9;
then (((len f) + i1) + 1) - j <= ((len f) + j) - j by XREAL_1:11;
then A144: ((((len f) + i1) + 1) - j) - 1 <= (len f) - 1 by XREAL_1:11;
not ((len f) + i1) - j = (len f) -' 1 by A138, A142, NAT_D:25;
then ((len f) + i1) -' j < (len f) -' 1 by A6, A138, A144, XXREAL_0:1;
hence g . j = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . j by A100, A137, A143, NAT_D:24; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

hence ( len g = ((len f) + i1) -' i2 & g = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) ) by A11, A95, A97, FINSEQ_2:10, NAT_D:37; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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