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 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, Def3;
A4: 1 <= i1 by A1, Def3;
g . (len g) = f . i2 by A1, Def3;
then A5: f . i2 = f . (S_Drop ((((len f) + i1) -' (len g)),f)) by A1, A3, Def3;
A6: i2 <= i2 + 1 by NAT_1:11;
A7: i2 + 1 <= len f by A1, Def3;
then A8: (i2 + 1) - 1 <= (len f) - 1 by XREAL_1:9;
A9: i1 + 1 <= len f by A1, Def3;
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

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, Def3;

A20: 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 + 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, Def3;
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

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

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

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, Th21
.= i1 by A4, XREAL_1:235 ;
len (mid (f,((len f) -' 1),i2)) = (((len f) -' 1) -' i2) + 1 by A19, A11, A8, A26, Th21;
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, Def3;
A49: ((len f) + i1) -' j = ((len f) + i1) - j by A27, A47, NAT_D:37, XXREAL_0:2;
A50: j in NAT by ORDINAL1:def 12;

now

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

case A51: 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, A51, XREAL_1:7;
then A52: (((len f) - 1) + j) - j <= ((len f) + i1) - j by XREAL_1:9;
j in dom (mid (f,i1,1)) by A46, A51, FINSEQ_3:25;
then A53: ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j = (mid (f,i1,1)) . j by FINSEQ_1:def 7;
A54: len (mid (f,i1,1)) = (i1 -' 1) + 1 by A4, A23, Th21;

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

end;

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

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

now

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

case A59: ( 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 Th8;
then S_Drop ((((len f) + i1) -' j),f) = (j + i1) -' 1 by A59, Def1;
then A60: S_Drop ((((len f) + i1) -' j),f) = (1 + i1) - 1 by A59, NAT_D:37
.= (i1 - j) + 1 by A59 ;
A61: 1 <= (i1 -' j) + 1 by NAT_1:11;
i1 <= i1 + (j -' 1) by NAT_1:11;
then A62: i1 - (j -' 1) <= i1 by XREAL_1:20;
A63: (i1 - j) + 1 = (i1 -' j) + 1 by A41, A51, XREAL_1:233;
A64: 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, A51, A54, Th25
.= f . ((i1 -' j) + 1) by A23, A63, A61, A64, A62, FINSEQ_6:123 ;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A41, A48, A51, A53, A60, XREAL_1:233; :: thesis: verum

end;

case A65: ( 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 A65;

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 A57, 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 A56, 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 A66: ((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, A58, Th6;
then A67: 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, A52, A66, Th7
.= (i1 - j) + 1 ;
A68: 1 <= (i1 -' j) + 1 by NAT_1:11;
i1 <= i1 + (j -' 1) by NAT_1:11;
then A69: i1 - (j -' 1) <= i1 by XREAL_1:20;
A70: (i1 - j) + 1 = (i1 -' j) + 1 by A41, A51, XREAL_1:233;
A71: 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, A51, A54, Th25
.= f . ((i1 -' j) + 1) by A23, A70, A68, A71, A69, FINSEQ_6:123 ;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A41, A48, A51, A53, A67, 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 A72: 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 A73: i2 - i2 <= ((len f) - 1) - i2 by XREAL_1:9;
A74: (len f) - i2 = (((len f) - 1) - i2) + 1
.= (((len f) -' 1) -' i2) + 1 by A11, A73, XREAL_0:def 2 ;
A75: (len f) + 0 < (len f) + i1 by A4, XREAL_1:8;
A76: ((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, A72, FINSEQ_6:108;
A77: j - i1 <= (((len f) + i1) - i2) - i1 by A39, A47, XREAL_1:9;
i1 + 1 <= j by A41, A72, NAT_1:13;
then A78: (i1 + 1) - i1 <= j - i1 by XREAL_1:9;
then A79: 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 A80: (len f) - (i2 - i1) <= ((len f) + (i2 - i1)) - (i2 - i1) by XREAL_1:9;
A81: j <= ((len f) + i1) - i2 by A39, A43, A45, FINSEQ_1:1;
then j <= len f by A80, XXREAL_0:2;
then j < (len f) + i1 by A75, XXREAL_0:2;
then j - j < ((len f) + i1) - j by XREAL_1:9;
then A82: 0 < ((len f) + i1) -' j by A81, A80, 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, A77, XXREAL_0:2;
then j -' i1 <= (len f) -' 1 by A41, A72, 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, A72, XREAL_1:233
.= ((len f) + i1) - j
.= ((len f) + i1) -' j by A81, A80, NAT_D:37, XXREAL_0:2 ;
then A83: ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j = f . (((len f) + i1) -' j) by A19, A11, A8, A26, A41, A76, A78, A77, A74, A79, Th24;
A84: i1 + 1 <= j by A41, A72, NAT_1:13;
A85: ((len f) + i1) - j = ((len f) + i1) -' j by A27, A47, NAT_D:37, XXREAL_0:2;
i1 + 1 <= j by A41, A72, 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 A86: (len f) -' 1 >= ((len f) + i1) -' j by A11, A81, A80, 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 A87: (((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 A82, A86, Th9;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A48, A83, A87, Def1; :: thesis: verum

end;

case A88: (((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 A84, XREAL_1:7;
then (((len f) + i1) + 1) - j <= ((len f) + j) - j by XREAL_1:9;
then A89: ((((len f) + i1) + 1) - j) - 1 <= (len f) - 1 by XREAL_1:9;
A90: S_Drop ((((len f) + i1) -' j),f) = (((len f) + i1) -' j) mod ((len f) -' 1) by A88, Def1;
not ((len f) + i1) - j = (len f) -' 1 by A85, A88, NAT_D:25;
then ((len f) + i1) -' j < (len f) -' 1 by A11, A85, A89, XXREAL_0:1;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A48, A83, A90, 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 A91: 0 + 1 <= n by NAT_1:13;

now

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

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

A93: ((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, A92, A93; :: 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 A94: ((len f) + i1) -' (len g) >= (((len f) -' 1) * (1 + 1)) + i2 by A38, XREAL_1:6;
A95: ((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 A96: ((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, A94, A96, A95, 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 A97: (((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
A98: ((len f) + i1) -' (len g) = (((len f) -' 1) * n) + ((((len f) + i1) -' (len g)) mod ((len f) -' 1)) ;

A99: now

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

now

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, A100, 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, Def3; :: thesis: verum

end;

now

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

end;

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

now

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

case A114: 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, A106, A114, XREAL_1:7;
then A115: (((len f) - 1) + j) - j <= ((len f) + i1) - j by XREAL_1:9;
j in dom (mid (f,i1,1)) by A109, A114, FINSEQ_3:25;
then A116: ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j = (mid (f,i1,1)) . j by FINSEQ_1:def 7;
A117: len (mid (f,i1,1)) = (i1 -' 1) + 1 by A4, A23, Th21;

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

end;

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

A119: j - 1 >= 0 by A109, XREAL_1:48;
then j - 1 = j -' 1 by XREAL_0:def 2;
then A120: len f <= (len f) + (j - 1) by NAT_1:11;
A121: ((len f) + i1) -' j > (len f) -' 1 by A11, A112, A115, A118, XXREAL_0:1;

now

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

case A122: ( 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 Th8;
then S_Drop ((((len f) + i1) -' j),f) = (j + i1) -' 1 by A122, Def1;
then S_Drop ((((len f) + i1) -' j),f) = (i1 + 1) - 1 by A122, NAT_D:37
.= (i1 - j) + 1 by A122 ;
then A123: f . (S_Drop ((((len f) + i1) -' j),f)) = f . ((i1 -' j) + 1) by A106, A114, XREAL_1:233;
A124: 1 <= (i1 -' j) + 1 by NAT_1:11;
i1 <= i1 + (j -' 1) by NAT_1:11;
then A125: i1 - (j -' 1) <= i1 by XREAL_1:20;
A126: (i1 - j) + 1 = (i1 -' j) + 1 by A106, A114, XREAL_1:233;
A127: j - 1 = j -' 1 by A109, XREAL_1:233;
(mid (f,i1,1)) . j = (mid (f,1,i1)) . ((((i1 - 1) + 1) - j) + 1) by A4, A23, A109, A113, A114, A117, Th25
.= f . ((i1 -' j) + 1) by A23, A126, A124, A127, A125, FINSEQ_6:123 ;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A1, A109, A110, A116, A123, Def3; :: thesis: verum

end;

case A128: ( 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 A128;

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 A120, 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 A119, 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 A129: ((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, A112, A121, Th6;
then A130: 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, A112, A115, A129, Th7
.= (i1 - j) + 1 ;
A131: 1 <= (i1 -' j) + 1 by NAT_1:11;
i1 <= i1 + (j -' 1) by NAT_1:11;
then A132: i1 - (j -' 1) <= i1 by XREAL_1:20;
A133: (i1 - j) + 1 = (i1 -' j) + 1 by A106, A114, XREAL_1:233;
A134: j - 1 = j -' 1 by A109, XREAL_1:233;
(mid (f,i1,1)) . j = (mid (f,1,i1)) . ((((i1 - 1) + 1) - j) + 1) by A4, A23, A109, A113, A114, A117, Th25
.= f . ((i1 -' j) + 1) by A23, A133, A131, A134, A132, FINSEQ_6:123 ;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A106, A111, A114, A116, A130, 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 A135: 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 A136: i2 - i2 <= ((len f) - 1) - i2 by XREAL_1:9;
A137: (len f) - i2 = (((len f) - 1) - i2) + 1
.= (((len f) -' 1) -' i2) + 1 by A11, A136, XREAL_0:def 2 ;
A138: (len f) + 0 < (len f) + i1 by A4, XREAL_1:8;
A139: ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j = (mid (f,((len f) -' 1),i2)) . (j - (len (mid (f,i1,1)))) by A107, A110, A135, FINSEQ_6:108;
A140: j - i1 <= (((len f) + i1) - i2) - i1 by A103, A110, XREAL_1:9;
i1 + 1 <= j by A106, A135, NAT_1:13;
then A141: (i1 + 1) - i1 <= j - i1 by XREAL_1:9;
then A142: j - i1 = j -' (len (mid (f,i1,1))) by A106, 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 A143: (len f) - (i2 - i1) <= ((len f) + (i2 - i1)) - (i2 - i1) by XREAL_1:9;
A144: j <= ((len f) + i1) - i2 by A103, A105, A108, FINSEQ_1:1;
then j <= len f by A143, XXREAL_0:2;
then j < (len f) + i1 by A138, XXREAL_0:2;
then j - j < ((len f) + i1) - j by XREAL_1:9;
then A145: 0 < ((len f) + i1) -' j by A144, A143, 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, A140, XXREAL_0:2;
then j -' i1 <= (len f) -' 1 by A106, A135, 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, A106, A135, XREAL_1:233
.= ((len f) + i1) - j
.= ((len f) + i1) -' j by A144, A143, NAT_D:37, XXREAL_0:2 ;
then A146: ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j = f . (((len f) + i1) -' j) by A19, A11, A8, A26, A106, A139, A141, A140, A137, A142, Th24;
A147: i1 + 1 <= j by A106, A135, NAT_1:13;
A148: ((len f) + i1) - j = ((len f) + i1) -' j by A27, A110, NAT_D:37, XXREAL_0:2;
i1 + 1 <= j by A106, A135, 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 A149: (len f) -' 1 >= ((len f) + i1) -' j by A11, A144, A143, 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 A150: (((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 A145, A149, Th9;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A111, A146, A150, Def1; :: thesis: verum

end;

case A151: (((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 A147, XREAL_1:7;
then (((len f) + i1) + 1) - j <= ((len f) + j) - j by XREAL_1:9;
then A152: ((((len f) + i1) + 1) - j) - 1 <= (len f) - 1 by XREAL_1:9;
A153: S_Drop ((((len f) + i1) -' j),f) = (((len f) + i1) -' j) mod ((len f) -' 1) by A151, Def1;
not ((len f) + i1) - j = (len f) -' 1 by A148, A151, NAT_D:25;
then ((len f) + i1) -' j < (len f) -' 1 by A11, A148, A152, XXREAL_0:1;
hence g . j = ((mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2))) . j by A111, A146, A153, 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, A104, A107, 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