let f be FinSequence of (TOP-REAL 2); :: thesis: for i1, i2, i being Element of NAT st 1 <= i1 & i1 < i2 & i2 <= len f & 1 <= i & i < (i2 -' i1) + 1 holds
LSeg (mid f,i2,i1),i = LSeg f,(i2 -' i)
let i1, i2, i be Element of NAT ; :: thesis: ( 1 <= i1 & i1 < i2 & i2 <= len f & 1 <= i & i < (i2 -' i1) + 1 implies LSeg (mid f,i2,i1),i = LSeg f,(i2 -' i) )
assume that
A1: 1 <= i1 and
A2: i1 < i2 and
A3: i2 <= len f and
A4: 1 <= i and
A5: i < (i2 -' i1) + 1 ; :: thesis: LSeg (mid f,i2,i1),i = LSeg f,(i2 -' i)
A6: len (mid f,i2,i1) = (i2 -' i1) + 1 by A1, A2, A3, Th21;
i < len (mid f,i2,i1) by A1, A2, A3, A5, Th21;
then i + 1 <= len (mid f,i2,i1) by NAT_1:13;
then A7: (i + 1) - i <= (len (mid f,i2,i1)) - i by XREAL_1:11;
then A8: 1 <= (len (mid f,i2,i1)) -' i by NAT_D:39;
i2 <= i2 + (i1 -' 1) by NAT_1:11;
then i2 <= i2 + (i1 - 1) by A1, XREAL_1:235;
then i2 - (i1 - 1) <= (i2 + (i1 - 1)) - (i1 - 1) by XREAL_1:11;
then (i2 - i1) + 1 <= i2 ;
then A9: (i2 -' i1) + 1 <= i2 by A2, XREAL_1:235;
A10: ((((i2 -' i1) + 1) -' i) + i1) -' 1 = ((((i2 -' i1) + 1) -' i) + i1) - 1 by A1, NAT_D:37
.= ((((i2 -' i1) + 1) - i) + i1) - 1 by A5, XREAL_1:235
.= ((i2 -' i1) - i) + i1
.= ((i2 - i1) - i) + i1 by A2, XREAL_1:235
.= i2 - i
.= i2 -' i by A5, A9, XREAL_1:235, XXREAL_0:2 ;
(len (mid f,i2,i1)) + 1 <= (len (mid f,i2,i1)) + i by A4, XREAL_1:8;
then len (mid f,i2,i1) < (len (mid f,i2,i1)) + i by NAT_1:13;
then (len (mid f,i2,i1)) - i < ((len (mid f,i2,i1)) + i) - i by XREAL_1:11;
then A11: (len (mid f,i2,i1)) -' i < (i2 -' i1) + 1 by A6, A7, NAT_D:39;
i + ((len (mid f,i2,i1)) -' i) = len (mid f,i2,i1) by A5, A6, XREAL_1:237;
hence LSeg (mid f,i2,i1),i = LSeg (Rev (mid f,i2,i1)),((len (mid f,i2,i1)) -' i) by SPPOL_2:2
.= LSeg (mid f,i1,i2),((len (mid f,i2,i1)) -' i) by Th30
.= LSeg f,((((len (mid f,i2,i1)) -' i) + i1) -' 1) by A1, A2, A3, A8, A11, Th31
.= LSeg f,(i2 -' i) by A1, A2, A3, A10, Th21 ;
:: thesis: verum