let f be FinSequence; :: thesis: for k1, k2 being Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds

( (mid (f,k1,k2)) . 1 = f . k1 & ( k1 <= k2 implies ( len (mid (f,k1,k2)) = (k2 -' k1) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k1,k2)) holds

(mid (f,k1,k2)) . i = f . ((i + k1) -' 1) ) ) ) & ( k1 > k2 implies ( len (mid (f,k1,k2)) = (k1 -' k2) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k1,k2)) holds

(mid (f,k1,k2)) . i = f . ((k1 -' i) + 1) ) ) ) )

let k11, k21 be Nat; :: thesis: ( 1 <= k11 & k11 <= len f & 1 <= k21 & k21 <= len f implies ( (mid (f,k11,k21)) . 1 = f . k11 & ( k11 <= k21 implies ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) ) & ( k11 > k21 implies ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) ) ) ) )

assume that

A1: 1 <= k11 and

A2: k11 <= len f and

A3: 1 <= k21 and

A4: k21 <= len f ; :: thesis: ( (mid (f,k11,k21)) . 1 = f . k11 & ( k11 <= k21 implies ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) ) & ( k11 > k21 implies ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) ) ) )

reconsider fa = f as FinSequence of rng f by FINSEQ_1:def 4;

k21 -' 1 <= len f by A4, NAT_D:44;

then A5: len (f /^ (k21 -' 1)) = (len f) - (k21 -' 1) by RFINSEQ:def 1;

A6: k21 - 1 >= 0 by A3, XREAL_1:48;

then A7: k21 -' 1 = k21 - 1 by XREAL_0:def 2;

(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) ) & ( k11 > k21 implies ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) ) ) )

(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) ) :: thesis: ( k11 > k21 implies ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) ) )

(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) )

then A44: k11 - k21 >= 0 by XREAL_1:48;

then A45: k11 -' k21 = k11 - k21 by XREAL_0:def 2;

A46: mid (f,k11,k21) = Rev ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) by A43, Def3;

then A47: len (mid (f,k11,k21)) = len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) by FINSEQ_5:def 3;

(k11 -' k21) + 1 = (k11 - k21) + 1 by A44, XREAL_0:def 2

.= k11 - (k21 - 1)

.= k11 - (k21 -' 1) by A6, XREAL_0:def 2 ;

then A48: (k11 -' k21) + 1 <= len (f /^ (k21 -' 1)) by A2, A5, XREAL_1:9;

hence A49: len (mid (f,k11,k21)) = (k11 -' k21) + 1 by A47, FINSEQ_1:59; :: thesis: for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1)

A50: len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) = (k11 -' k21) + 1 by A48, FINSEQ_1:59;

thus for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) :: thesis: verum

( (mid (f,k1,k2)) . 1 = f . k1 & ( k1 <= k2 implies ( len (mid (f,k1,k2)) = (k2 -' k1) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k1,k2)) holds

(mid (f,k1,k2)) . i = f . ((i + k1) -' 1) ) ) ) & ( k1 > k2 implies ( len (mid (f,k1,k2)) = (k1 -' k2) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k1,k2)) holds

(mid (f,k1,k2)) . i = f . ((k1 -' i) + 1) ) ) ) )

let k11, k21 be Nat; :: thesis: ( 1 <= k11 & k11 <= len f & 1 <= k21 & k21 <= len f implies ( (mid (f,k11,k21)) . 1 = f . k11 & ( k11 <= k21 implies ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) ) & ( k11 > k21 implies ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) ) ) ) )

assume that

A1: 1 <= k11 and

A2: k11 <= len f and

A3: 1 <= k21 and

A4: k21 <= len f ; :: thesis: ( (mid (f,k11,k21)) . 1 = f . k11 & ( k11 <= k21 implies ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) ) & ( k11 > k21 implies ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) ) ) )

reconsider fa = f as FinSequence of rng f by FINSEQ_1:def 4;

k21 -' 1 <= len f by A4, NAT_D:44;

then A5: len (f /^ (k21 -' 1)) = (len f) - (k21 -' 1) by RFINSEQ:def 1;

A6: k21 - 1 >= 0 by A3, XREAL_1:48;

then A7: k21 -' 1 = k21 - 1 by XREAL_0:def 2;

A8: now :: thesis: for k1, k2 being Nat st k1 <= k2 & 1 <= k1 & k1 <= len f holds

(mid (f,k1,k2)) . 1 = f . k1

thus
(mid (f,k11,k21)) . 1 = f . k11
:: thesis: ( ( k11 <= k21 implies ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds (mid (f,k1,k2)) . 1 = f . k1

let k1, k2 be Nat; :: thesis: ( k1 <= k2 & 1 <= k1 & k1 <= len f implies (mid (f,k1,k2)) . 1 = f . k1 )

end;now :: thesis: ( k1 <= k2 & 1 <= k1 & k1 <= len f implies (mid (f,k1,k2)) . 1 = f . k1 )

hence
( k1 <= k2 & 1 <= k1 & k1 <= len f implies (mid (f,k1,k2)) . 1 = f . k1 )
; :: thesis: verumassume that

A9: k1 <= k2 and

A10: 1 <= k1 and

A11: k1 <= len f ; :: thesis: (mid (f,k1,k2)) . 1 = f . k1

A12: (mid (f,k1,k2)) . 1 = ((f /^ (k1 -' 1)) | ((k2 -' k1) + 1)) . 1 by A9, Def3

.= ((f /^ (k1 -' 1)) | (Seg ((k2 -' k1) + 1))) . 1 ;

k1 - 1 >= 0 by A10, XREAL_1:48;

then A13: 1 + (k1 -' 1) = 1 + (k1 - 1) by XREAL_0:def 2

.= k1 ;

then 1 + (k1 -' 1) <= ((len f) - (k1 -' 1)) + (k1 -' 1) by A11;

then A14: 1 <= (len f) - (k1 -' 1) by XREAL_1:6;

A15: k1 -' 1 <= len f by A11, NAT_D:44;

then len (f /^ (k1 -' 1)) = (len f) - (k1 -' 1) by RFINSEQ:def 1;

then 1 in Seg (len (f /^ (k1 -' 1))) by A14;

then A16: 1 in dom (f /^ (k1 -' 1)) by FINSEQ_1:def 3;

0 + 1 <= (k2 -' k1) + 1 by XREAL_1:6;

then 1 in Seg ((k2 -' k1) + 1) ;

then 1 in (dom (f /^ (k1 -' 1))) /\ (Seg ((k2 -' k1) + 1)) by A16, XBOOLE_0:def 4;

then 1 in dom ((f /^ (k1 -' 1)) | (Seg ((k2 -' k1) + 1))) by RELAT_1:61;

then (mid (f,k1,k2)) . 1 = (f /^ (k1 -' 1)) . 1 by A12, FUNCT_1:47;

hence (mid (f,k1,k2)) . 1 = f . k1 by A13, A15, A16, RFINSEQ:def 1; :: thesis: verum

end;A9: k1 <= k2 and

A10: 1 <= k1 and

A11: k1 <= len f ; :: thesis: (mid (f,k1,k2)) . 1 = f . k1

A12: (mid (f,k1,k2)) . 1 = ((f /^ (k1 -' 1)) | ((k2 -' k1) + 1)) . 1 by A9, Def3

.= ((f /^ (k1 -' 1)) | (Seg ((k2 -' k1) + 1))) . 1 ;

k1 - 1 >= 0 by A10, XREAL_1:48;

then A13: 1 + (k1 -' 1) = 1 + (k1 - 1) by XREAL_0:def 2

.= k1 ;

then 1 + (k1 -' 1) <= ((len f) - (k1 -' 1)) + (k1 -' 1) by A11;

then A14: 1 <= (len f) - (k1 -' 1) by XREAL_1:6;

A15: k1 -' 1 <= len f by A11, NAT_D:44;

then len (f /^ (k1 -' 1)) = (len f) - (k1 -' 1) by RFINSEQ:def 1;

then 1 in Seg (len (f /^ (k1 -' 1))) by A14;

then A16: 1 in dom (f /^ (k1 -' 1)) by FINSEQ_1:def 3;

0 + 1 <= (k2 -' k1) + 1 by XREAL_1:6;

then 1 in Seg ((k2 -' k1) + 1) ;

then 1 in (dom (f /^ (k1 -' 1))) /\ (Seg ((k2 -' k1) + 1)) by A16, XBOOLE_0:def 4;

then 1 in dom ((f /^ (k1 -' 1)) | (Seg ((k2 -' k1) + 1))) by RELAT_1:61;

then (mid (f,k1,k2)) . 1 = (f /^ (k1 -' 1)) . 1 by A12, FUNCT_1:47;

hence (mid (f,k1,k2)) . 1 = f . k1 by A13, A15, A16, RFINSEQ:def 1; :: thesis: verum

(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) ) & ( k11 > k21 implies ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) ) ) )

proof
end;

thus
( k11 <= k21 implies ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds per cases
( k11 <= k21 or k11 > k21 )
;

end;

suppose A17:
k11 > k21
; :: thesis: (mid (f,k11,k21)) . 1 = f . k11

A18:
k21 - 1 >= 0
by A3, XREAL_1:48;

A19: k11 - k21 >= 0 by A17, XREAL_1:48;

then k11 -' k21 = k11 - k21 by XREAL_0:def 2;

then A20: (k21 -' 1) + ((k11 -' k21) + 1) = (k21 - 1) + (k11 - (k21 - 1)) by A18, XREAL_0:def 2

.= k11 ;

k21 -' 1 <= len f by A4, NAT_D:44;

then A21: len (f /^ (k21 -' 1)) = (len f) - (k21 -' 1) by RFINSEQ:def 1;

A22: 1 <= (k11 -' k21) + 1 by NAT_1:11;

(k11 -' k21) + 1 = (k11 - k21) + 1 by A19, XREAL_0:def 2

.= k11 - (k21 - 1)

.= k11 - (k21 -' 1) by A18, XREAL_0:def 2 ;

then A23: (k11 -' k21) + 1 <= len (f /^ (k21 -' 1)) by A2, A21, XREAL_1:9;

then A24: len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) = (k11 -' k21) + 1 by FINSEQ_1:59;

then A25: (k11 -' k21) + 1 in dom ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) by A22, FINSEQ_3:25;

a25: (k11 -' k21) + 1 in dom (f /^ (k21 -' 1)) by A23, FINSEQ_3:25, A22;

A26: (k11 -' k21) + 1 in dom (f /^ (k21 -' 1)) by A22, A23, FINSEQ_3:25;

A27: ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) = ((fa /^ (k21 -' 1)) | ((k11 -' k21) + 1)) /. ((k11 -' k21) + 1) by A22, A24, FINSEQ_4:15

.= (fa /^ (k21 -' 1)) /. ((k11 -' k21) + 1) by A25, FINSEQ_4:70

.= (f /^ (k21 -' 1)) . ((k11 -' k21) + 1) by a25, PARTFUN1:def 6

.= f . k11 by A20, A26, FINSEQ_5:27 ;

1 in dom ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) by A22, A24, FINSEQ_3:25;

then (Rev ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) . 1 = ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (((len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) - 1) + 1) by FINSEQ_5:58

.= f . k11 by A27 ;

hence (mid (f,k11,k21)) . 1 = f . k11 by A17, Def3; :: thesis: verum

end;A19: k11 - k21 >= 0 by A17, XREAL_1:48;

then k11 -' k21 = k11 - k21 by XREAL_0:def 2;

then A20: (k21 -' 1) + ((k11 -' k21) + 1) = (k21 - 1) + (k11 - (k21 - 1)) by A18, XREAL_0:def 2

.= k11 ;

k21 -' 1 <= len f by A4, NAT_D:44;

then A21: len (f /^ (k21 -' 1)) = (len f) - (k21 -' 1) by RFINSEQ:def 1;

A22: 1 <= (k11 -' k21) + 1 by NAT_1:11;

(k11 -' k21) + 1 = (k11 - k21) + 1 by A19, XREAL_0:def 2

.= k11 - (k21 - 1)

.= k11 - (k21 -' 1) by A18, XREAL_0:def 2 ;

then A23: (k11 -' k21) + 1 <= len (f /^ (k21 -' 1)) by A2, A21, XREAL_1:9;

then A24: len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) = (k11 -' k21) + 1 by FINSEQ_1:59;

then A25: (k11 -' k21) + 1 in dom ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) by A22, FINSEQ_3:25;

a25: (k11 -' k21) + 1 in dom (f /^ (k21 -' 1)) by A23, FINSEQ_3:25, A22;

A26: (k11 -' k21) + 1 in dom (f /^ (k21 -' 1)) by A22, A23, FINSEQ_3:25;

A27: ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) = ((fa /^ (k21 -' 1)) | ((k11 -' k21) + 1)) /. ((k11 -' k21) + 1) by A22, A24, FINSEQ_4:15

.= (fa /^ (k21 -' 1)) /. ((k11 -' k21) + 1) by A25, FINSEQ_4:70

.= (f /^ (k21 -' 1)) . ((k11 -' k21) + 1) by a25, PARTFUN1:def 6

.= f . k11 by A20, A26, FINSEQ_5:27 ;

1 in dom ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) by A22, A24, FINSEQ_3:25;

then (Rev ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) . 1 = ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (((len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) - 1) + 1) by FINSEQ_5:58

.= f . k11 by A27 ;

hence (mid (f,k11,k21)) . 1 = f . k11 by A17, Def3; :: thesis: verum

(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) ) :: thesis: ( k11 > k21 implies ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) ) )

proof

assume A43:
k11 > k21
; :: thesis: ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds
A28:
k11 - 1 >= 0
by A1, XREAL_1:48;

then A29: k11 -' 1 = k11 - 1 by XREAL_0:def 2;

k11 -' 1 <= len f by A2, NAT_D:44;

then A30: len (f /^ (k11 -' 1)) = (len f) - (k11 -' 1) by RFINSEQ:def 1;

assume A31: k11 <= k21 ; :: thesis: ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) )

then A32: mid (f,k11,k21) = (f /^ (k11 -' 1)) | ((k21 -' k11) + 1) by Def3;

A33: k21 - k11 >= 0 by A31, XREAL_1:48;

then A34: k21 -' k11 = k21 - k11 by XREAL_0:def 2;

(k21 -' k11) + 1 = (k21 - k11) + 1 by A33, XREAL_0:def 2

.= k21 - (k11 - 1)

.= k21 - (k11 -' 1) by A28, XREAL_0:def 2 ;

then A35: (k21 -' k11) + 1 <= len (f /^ (k11 -' 1)) by A4, A30, XREAL_1:9;

then A36: len ((f /^ (k11 -' 1)) | ((k21 -' k11) + 1)) = (k21 -' k11) + 1 by FINSEQ_1:59;

for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((i + k11) -' 1)

(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) by A32, A35, FINSEQ_1:59; :: thesis: verum

end;then A29: k11 -' 1 = k11 - 1 by XREAL_0:def 2;

k11 -' 1 <= len f by A2, NAT_D:44;

then A30: len (f /^ (k11 -' 1)) = (len f) - (k11 -' 1) by RFINSEQ:def 1;

assume A31: k11 <= k21 ; :: thesis: ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) )

then A32: mid (f,k11,k21) = (f /^ (k11 -' 1)) | ((k21 -' k11) + 1) by Def3;

A33: k21 - k11 >= 0 by A31, XREAL_1:48;

then A34: k21 -' k11 = k21 - k11 by XREAL_0:def 2;

(k21 -' k11) + 1 = (k21 - k11) + 1 by A33, XREAL_0:def 2

.= k21 - (k11 - 1)

.= k21 - (k11 -' 1) by A28, XREAL_0:def 2 ;

then A35: (k21 -' k11) + 1 <= len (f /^ (k11 -' 1)) by A4, A30, XREAL_1:9;

then A36: len ((f /^ (k11 -' 1)) | ((k21 -' k11) + 1)) = (k21 -' k11) + 1 by FINSEQ_1:59;

for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((i + k11) -' 1)

proof

hence
( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds
let i be Nat; :: thesis: ( 1 <= i & i <= len (mid (f,k11,k21)) implies (mid (f,k11,k21)) . i = f . ((i + k11) -' 1) )

assume that

A37: 1 <= i and

A38: i <= len (mid (f,k11,k21)) ; :: thesis: (mid (f,k11,k21)) . i = f . ((i + k11) -' 1)

A39: i <= (k21 -' k11) + 1 by A32, A35, A38, FINSEQ_1:59;

i + (k11 - 1) <= (k21 - (k11 - 1)) + (k11 - 1) by A32, A34, A36, A38, XREAL_1:6;

then A40: i + (k11 -' 1) <= len f by A4, A29, XXREAL_0:2;

A41: k11 <= k11 + i by NAT_1:11;

A42: i + (k11 -' 1) = i + (k11 - 1) by A28, XREAL_0:def 2

.= (i + k11) - 1

.= (i + k11) -' 1 by A1, A41, XREAL_1:233, XXREAL_0:2 ;

(mid (f,k11,k21)) . i = ((f /^ (k11 -' 1)) | ((k21 -' k11) + 1)) . i by A31, Def3

.= (f /^ (k11 -' 1)) . i by A39, FINSEQ_3:112

.= f . (i + (k11 -' 1)) by A37, A40, Th113 ;

hence (mid (f,k11,k21)) . i = f . ((i + k11) -' 1) by A42; :: thesis: verum

end;assume that

A37: 1 <= i and

A38: i <= len (mid (f,k11,k21)) ; :: thesis: (mid (f,k11,k21)) . i = f . ((i + k11) -' 1)

A39: i <= (k21 -' k11) + 1 by A32, A35, A38, FINSEQ_1:59;

i + (k11 - 1) <= (k21 - (k11 - 1)) + (k11 - 1) by A32, A34, A36, A38, XREAL_1:6;

then A40: i + (k11 -' 1) <= len f by A4, A29, XXREAL_0:2;

A41: k11 <= k11 + i by NAT_1:11;

A42: i + (k11 -' 1) = i + (k11 - 1) by A28, XREAL_0:def 2

.= (i + k11) - 1

.= (i + k11) -' 1 by A1, A41, XREAL_1:233, XXREAL_0:2 ;

(mid (f,k11,k21)) . i = ((f /^ (k11 -' 1)) | ((k21 -' k11) + 1)) . i by A31, Def3

.= (f /^ (k11 -' 1)) . i by A39, FINSEQ_3:112

.= f . (i + (k11 -' 1)) by A37, A40, Th113 ;

hence (mid (f,k11,k21)) . i = f . ((i + k11) -' 1) by A42; :: thesis: verum

(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) by A32, A35, FINSEQ_1:59; :: thesis: verum

(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) )

then A44: k11 - k21 >= 0 by XREAL_1:48;

then A45: k11 -' k21 = k11 - k21 by XREAL_0:def 2;

A46: mid (f,k11,k21) = Rev ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) by A43, Def3;

then A47: len (mid (f,k11,k21)) = len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) by FINSEQ_5:def 3;

(k11 -' k21) + 1 = (k11 - k21) + 1 by A44, XREAL_0:def 2

.= k11 - (k21 - 1)

.= k11 - (k21 -' 1) by A6, XREAL_0:def 2 ;

then A48: (k11 -' k21) + 1 <= len (f /^ (k21 -' 1)) by A2, A5, XREAL_1:9;

hence A49: len (mid (f,k11,k21)) = (k11 -' k21) + 1 by A47, FINSEQ_1:59; :: thesis: for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1)

A50: len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) = (k11 -' k21) + 1 by A48, FINSEQ_1:59;

thus for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds

(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) :: thesis: verum

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (mid (f,k11,k21)) implies (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) )

assume that

A51: 1 <= i and

A52: i <= len (mid (f,k11,k21)) ; :: thesis: (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1)

A53: i + (k21 - 1) <= (k11 - (k21 - 1)) + (k21 - 1) by A45, A49, A52, XREAL_1:6;

(k11 -' k21) + 1 <= ((k11 -' k21) + 1) + (i -' 1) by NAT_1:11;

then (k11 -' k21) + 1 <= ((k11 -' k21) + 1) + (i - 1) by A51, XREAL_1:233;

then ((k11 -' k21) + 1) - (i - 1) <= (((k11 -' k21) + 1) + (i - 1)) - (i - 1) by XREAL_1:9;

then A54: (((k11 -' k21) + 1) - i) + 1 <= (k11 -' k21) + 1 ;

i <= (k11 -' k21) + 1 by A47, A48, A52, FINSEQ_1:59;

then A55: (((k11 -' k21) + 1) -' i) + 1 <= (k11 -' k21) + 1 by A54, XREAL_1:233;

A56: i + k11 <= i + (len f) by A2, XREAL_1:6;

A57: i <= i + (k21 -' 1) by NAT_1:11;

A58: ((((k11 -' k21) + 1) -' i) + 1) + (k21 -' 1) = ((((k11 -' k21) + 1) - i) + 1) + (k21 -' 1) by A49, A52, XREAL_1:233

.= (((k11 - (k21 - 1)) - i) + 1) + (k21 - 1) by A6, A45, XREAL_0:def 2

.= (k11 - i) + 1

.= (k11 -' i) + 1 by A7, A53, A57, XREAL_1:233, XXREAL_0:2 ;

1 + k11 <= i + k11 by A51, XREAL_1:6;

then 1 + k11 <= i + (len f) by A56, XXREAL_0:2;

then (1 + k11) - i <= (i + (len f)) - i by XREAL_1:9;

then (k11 - i) + 1 <= len f ;

then A59: ((((k11 -' k21) + 1) -' i) + 1) + (k21 -' 1) <= len f by A7, A53, A57, A58, XREAL_1:233, XXREAL_0:2;

(mid (f,k11,k21)) . i = ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (((len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) - i) + 1) by A46, A47, A51, A52, Th114

.= ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (((len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) -' i) + 1) by A47, A52, XREAL_1:233

.= (f /^ (k21 -' 1)) . ((((k11 -' k21) + 1) -' i) + 1) by A50, A55, FINSEQ_3:112

.= f . ((k11 -' i) + 1) by A58, A59, Th113, NAT_1:11 ;

hence (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ; :: thesis: verum

end;assume that

A51: 1 <= i and

A52: i <= len (mid (f,k11,k21)) ; :: thesis: (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1)

A53: i + (k21 - 1) <= (k11 - (k21 - 1)) + (k21 - 1) by A45, A49, A52, XREAL_1:6;

(k11 -' k21) + 1 <= ((k11 -' k21) + 1) + (i -' 1) by NAT_1:11;

then (k11 -' k21) + 1 <= ((k11 -' k21) + 1) + (i - 1) by A51, XREAL_1:233;

then ((k11 -' k21) + 1) - (i - 1) <= (((k11 -' k21) + 1) + (i - 1)) - (i - 1) by XREAL_1:9;

then A54: (((k11 -' k21) + 1) - i) + 1 <= (k11 -' k21) + 1 ;

i <= (k11 -' k21) + 1 by A47, A48, A52, FINSEQ_1:59;

then A55: (((k11 -' k21) + 1) -' i) + 1 <= (k11 -' k21) + 1 by A54, XREAL_1:233;

A56: i + k11 <= i + (len f) by A2, XREAL_1:6;

A57: i <= i + (k21 -' 1) by NAT_1:11;

A58: ((((k11 -' k21) + 1) -' i) + 1) + (k21 -' 1) = ((((k11 -' k21) + 1) - i) + 1) + (k21 -' 1) by A49, A52, XREAL_1:233

.= (((k11 - (k21 - 1)) - i) + 1) + (k21 - 1) by A6, A45, XREAL_0:def 2

.= (k11 - i) + 1

.= (k11 -' i) + 1 by A7, A53, A57, XREAL_1:233, XXREAL_0:2 ;

1 + k11 <= i + k11 by A51, XREAL_1:6;

then 1 + k11 <= i + (len f) by A56, XXREAL_0:2;

then (1 + k11) - i <= (i + (len f)) - i by XREAL_1:9;

then (k11 - i) + 1 <= len f ;

then A59: ((((k11 -' k21) + 1) -' i) + 1) + (k21 -' 1) <= len f by A7, A53, A57, A58, XREAL_1:233, XXREAL_0:2;

(mid (f,k11,k21)) . i = ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (((len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) - i) + 1) by A46, A47, A51, A52, Th114

.= ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (((len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) -' i) + 1) by A47, A52, XREAL_1:233

.= (f /^ (k21 -' 1)) . ((((k11 -' k21) + 1) -' i) + 1) by A50, A55, FINSEQ_3:112

.= f . ((k11 -' i) + 1) by A58, A59, Th113, NAT_1:11 ;

hence (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ; :: thesis: verum