let f be non constant standard special_circular_sequence; :: thesis: for i1, i2 being Element of 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 Element of 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, JORDAN3:25
.= i2 by A2, A3, FINSEQ_1:80, 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:11;
then A6: (len f) -' 1 < len f by A3, A5, XREAL_1:235, XXREAL_0:2;
A7: i1 + 1 <= len f by A3, NAT_1:13;
then (i1 + 1) - 1 <= (len f) - 1 by XREAL_1:11;
then A8: i1 <= (len f) -' 1 by A3, A5, XREAL_1:235, 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, JORDAN3:27
.= (((len f) -' 1) - i1) + 1 by A8, XREAL_1:235
.= (((len f) - 1) - i1) + 1 by A3, A5, XREAL_1:235, 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:35
.= (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:11;
then A13: i2 <= (len f) -' 1 by A3, A5, XREAL_1:235, 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:235;
A19: (((len f) -' 1) -' i1) + 1 = (((len f) -' 1) - i1) + 1 by A8, XREAL_1:235
.= (((len f) - 1) - i1) + 1 by A3, A5, XREAL_1:235, 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, JORDAN3:27;
A21: i in NAT by ORDINAL1:def 13;

now

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

case A22: 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:8;
then i1 + i <= ((((len f) -' 1) - i1) + 1) + i1 by A8, XREAL_1:235;
then i1 + i <= ((len f) -' 1) + 1 ;
then i1 + i <= len f by A3, A5, XREAL_1:237, XXREAL_0:2;
then (i1 + i) -' 1 <= (len f) - 1 by A17, XREAL_1:11;
then A23: (i1 + i) -' 1 <= (len f) -' 1 by A3, A5, XREAL_1:235, XXREAL_0:2;
0 <= i - 1 by A15, XREAL_1:50;
then A24: 1 + 0 <= i1 + (i - 1) by A5, XREAL_1:9;
i in dom (mid f,i1,((len f) -' 1)) by A15, A22, FINSEQ_3:27;
then A25: ((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, A22, JORDAN3:27;
hence ((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2)) . i = f . (S_Drop ((i1 + i) -' 1),f) by A17, A25, A24, A23, Th34; :: thesis: verum

end;

case A26: 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 A27: i - ((len f) -' i1) >= (((len f) -' i1) + 1) - ((len f) -' i1) by XREAL_1:11;
then A28: 1 <= i -' ((len f) -' i1) by NAT_D:39;
A29: (len f) - i1 = (len f) -' i1 by A3, XREAL_1:235;
i - ((len f) - i1) <= (((len f) - i1) + i2) - ((len f) - i1) by A10, A16, XREAL_1:11;
then A30: i -' ((len f) -' i1) <= i2 by A29, A27, NAT_D:39;
then A31: 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, A26, XREAL_1:235
.= (((len f) -' 1) + i) - ((len f) -' i1)
.= (((len f) - 1) + i) - ((len f) -' i1) by A3, A5, XREAL_1:235, XXREAL_0:2
.= (((len f) - 1) + i) - ((len f) - i1) by A3, XREAL_1:235
.= (i + i1) - 1
.= (i1 + i) -' 1 by A15, NAT_D:37 ;
then A32: S_Drop ((i1 + i) -' 1),f = S_Drop (i -' ((len f) -' i1)),f by Th35
.= i -' ((len f) -' i1) by A28, A31, Th34 ;
((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, A26, JORDAN3:15
.= (mid f,1,i2) . (i -' ((len f) -' i1)) by A20, A19, A18, A26, XREAL_1:235
.= f . (i -' ((len f) -' i1)) by A11, A28, A30, JORDAN3:32 ;
hence ((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2)) . i = f . (S_Drop ((i1 + i) -' 1),f) by A32; :: 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:52;
then len f < (len f) + (i1 - i2) by XREAL_1:31;
then A33: (len f) - (i1 - i2) < ((len f) + (i1 - i2)) - (i1 - i2) by XREAL_1:11;
A34: 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:35;
then len (mid f,1,i2) <= len ((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2)) by NAT_1:11;
then A35: 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:31;
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 A34, JORDAN3:15
.= f . i2 by A1, A11, Th22 ;
hence (mid f,i1,((len f) -' 1)) ^ (mid f,1,i2) is_a_part>_of f,i1,i2 by A1, A5, A12, A7, A35, A10, A33, A14, Def2; :: thesis: verum