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, FINSEQ_6:186
.= ((((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, FINSEQ_6:186 ;

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

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₁ = (mid (f,i,(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₁ = (mid (f,i,(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;

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

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;

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

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;

end;

end;

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