let f be constant standard special_circular_sequence; :: thesis: for g being FinSequence of (TOP-REAL 2)
for i1, i2 being 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 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 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 that
A1: g is_a_part<_of f,i1,i2 and
A2: i1 < i2 ; :: thesis: ( len g = ((len f) + i1) -' i2 & g = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) )
A3: 1 <= len g by A1;
A4: 1 <= i1 by A1;
A5: f . i2 = f . (S_Drop ((((len f) + i1) -' (len g)),f)) by A1;
A6: i2 <= i2 + 1 by NAT_1:11;
A7: i2 + 1 <= len f by A1;
then A8: (i2 + 1) - 1 <= (len f) - 1 by XREAL_1:9;
A9: i1 + 1 <= len f by A1;
then (i1 + 1) - 1 <= (len f) - 1 by XREAL_1:9;
then A10: 1 <= (len f) - 1 by A4, XXREAL_0:2;
then A11: (len f) - 1 = (len f) -' 1 by NAT_D:39;

A12: now :: thesis: ( ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 & S_Drop ((((len f) + i1) -' (len g)),f) < len f ) or ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 & S_Drop ((((len f) + i1) -' (len g)),f) < len f ) )

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

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

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

end;

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

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

end;

end;

end;

A19: 1 <= i2 by A1;

A20: now :: thesis: ( ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 & 1 <= S_Drop ((((len f) + i1) -' (len g)),f) ) or ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 & 1 <= S_Drop ((((len f) + i1) -' (len g)),f) ) )

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 + 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 A21: (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 ; :: thesis: 1 <= S_Drop ((((len f) + i1) -' (len g)),f)

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

end;

end;

end;

i1 <= i1 + 1 by NAT_1:11;
then A23: i1 <= len f by A9, XXREAL_0:2;
i1 <= i1 + 1 by NAT_1:12;
then A24: i1 <= len f by A9, XXREAL_0:2;
A25: 0 <> (len f) -' 1 by A10, NAT_D:39;
i1 <= (len f) -' 1 by A9, NAT_D:49;
then 1 <= (len f) -' 1 by A4, XXREAL_0:2;
then A26: (len f) -' 1 < len f by NAT_D:51;
A27: len g < len f by A1;
A28: i2 <= (len f) -' 1 by A7, NAT_D:49;
then 1 <= (len f) -' 1 by A19, XXREAL_0:2;
then (len f) -' 1 < len f by NAT_D:51;
then A29: i2 < len f by A28, XXREAL_0:2;

now :: thesis: ( ( i2 < S_Drop ((((len f) + i1) -' (len g)),f) & contradiction ) or ( i2 > S_Drop ((((len f) + i1) -' (len g)),f) & contradiction ) or ( i2 = S_Drop ((((len f) + i1) -' (len g)),f) & len g = ((len f) + i1) -' i2 & g = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) ) )

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 A30: i2 < S_Drop ((((len f) + i1) -' (len g)),f) ; :: thesis: contradiction

i2 <= len f by A7, NAT_1:13;
then A31: f /. i2 = f . i2 by A19, FINSEQ_4:15;
A32: 1 <= S_Drop ((((len f) + i1) -' (len g)),f) by A19, A30, XXREAL_0:2;
f /. i2 <> f /. (S_Drop ((((len f) + i1) -' (len g)),f)) by A19, A12, A30, GOBOARD7:36;
hence contradiction by A5, A12, A31, A32, FINSEQ_4:15; :: thesis: verum

end;

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

i2 <= len f by A7, NAT_1:13;
then A34: f /. i2 = f . i2 by A19, FINSEQ_4:15;
f /. i2 <> f /. (S_Drop ((((len f) + i1) -' (len g)),f)) by A20, A29, A33, GOBOARD7:36;
hence contradiction by A5, A20, A12, A34, FINSEQ_4:15; :: thesis: verum

end;

case A35: 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 :: thesis: ( ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 & len g = ((len f) + i1) -' i2 & g = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) ) or ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 & len g = ((len f) + i1) -' i2 & g = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) ) )

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

case A36: (((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 A25, NAT_D:def 2;
then consider n being Nat such that
A37: ((len f) + i1) -' (len g) = (((len f) -' 1) * n) + ((((len f) + i1) -' (len g)) mod ((len f) -' 1)) ;
A38: ((len f) + i1) -' (len g) = (((len f) -' 1) * n) + i2 by A35, A36, A37, Def1;

now :: thesis: ( ( n = 0 & len g = ((len f) + i1) -' i2 & g = (mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) ) or ( n <> 0 & contradiction ) )

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 A39: i2 = ((len f) + i1) -' (len g) by A35, A36, A37, Def1
.= ((len f) + i1) - (len g) by A27, NAT_D:37
.= ((len f) - (len g)) + i1 ;
then A40: len g = ((len f) + i1) - i2 ;
A41: len (mid (f,i1,1)) = (i1 -' 1) + 1 by A4, A24, FINSEQ_6:187
.= i1 by A4, XREAL_1:235 ;
len (mid (f,((len f) -' 1),i2)) = (((len f) -' 1) -' i2) + 1 by A19, A11, A8, A26, FINSEQ_6:187;
then A42: len (mid (f,((len f) -' 1),i2)) = (((len f) -' 1) - i2) + 1 by A11, A8, XREAL_1:233;
A43: dom g = Seg (len g) by FINSEQ_1:def 3;
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:22;
then len ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) = (i1 + (len f)) - i2 by A11, A41, A42
.= ((len f) + i1) -' i2 by A7, A6, NAT_D:37, XXREAL_0:2 ;
then A44: len ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) = len g by A7, A6, A40, NAT_D:37, XXREAL_0:2;
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 A45: j in dom g ; :: thesis: g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j
then A46: 1 <= j by A43, FINSEQ_1:1;
A47: j <= len g by A43, A45, FINSEQ_1:1;
then A48: g . j = f . (S_Drop ((((len f) + i1) -' j),f)) by A1, A46;
A49: ((len f) + i1) -' j = ((len f) + i1) - j by A27, A47, NAT_D:37, XXREAL_0:2;

now :: thesis: ( ( j <= len (mid (f,i1,1)) & g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j ) or ( j > len (mid (f,i1,1)) & g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j ) )

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

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

(len f) -' 1 <= len f by NAT_D:50;
then ((len f) - 1) + j <= (len f) + i1 by A11, A41, A50, XREAL_1:7;
then A51: (((len f) - 1) + j) - j <= ((len f) + i1) - j by XREAL_1:9;
j in dom (mid (f,i1,1)) by A46, A50, FINSEQ_3:25;
then A52: ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j = (mid (f,i1,1)) . j by FINSEQ_1:def 7;
A53: len (mid (f,i1,1)) = (i1 -' 1) + 1 by A4, A23, FINSEQ_6:187;

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

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 A11, A41, A50, NAT_D:37;
then i1 + 1 = j ;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A41, A50, NAT_1:13; :: thesis: verum

end;

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

A55: j - 1 >= 0 by A46, XREAL_1:48;
then j - 1 = j -' 1 by XREAL_0:def 2;
then A56: len f <= (len f) + (j - 1) by NAT_1:11;
A57: ((len f) + i1) -' j > (len f) -' 1 by A11, A49, A51, A54, XXREAL_0:1;

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

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

case A58: ( 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 A4, NAT_D:37
.= ((len f) -' 1) + ((len f) -' 1) by A11 ;
then (((len f) + i1) -' j) mod ((len f) -' 1) = 0 by Th3;
then S_Drop ((((len f) + i1) -' j),f) = (j + i1) -' 1 by A58, Def1;
then A59: S_Drop ((((len f) + i1) -' j),f) = (1 + i1) - 1 by A58, NAT_D:37
.= (i1 - j) + 1 by A58 ;
A60: 1 <= (i1 -' j) + 1 by NAT_1:11;
i1 <= i1 + (j -' 1) by NAT_1:11;
then A61: i1 - (j -' 1) <= i1 by XREAL_1:20;
A62: (i1 - j) + 1 = (i1 -' j) + 1 by A41, A50, XREAL_1:233;
A63: j - 1 = j -' 1 by A46, XREAL_1:233;
(mid (f,i1,1)) . j = (mid (f,1,i1)) . ((((i1 - 1) + 1) - j) + 1) by A4, A23, A46, A50, A53, FINSEQ_6:191
.= f . ((i1 -' j) + 1) by A23, A62, A60, A63, A61, FINSEQ_6:123 ;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A41, A48, A50, A52, A59, XREAL_1:233; :: thesis: verum

end;

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

now :: thesis: ( ( i1 + 1 <> len f & i1 + 1 < (len f) + (j - 1) ) or ( j - 1 <> 0 & i1 + 1 < (len f) + (j - 1) ) )

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

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

then i1 + 1 < len f by A9, XXREAL_0:1;
hence i1 + 1 < (len f) + (j - 1) by A56, 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 A55, XREAL_1:29;
hence i1 + 1 < (len f) + (j - 1) by A9, XXREAL_0:2; :: thesis: verum

end;

end;

end;

then (i1 + 1) - j < (((len f) - 1) + j) - j by XREAL_1:9;
then A65: ((len f) - 1) + ((i1 + 1) - j) < ((len f) - 1) + ((len f) - 1) by XREAL_1:8;
then (((len f) + i1) -' j) mod ((len f) -' 1) <> 0 by A11, A49, A57, Th1;
then A66: 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 A11, A49, A51, A65, Th2
.= (i1 - j) + 1 ;
A67: 1 <= (i1 -' j) + 1 by NAT_1:11;
i1 <= i1 + (j -' 1) by NAT_1:11;
then A68: i1 - (j -' 1) <= i1 by XREAL_1:20;
A69: (i1 - j) + 1 = (i1 -' j) + 1 by A41, A50, XREAL_1:233;
A70: j - 1 = j -' 1 by A46, XREAL_1:233;
(mid (f,i1,1)) . j = (mid (f,1,i1)) . ((((i1 - 1) + 1) - j) + 1) by A4, A23, A46, A50, A53, FINSEQ_6:191
.= f . ((i1 -' j) + 1) by A23, A69, A67, A70, A68, FINSEQ_6:123 ;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A41, A48, A50, A52, A66, XREAL_1:233; :: 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 A71: j > len (mid (f,i1,1)) ; :: thesis: g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j

(i2 + 1) - 1 <= (len f) - 1 by A7, XREAL_1:9;
then A72: i2 - i2 <= ((len f) - 1) - i2 by XREAL_1:9;
A73: (len f) - i2 = (((len f) - 1) - i2) + 1
.= (((len f) -' 1) -' i2) + 1 by A11, A72, XREAL_0:def 2 ;
A74: (len f) + 0 < (len f) + i1 by A4, XREAL_1:8;
A75: ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j = (mid (f,((len f) -' 1),i2)) . (j - (len (mid (f,i1,1)))) by A44, A47, A71, FINSEQ_6:108;
A76: j - i1 <= (((len f) + i1) - i2) - i1 by A39, A47, XREAL_1:9;
i1 + 1 <= j by A41, A71, NAT_1:13;
then A77: (i1 + 1) - i1 <= j - i1 by XREAL_1:9;
then A78: j - i1 = j -' (len (mid (f,i1,1))) by A41, XREAL_0:def 2;
i2 - i1 >= 0 by A2, XREAL_1:48;
then (len f) + 0 <= (len f) + (i2 - i1) by XREAL_1:7;
then A79: (len f) - (i2 - i1) <= ((len f) + (i2 - i1)) - (i2 - i1) by XREAL_1:9;
A80: j <= ((len f) + i1) - i2 by A39, A43, A45, FINSEQ_1:1;
then j <= len f by A79, XXREAL_0:2;
then j < (len f) + i1 by A74, XXREAL_0:2;
then j - j < ((len f) + i1) - j by XREAL_1:9;
then A81: 0 < ((len f) + i1) -' j by A80, A79, NAT_D:37, XXREAL_0:2;
(len f) - i2 <= (len f) - 1 by A19, XREAL_1:13;
then j - i1 <= (len f) -' 1 by A11, A76, XXREAL_0:2;
then j -' i1 <= (len f) -' 1 by A41, A71, XREAL_1:233;
then (((len f) -' 1) -' (j -' i1)) + 1 = (((len f) -' 1) - (j -' i1)) + 1 by XREAL_1:233
.= (((len f) - 1) - (j - i1)) + 1 by A11, A41, A71, XREAL_1:233
.= ((len f) + i1) - j
.= ((len f) + i1) -' j by A80, A79, NAT_D:37, XXREAL_0:2 ;
then A82: ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j = f . (((len f) + i1) -' j) by A19, A11, A8, A26, A41, A75, A77, A76, A73, A78, FINSEQ_6:190;
A83: i1 + 1 <= j by A41, A71, NAT_1:13;
A84: ((len f) + i1) - j = ((len f) + i1) -' j by A27, A47, NAT_D:37, XXREAL_0:2;
i1 + 1 <= j by A41, A71, NAT_1:13;
then (len f) + (i1 + 1) <= (len f) + j by XREAL_1:6;
then (((len f) + i1) + 1) - 1 <= ((len f) + j) - 1 by XREAL_1:9;
then ((len f) + i1) - j <= (((len f) + j) - 1) - j by XREAL_1:9;
then A85: (len f) -' 1 >= ((len f) + i1) -' j by A11, A80, A79, NAT_D:37, XXREAL_0:2;

now :: thesis: ( ( (((len f) + i1) -' j) mod ((len f) -' 1) = 0 & g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j ) or ( (((len f) + i1) -' j) mod ((len f) -' 1) <> 0 & g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j ) )

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

case A86: (((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 A81, A85, Th4;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A48, A82, A86, Def1; :: thesis: verum

end;

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

(len f) + (i1 + 1) <= (len f) + j by A83, XREAL_1:7;
then (((len f) + i1) + 1) - j <= ((len f) + j) - j by XREAL_1:9;
then A88: ((((len f) + i1) + 1) - j) - 1 <= (len f) - 1 by XREAL_1:9;
A89: S_Drop ((((len f) + i1) -' j),f) = (((len f) + i1) -' j) mod ((len f) -' 1) by A87, Def1;
not ((len f) + i1) - j = (len f) -' 1 by A84, A87, NAT_D:25;
then ((len f) + i1) -' j < (len f) -' 1 by A11, A84, A88, XXREAL_0:1;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A48, A82, A89, 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 A7, A6, A40, A44, FINSEQ_2:9, NAT_D:37, XXREAL_0:2; :: thesis: verum

end;

case n <> 0 ; :: thesis: contradiction

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

now :: thesis: ( ( 1 = n & contradiction ) or ( 1 < n & contradiction ) )

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

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

A92: ((len f) + i1) -' (len g) = ((len f) + i1) - (len g) by A27, NAT_D:37;
(i1 + 1) + 0 < i2 + (len g) by A2, A3, XREAL_1:8;
hence contradiction by A11, A38, A91, A92; :: 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:64;
then A93: ((len f) + i1) -' (len g) >= (((len f) -' 1) * (1 + 1)) + i2 by A38, XREAL_1:6;
A94: ((len f) -' 1) * (1 + 1) < (((len f) -' 1) * (1 + 1)) + i2 by A2, XREAL_1:29;
(i1 + 1) - 1 <= (len f) - 1 by A9, XREAL_1:9;
then 1 + i1 <= (len g) + ((len f) -' 1) by A3, A11, XREAL_1:7;
then ((len f) - 1) + (1 + i1) <= ((len f) - 1) + ((len g) + ((len f) -' 1)) by XREAL_1:6;
then A95: ((len f) + i1) - (len g) <= ((((len f) - 1) + (len g)) + ((len f) -' 1)) - (len g) by XREAL_1:9;
((len f) + i1) - (len g) = ((len f) + i1) -' (len g) by A27, NAT_D:37;
hence contradiction by A11, A93, A95, A94, 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 A96: (((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 A25, NAT_D:def 2;
then consider n being Nat such that
A97: ((len f) + i1) -' (len g) = (((len f) -' 1) * n) + ((((len f) + i1) -' (len g)) mod ((len f) -' 1)) ;

A98: now :: thesis: not n > 1

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

now :: thesis: not i1 + 1 < len f

assume i1 + 1 < len f ; :: thesis: contradiction
then (i1 + 1) + 1 < (len f) + (len g) by A3, XREAL_1:8;
then ((i1 + 1) + 1) - 1 < ((len f) + (len g)) - 1 by XREAL_1:9;
then (i1 + 1) - (len g) < (((len f) + (len g)) - 1) - (len g) by XREAL_1:9;
then ((len f) - 1) + ((i1 + 1) - (len g)) < ((len f) - 1) + ((len f) - 1) by XREAL_1:6;
then ((len f) + i1) - (len g) < ((len f) - 1) + ((len f) - 1) ;
hence contradiction by A27, A11, A99, NAT_D:37; :: thesis: verum

end;

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

end;

now :: thesis: not n = 0

assume n = 0 ; :: thesis: contradiction
then A100: (len f) + i1 <= len g by A96, A97, NAT_D:36;
len f <= (len f) + i1 by NAT_1:11;
hence contradiction by A27, A100, XXREAL_0:2; :: thesis: verum

end;

then n >= 0 + 1 by NAT_1:13;
then A101: n = 1 by A98, XXREAL_0:1;
((len f) + i1) -' (len g) = i2 * n by A35, A96, A97, Def1;
then A102: ((len f) + i1) - (len g) = i2 by A27, A101, NAT_D:37;
then A103: ((len f) + i1) - i2 = len g ;
A104: dom g = Seg (len g) by FINSEQ_1:def 3;
A105: len (mid (f,i1,1)) = (i1 -' 1) + 1 by A4, A24, FINSEQ_6:187
.= i1 by A4, XREAL_1:235 ;
len (mid (f,((len f) -' 1),i2)) = (((len f) -' 1) -' i2) + 1 by A19, A11, A8, A26, FINSEQ_6:187;
then len (mid (f,((len f) -' 1),i2)) = (((len f) - 1) - i2) + 1 by A11, A8, XREAL_1:233;
then len ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) = i1 + ((len f) - i2) by A105, FINSEQ_1:22
.= (i1 + (len f)) - i2
.= ((len f) + i1) -' i2 by A7, A6, NAT_D:37, XXREAL_0:2 ;
then A106: len ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) = len g by A7, A6, A103, NAT_D:37, XXREAL_0:2;
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 A107: j in dom g ; :: thesis: g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j
then A108: 1 <= j by A104, FINSEQ_1:1;
A109: j <= len g by A104, A107, FINSEQ_1:1;
then A110: g . j = f . (S_Drop ((((len f) + i1) -' j),f)) by A1, A108;
A111: ((len f) + i1) -' j = ((len f) + i1) - j by A27, A109, NAT_D:37, XXREAL_0:2;

now :: thesis: ( ( j <= len (mid (f,i1,1)) & g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j ) or ( j > len (mid (f,i1,1)) & g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j ) )

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

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

(len f) -' 1 <= len f by NAT_D:50;
then ((len f) - 1) + j <= (len f) + i1 by A11, A105, A112, XREAL_1:7;
then A113: (((len f) - 1) + j) - j <= ((len f) + i1) - j by XREAL_1:9;
j in dom (mid (f,i1,1)) by A108, A112, FINSEQ_3:25;
then A114: ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j = (mid (f,i1,1)) . j by FINSEQ_1:def 7;
A115: len (mid (f,i1,1)) = (i1 -' 1) + 1 by A4, A23, FINSEQ_6:187;

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

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 A11, A105, A112, NAT_D:37;
then i1 + 1 = j ;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A105, A112, NAT_1:13; :: thesis: verum

end;

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

A117: j - 1 >= 0 by A108, XREAL_1:48;
then j - 1 = j -' 1 by XREAL_0:def 2;
then A118: len f <= (len f) + (j - 1) by NAT_1:11;
A119: ((len f) + i1) -' j > (len f) -' 1 by A11, A111, A113, A116, XXREAL_0:1;

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

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

case A120: ( 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 A4, NAT_D:37
.= ((len f) -' 1) + ((len f) -' 1) by A11 ;
then (((len f) + i1) -' j) mod ((len f) -' 1) = 0 by Th3;
then S_Drop ((((len f) + i1) -' j),f) = (j + i1) -' 1 by A120, Def1;
then S_Drop ((((len f) + i1) -' j),f) = (i1 + 1) - 1 by A120, NAT_D:37
.= (i1 - j) + 1 by A120 ;
then A121: f . (S_Drop ((((len f) + i1) -' j),f)) = f . ((i1 -' j) + 1) by A105, A112, XREAL_1:233;
A122: 1 <= (i1 -' j) + 1 by NAT_1:11;
i1 <= i1 + (j -' 1) by NAT_1:11;
then A123: i1 - (j -' 1) <= i1 by XREAL_1:20;
A124: (i1 - j) + 1 = (i1 -' j) + 1 by A105, A112, XREAL_1:233;
A125: j - 1 = j -' 1 by A108, XREAL_1:233;
(mid (f,i1,1)) . j = (mid (f,1,i1)) . ((((i1 - 1) + 1) - j) + 1) by A4, A23, A108, A112, A115, FINSEQ_6:191
.= f . ((i1 -' j) + 1) by A23, A124, A122, A125, A123, FINSEQ_6:123 ;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A1, A108, A109, A114, A121; :: thesis: verum

end;

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

now :: thesis: ( ( i1 + 1 <> len f & i1 + 1 < (len f) + (j - 1) ) or ( j - 1 <> 0 & i1 + 1 < (len f) + (j - 1) ) )

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

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

then i1 + 1 < len f by A9, XXREAL_0:1;
hence i1 + 1 < (len f) + (j - 1) by A118, 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 A117, XREAL_1:29;
hence i1 + 1 < (len f) + (j - 1) by A9, XXREAL_0:2; :: thesis: verum

end;

end;

end;

then (i1 + 1) - j < (((len f) - 1) + j) - j by XREAL_1:9;
then A127: ((len f) - 1) + ((i1 + 1) - j) < ((len f) - 1) + ((len f) - 1) by XREAL_1:8;
then (((len f) + i1) -' j) mod ((len f) -' 1) <> 0 by A11, A111, A119, Th1;
then A128: 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 A11, A111, A113, A127, Th2
.= (i1 - j) + 1 ;
A129: 1 <= (i1 -' j) + 1 by NAT_1:11;
i1 <= i1 + (j -' 1) by NAT_1:11;
then A130: i1 - (j -' 1) <= i1 by XREAL_1:20;
A131: (i1 - j) + 1 = (i1 -' j) + 1 by A105, A112, XREAL_1:233;
A132: j - 1 = j -' 1 by A108, XREAL_1:233;
(mid (f,i1,1)) . j = (mid (f,1,i1)) . ((((i1 - 1) + 1) - j) + 1) by A4, A23, A108, A112, A115, FINSEQ_6:191
.= f . ((i1 -' j) + 1) by A23, A131, A129, A132, A130, FINSEQ_6:123 ;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A105, A110, A112, A114, A128, XREAL_1:233; :: 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 A133: j > len (mid (f,i1,1)) ; :: thesis: g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j

(i2 + 1) - 1 <= (len f) - 1 by A7, XREAL_1:9;
then A134: i2 - i2 <= ((len f) - 1) - i2 by XREAL_1:9;
A135: (len f) - i2 = (((len f) - 1) - i2) + 1
.= (((len f) -' 1) -' i2) + 1 by A11, A134, XREAL_0:def 2 ;
A136: (len f) + 0 < (len f) + i1 by A4, XREAL_1:8;
A137: ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j = (mid (f,((len f) -' 1),i2)) . (j - (len (mid (f,i1,1)))) by A106, A109, A133, FINSEQ_6:108;
A138: j - i1 <= (((len f) + i1) - i2) - i1 by A102, A109, XREAL_1:9;
i1 + 1 <= j by A105, A133, NAT_1:13;
then A139: (i1 + 1) - i1 <= j - i1 by XREAL_1:9;
then A140: j - i1 = j -' (len (mid (f,i1,1))) by A105, XREAL_0:def 2;
i2 - i1 >= 0 by A2, XREAL_1:48;
then (len f) + 0 <= (len f) + (i2 - i1) by XREAL_1:7;
then A141: (len f) - (i2 - i1) <= ((len f) + (i2 - i1)) - (i2 - i1) by XREAL_1:9;
A142: j <= ((len f) + i1) - i2 by A102, A104, A107, FINSEQ_1:1;
then j <= len f by A141, XXREAL_0:2;
then j < (len f) + i1 by A136, XXREAL_0:2;
then j - j < ((len f) + i1) - j by XREAL_1:9;
then A143: 0 < ((len f) + i1) -' j by A142, A141, NAT_D:37, XXREAL_0:2;
(len f) - i2 <= (len f) - 1 by A19, XREAL_1:13;
then j - i1 <= (len f) -' 1 by A11, A138, XXREAL_0:2;
then j -' i1 <= (len f) -' 1 by A105, A133, XREAL_1:233;
then (((len f) -' 1) -' (j -' i1)) + 1 = (((len f) -' 1) - (j -' i1)) + 1 by XREAL_1:233
.= (((len f) - 1) - (j - i1)) + 1 by A11, A105, A133, XREAL_1:233
.= ((len f) + i1) - j
.= ((len f) + i1) -' j by A142, A141, NAT_D:37, XXREAL_0:2 ;
then A144: ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j = f . (((len f) + i1) -' j) by A19, A11, A8, A26, A105, A137, A139, A138, A135, A140, FINSEQ_6:190;
A145: i1 + 1 <= j by A105, A133, NAT_1:13;
A146: ((len f) + i1) - j = ((len f) + i1) -' j by A27, A109, NAT_D:37, XXREAL_0:2;
i1 + 1 <= j by A105, A133, NAT_1:13;
then (len f) + (i1 + 1) <= (len f) + j by XREAL_1:6;
then (((len f) + i1) + 1) - 1 <= ((len f) + j) - 1 by XREAL_1:9;
then ((len f) + i1) - j <= (((len f) + j) - 1) - j by XREAL_1:9;
then A147: (len f) -' 1 >= ((len f) + i1) -' j by A11, A142, A141, NAT_D:37, XXREAL_0:2;

now :: thesis: ( ( (((len f) + i1) -' j) mod ((len f) -' 1) = 0 & g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j ) or ( (((len f) + i1) -' j) mod ((len f) -' 1) <> 0 & g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j ) )

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

case A148: (((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 A143, A147, Th4;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A110, A144, A148, Def1; :: thesis: verum

end;

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

(len f) + (i1 + 1) <= (len f) + j by A145, XREAL_1:7;
then (((len f) + i1) + 1) - j <= ((len f) + j) - j by XREAL_1:9;
then A150: ((((len f) + i1) + 1) - j) - 1 <= (len f) - 1 by XREAL_1:9;
A151: S_Drop ((((len f) + i1) -' j),f) = (((len f) + i1) -' j) mod ((len f) -' 1) by A149, Def1;
not ((len f) + i1) - j = (len f) -' 1 by A146, A149, NAT_D:25;
then ((len f) + i1) -' j < (len f) -' 1 by A11, A146, A150, XXREAL_0:1;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A110, A144, A151, 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 A7, A6, A103, A106, FINSEQ_2:9, NAT_D:37, XXREAL_0:2; :: 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