let f be constant standard special_circular_sequence; :: thesis: for i1, i2 being Nat st 1 <= i2 & i1 > i2 & i1 < len f holds
(mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part>_of f,i1,i2
let i1, i2 be Nat; :: thesis: ( 1 <= i2 & i1 > i2 & i1 < len f implies (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part>_of f,i1,i2 )
assume that
A1: 1 <= i2 and
A2: i1 > i2 and
A3: i1 < len f ; :: thesis: (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part>_of f,i1,i2
A4: len (mid (f,1,i2)) = len (f | i2) by A1, FINSEQ_6:116
.= i2 by A2, A3, FINSEQ_1:59, XXREAL_0:2 ;
A5: 1 <= i1 by A1, A2, XXREAL_0:2;
len f < (len f) + 1 by NAT_1:13;
then (len f) - 1 < ((len f) + 1) - 1 by XREAL_1:9;
then A6: (len f) -' 1 < len f by A3, A5, XREAL_1:233, XXREAL_0:2;
A7: i1 + 1 <= len f by A3, NAT_1:13;
then (i1 + 1) - 1 <= (len f) - 1 by XREAL_1:9;
then A8: i1 <= (len f) -' 1 by A3, A5, XREAL_1:233, XXREAL_0:2;
then A9: 1 <= (len f) -' 1 by A5, XXREAL_0:2;
then len (mid (f,i1,((len f) -' 1))) = (((len f) -' 1) -' i1) + 1 by A3, A5, A8, A6, FINSEQ_6:118
.= (((len f) -' 1) - i1) + 1 by A8, XREAL_1:233
.= (((len f) - 1) - i1) + 1 by A3, A5, XREAL_1:233, XXREAL_0:2
.= (len f) - i1 ;
then A10: len ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) = ((len f) - i1) + i2 by A4, FINSEQ_1:22
.= (len f) - (i1 - i2) ;
A11: i2 < len f by A2, A3, XXREAL_0:2;
then A12: i2 + 1 <= len f by NAT_1:13;
then (i2 + 1) - 1 <= (len f) - 1 by XREAL_1:9;
then A13: i2 <= (len f) -' 1 by A3, A5, XREAL_1:233, XXREAL_0:2;
A14: for i being Nat st 1 <= i & i <= len ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) holds
((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f))

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) implies ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f)) )
assume that
A15: 1 <= i and
A16: i <= len ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) ; :: thesis: ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f))
A17: (i1 + i) -' 1 = (i1 + i) - 1 by A15, NAT_D:37;
A18: (len f) - i1 = (len f) -' i1 by A3, XREAL_1:233;
A19: (((len f) -' 1) -' i1) + 1 = (((len f) -' 1) - i1) + 1 by A8, XREAL_1:233
.= (((len f) - 1) - i1) + 1 by A3, A5, XREAL_1:233, XXREAL_0:2
.= (len f) - i1 ;
A20: len (mid (f,i1,((len f) -' 1))) = (((len f) -' 1) -' i1) + 1 by A3, A5, A8, A9, A6, FINSEQ_6:118;

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

per cases ( i <= len (mid (f,i1,((len f) -' 1))) or i > len (mid (f,i1,((len f) -' 1))) ) ;

case A21: i <= len (mid (f,i1,((len f) -' 1))) ; :: thesis: ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f))

then i1 + i <= i1 + ((((len f) -' 1) -' i1) + 1) by A20, XREAL_1:6;
then i1 + i <= ((((len f) -' 1) - i1) + 1) + i1 by A8, XREAL_1:233;
then i1 + i <= ((len f) -' 1) + 1 ;
then i1 + i <= len f by A3, A5, XREAL_1:235, XXREAL_0:2;
then (i1 + i) -' 1 <= (len f) - 1 by A17, XREAL_1:9;
then A22: (i1 + i) -' 1 <= (len f) -' 1 by A3, A5, XREAL_1:233, XXREAL_0:2;
0 <= i - 1 by A15, XREAL_1:48;
then A23: 1 + 0 <= i1 + (i - 1) by A5, XREAL_1:7;
i in dom (mid (f,i1,((len f) -' 1))) by A15, A21, FINSEQ_3:25;
then A24: ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = (mid (f,i1,((len f) -' 1))) . i by FINSEQ_1:def 7;
(mid (f,i1,((len f) -' 1))) . i = f . ((i1 + i) -' 1) by A3, A5, A8, A9, A6, A15, A21, FINSEQ_6:118;
hence ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f)) by A17, A24, A23, A22, Th22; :: thesis: verum

end;

case A25: i > len (mid (f,i1,((len f) -' 1))) ; :: thesis: ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f))

then i >= ((len f) -' i1) + 1 by A20, A19, A18, NAT_1:13;
then A26: i - ((len f) -' i1) >= (((len f) -' i1) + 1) - ((len f) -' i1) by XREAL_1:9;
then A27: 1 <= i -' ((len f) -' i1) by NAT_D:39;
A28: (len f) - i1 = (len f) -' i1 by A3, XREAL_1:233;
i - ((len f) - i1) <= (((len f) - i1) + i2) - ((len f) - i1) by A10, A16, XREAL_1:9;
then A29: i -' ((len f) -' i1) <= i2 by A28, A26, NAT_D:39;
then A30: i -' ((len f) -' i1) <= (len f) -' 1 by A13, XXREAL_0:2;
((len f) -' 1) + (i -' ((len f) -' i1)) = ((len f) -' 1) + (i - ((len f) -' i1)) by A20, A19, A18, A25, XREAL_1:233
.= (((len f) -' 1) + i) - ((len f) -' i1)
.= (((len f) - 1) + i) - ((len f) -' i1) by A3, A5, XREAL_1:233, XXREAL_0:2
.= (((len f) - 1) + i) - ((len f) - i1) by A3, XREAL_1:233
.= (i + i1) - 1
.= (i1 + i) -' 1 by A15, NAT_D:37 ;
then A31: S_Drop (((i1 + i) -' 1),f) = S_Drop ((i -' ((len f) -' i1)),f) by Th23
.= i -' ((len f) -' i1) by A27, A30, Th22 ;
((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = (mid (f,1,i2)) . (i - (len (mid (f,i1,((len f) -' 1))))) by A16, A25, FINSEQ_6:108
.= (mid (f,1,i2)) . (i -' ((len f) -' i1)) by A20, A19, A18, A25, XREAL_1:233
.= f . (i -' ((len f) -' i1)) by A11, A27, A29, FINSEQ_6:123 ;
hence ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f)) by A31; :: thesis: verum

end;

end;

end;

hence ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . i = f . (S_Drop (((i1 + i) -' 1),f)) ; :: thesis: verum

end;

i1 - i2 > 0 by A2, XREAL_1:50;
then len f < (len f) + (i1 - i2) by XREAL_1:29;
then A32: (len f) - (i1 - i2) < ((len f) + (i1 - i2)) - (i1 - i2) by XREAL_1:9;
A33: len ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) = (len (mid (f,i1,((len f) -' 1)))) + (len (mid (f,1,i2))) by FINSEQ_1:22;
then len (mid (f,1,i2)) <= len ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) by NAT_1:11;
then A34: 1 <= len ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) by A1, A4, XXREAL_0:2;
len (mid (f,i1,((len f) -' 1))) < (len (mid (f,i1,((len f) -' 1)))) + (len (mid (f,1,i2))) by A1, A4, XREAL_1:29;
then ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2))) . (len ((mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)))) = (mid (f,1,i2)) . (((len (mid (f,i1,((len f) -' 1)))) + (len (mid (f,1,i2)))) - (len (mid (f,i1,((len f) -' 1))))) by A33, FINSEQ_6:108
.= f . i2 by A1, A11, FINSEQ_6:188 ;
hence (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) is_a_part>_of f,i1,i2 by A1, A5, A12, A7, A34, A10, A32, A14; :: thesis: verum