let i be Nat; :: thesis: for D being non empty set

for f being FinSequence of D st 1 <= i & i < len f holds

(mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*> = mid (f,i,(len f))

let D be non empty set ; :: thesis: for f being FinSequence of D st 1 <= i & i < len f holds

(mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*> = mid (f,i,(len f))

let f be FinSequence of D; :: thesis: ( 1 <= i & i < len f implies (mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*> = mid (f,i,(len f)) )

assume that

A1: 1 <= i and

A2: i < len f ; :: thesis: (mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*> = mid (f,i,(len f))

A3: i + 1 <= len f by A2, NAT_1:13;

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

then A5: i <= (len f) -' 1 by XREAL_0:def 2;

0 + i <= (len f) - 1 by A4;

then ((len f) - 1) - i >= 0 by XREAL_1:19;

then A6: ((len f) -' 1) - i >= 0 by A4, XREAL_0:def 2;

A7: (len f) - i >= 0 by A3, XREAL_1:19;

len f <= (len f) + 1 by NAT_1:11;

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

then A8: (len f) -' 1 <= len f by XREAL_0:def 2;

then A9: (len (mid (f,i,((len f) -' 1)))) + 1 = ((((len f) -' 1) -' i) + 1) + 1 by A1, A5, JORDAN4:8

.= ((((len f) -' 1) - i) + 1) + 1 by A6, XREAL_0:def 2

.= ((((len f) - 1) - i) + 1) + 1 by A4, XREAL_0:def 2

.= ((len f) -' i) + 1 by A7, XREAL_0:def 2

.= len (mid (f,i,(len f))) by A1, A2, JORDAN4:8 ;

hence (mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*> = mid (f,i,(len f)) by A9, A10, FINSEQ_5:13; :: thesis: verum

for f being FinSequence of D st 1 <= i & i < len f holds

(mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*> = mid (f,i,(len f))

let D be non empty set ; :: thesis: for f being FinSequence of D st 1 <= i & i < len f holds

(mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*> = mid (f,i,(len f))

let f be FinSequence of D; :: thesis: ( 1 <= i & i < len f implies (mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*> = mid (f,i,(len f)) )

assume that

A1: 1 <= i and

A2: i < len f ; :: thesis: (mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*> = mid (f,i,(len f))

A3: i + 1 <= len f by A2, NAT_1:13;

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

then A5: i <= (len f) -' 1 by XREAL_0:def 2;

0 + i <= (len f) - 1 by A4;

then ((len f) - 1) - i >= 0 by XREAL_1:19;

then A6: ((len f) -' 1) - i >= 0 by A4, XREAL_0:def 2;

A7: (len f) - i >= 0 by A3, XREAL_1:19;

len f <= (len f) + 1 by NAT_1:11;

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

then A8: (len f) -' 1 <= len f by XREAL_0:def 2;

then A9: (len (mid (f,i,((len f) -' 1)))) + 1 = ((((len f) -' 1) -' i) + 1) + 1 by A1, A5, JORDAN4:8

.= ((((len f) -' 1) - i) + 1) + 1 by A6, XREAL_0:def 2

.= ((((len f) - 1) - i) + 1) + 1 by A4, XREAL_0:def 2

.= ((len f) -' i) + 1 by A7, XREAL_0:def 2

.= len (mid (f,i,(len f))) by A1, A2, JORDAN4:8 ;

A10: now :: thesis: for j being Nat st 1 <= j & j <= len (mid (f,i,(len f))) holds

((mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*>) /. j = (mid (f,i,(len f))) /. j

len ((mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*>) = (len (mid (f,i,((len f) -' 1)))) + 1
by FINSEQ_2:16;((mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*>) /. j = (mid (f,i,(len f))) /. j

1 < len f
by A1, A2, XXREAL_0:2;

then len f in Seg (len f) by FINSEQ_1:1;

then A11: len f in dom f by FINSEQ_1:def 3;

i in Seg (len f) by A1, A2, FINSEQ_1:1;

then A12: i in dom f by FINSEQ_1:def 3;

let j be Nat; :: thesis: ( 1 <= j & j <= len (mid (f,i,(len f))) implies ((mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*>) /. b_{1} = (mid (f,i,(len f))) /. b_{1} )

assume that

A13: 1 <= j and

A14: j <= len (mid (f,i,(len f))) ; :: thesis: ((mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*>) /. b_{1} = (mid (f,i,(len f))) /. b_{1}

end;then len f in Seg (len f) by FINSEQ_1:1;

then A11: len f in dom f by FINSEQ_1:def 3;

i in Seg (len f) by A1, A2, FINSEQ_1:1;

then A12: i in dom f by FINSEQ_1:def 3;

let j be Nat; :: thesis: ( 1 <= j & j <= len (mid (f,i,(len f))) implies ((mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*>) /. b

assume that

A13: 1 <= j and

A14: j <= len (mid (f,i,(len f))) ; :: thesis: ((mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*>) /. b

per cases
( j < len (mid (f,i,(len f))) or j = len (mid (f,i,(len f))) )
by A14, XXREAL_0:1;

end;

suppose
j < len (mid (f,i,(len f)))
; :: thesis: ((mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*>) /. b_{1} = (mid (f,i,(len f))) /. b_{1}

then A15:
j <= len (mid (f,i,((len f) -' 1)))
by A9, NAT_1:13;

then j in Seg (len (mid (f,i,((len f) -' 1)))) by A13, FINSEQ_1:1;

then A16: j in dom (mid (f,i,((len f) -' 1))) by FINSEQ_1:def 3;

1 <= (len f) -' 1 by A1, A5, XXREAL_0:2;

then (len f) -' 1 in Seg (len f) by A8, FINSEQ_1:1;

then A17: (len f) -' 1 in dom f by FINSEQ_1:def 3;

j in Seg (len (mid (f,i,(len f)))) by A13, A14, FINSEQ_1:1;

then A18: j in dom (mid (f,i,(len f))) by FINSEQ_1:def 3;

j in NAT by ORDINAL1:def 12;

hence ((mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*>) /. j = (mid (f,i,((len f) -' 1))) /. j by A13, A15, BOOLMARK:7

.= f /. ((j + i) -' 1) by A5, A12, A16, A17, SPRECT_2:3

.= (mid (f,i,(len f))) /. j by A2, A12, A11, A18, SPRECT_2:3 ;

:: thesis: verum

end;then j in Seg (len (mid (f,i,((len f) -' 1)))) by A13, FINSEQ_1:1;

then A16: j in dom (mid (f,i,((len f) -' 1))) by FINSEQ_1:def 3;

1 <= (len f) -' 1 by A1, A5, XXREAL_0:2;

then (len f) -' 1 in Seg (len f) by A8, FINSEQ_1:1;

then A17: (len f) -' 1 in dom f by FINSEQ_1:def 3;

j in Seg (len (mid (f,i,(len f)))) by A13, A14, FINSEQ_1:1;

then A18: j in dom (mid (f,i,(len f))) by FINSEQ_1:def 3;

j in NAT by ORDINAL1:def 12;

hence ((mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*>) /. j = (mid (f,i,((len f) -' 1))) /. j by A13, A15, BOOLMARK:7

.= f /. ((j + i) -' 1) by A5, A12, A16, A17, SPRECT_2:3

.= (mid (f,i,(len f))) /. j by A2, A12, A11, A18, SPRECT_2:3 ;

:: thesis: verum

suppose A19:
j = len (mid (f,i,(len f)))
; :: thesis: ((mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*>) /. b_{1} = (mid (f,i,(len f))) /. b_{1}

hence ((mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*>) /. j =
f /. (len f)
by A9, FINSEQ_4:67

.= (mid (f,i,(len f))) /. j by A12, A11, A19, SPRECT_2:9 ;

:: thesis: verum

end;.= (mid (f,i,(len f))) /. j by A12, A11, A19, SPRECT_2:9 ;

:: thesis: verum

hence (mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*> = mid (f,i,(len f)) by A9, A10, FINSEQ_5:13; :: thesis: verum