let f be V26() standard special_circular_sequence; for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 < len f holds
mid (f,i1,i2) is_a_part>_of f,i1,i2
let i1, i2 be Nat; ( 1 <= i1 & i1 <= i2 & i2 < len f implies mid (f,i1,i2) is_a_part>_of f,i1,i2 )
assume that
A1:
1 <= i1
and
A2:
i1 <= i2
and
A3:
i2 < len f
; mid (f,i1,i2) is_a_part>_of f,i1,i2
A4:
1 <= i2
by A1, A2, XXREAL_0:2;
A5:
i1 < len f
by A2, A3, XXREAL_0:2;
then A6:
len (mid (f,i1,i2)) = (i2 -' i1) + 1
by A1, A2, A3, A4, FINSEQ_6:118;
then A7:
1 <= len (mid (f,i1,i2))
by NAT_1:11;
A8:
i2 + 1 <= len f
by A3, NAT_1:13;
A9:
(i2 -' i1) + 1 = (i2 - i1) + 1
by A2, XREAL_1:233;
A10:
for i being Nat st 1 <= i & i <= len (mid (f,i1,i2)) holds
(mid (f,i1,i2)) . i = f . (S_Drop (((i1 + i) -' 1),f))
proof
let i be
Nat;
( 1 <= i & i <= len (mid (f,i1,i2)) implies (mid (f,i1,i2)) . i = f . (S_Drop (((i1 + i) -' 1),f)) )
assume that A11:
1
<= i
and A12:
i <= len (mid (f,i1,i2))
;
(mid (f,i1,i2)) . i = f . (S_Drop (((i1 + i) -' 1),f))
i + i1 <= ((i2 - i1) + 1) + i1
by A6, A9, A12, XREAL_1:6;
then
i1 + i <= len f
by A8, XXREAL_0:2;
then
(i1 + i) - 1
<= (len f) - 1
by XREAL_1:9;
then
(i1 + i) - 1
<= (len f) -' 1
by A3, A4, XREAL_1:233, XXREAL_0:2;
then A13:
(i1 + i) -' 1
<= (len f) -' 1
by A1, NAT_D:37;
1
+ 1
<= i1 + i
by A1, A11, XREAL_1:7;
then
(1 + 1) - 1
<= (i1 + i) - 1
by XREAL_1:9;
then
1
<= (i1 + i) -' 1
by A1, NAT_D:37;
then
S_Drop (
((i1 + i) -' 1),
f)
= (i1 + i) -' 1
by A13, Th22;
hence
(mid (f,i1,i2)) . i = f . (S_Drop (((i1 + i) -' 1),f))
by A1, A2, A3, A4, A5, A11, A12, FINSEQ_6:118;
verum
end;
A14:
(mid (f,i1,i2)) . (len (mid (f,i1,i2))) = f . i2
by A1, A2, A3, Th10;
A15:
i1 + 1 <= len f
by A5, NAT_1:13;
i2 + 1 < (i2 + 1) + i1
by A1, XREAL_1:29;
then
(i2 + 1) - i1 < ((i2 + 1) + i1) - i1
by XREAL_1:9;
then
len (mid (f,i1,i2)) < len f
by A8, A6, A9, XXREAL_0:2;
hence
mid (f,i1,i2) is_a_part>_of f,i1,i2
by A1, A4, A15, A8, A14, A7, A10; verum