let i be Element of 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 A1: ( 1 <= i & i < len f ) ; :: thesis: (mid f,i,((len f) -' 1)) ^ <*(f /. (len f))*> = mid f,i,(len f)
then A2: i + 1 <= len f by NAT_1:13;
then A3: (i + 1) - 1 <= (len f) - 1 by XREAL_1:11;
then A4: 0 + i <= (len f) - 1 ;
A5: i <= (len f) -' 1 by A3, XREAL_0:def 2;
len f <= (len f) + 1 by NAT_1:11;
then (len f) - 1 <= ((len f) + 1) - 1 by XREAL_1:11;
then A6: (len f) -' 1 <= len f by XREAL_0:def 2;
A7: (len f) - i >= 0 by A2, XREAL_1:21;
((len f) - 1) - i >= 0 by A4, XREAL_1:21;
then A8: ((len f) -' 1) - i >= 0 by A3, XREAL_0:def 2;
A9: len ((mid f,i,((len f) -' 1)) ^ <*(f /. (len f))*>) = (len (mid f,i,((len f) -' 1))) + 1 by FINSEQ_2:19;
A10: (len (mid f,i,((len f) -' 1))) + 1 = ((((len f) -' 1) -' i) + 1) + 1 by A1, A5, A6, JORDAN4:20
.= ((((len f) -' 1) - i) + 1) + 1 by A8, XREAL_0:def 2
.= ((((len f) - 1) - i) + 1) + 1 by A3, XREAL_0:def 2
.= ((len f) -' i) + 1 by A7, XREAL_0:def 2
.= len (mid f,i,(len f)) by A1, JORDAN4:20 ;

now

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 A11: ( 1 <= j & j <= len (mid f,i,(len f)) ) ; :: thesis: ((mid f,i,((len f) -' 1)) ^ <*(f /. (len f))*>) /. b₁ = (mid f,i,(len f)) /. b₁
1 < len f by A1, XXREAL_0:2;
then ( i in Seg (len f) & len f in Seg (len f) ) by A1, FINSEQ_1:3;
then A12: ( i in dom f & len f in dom f ) by FINSEQ_1:def 3;

per cases ( j < len (mid f,i,(len f)) or j = len (mid f,i,(len f)) ) by A11, 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 A13: j <= len (mid f,i,((len f) -' 1)) by A10, NAT_1:13;
then j in Seg (len (mid f,i,((len f) -' 1))) by A11, FINSEQ_1:3;
then A14: j in dom (mid f,i,((len f) -' 1)) by FINSEQ_1:def 3;
j in Seg (len (mid f,i,(len f))) by A11, FINSEQ_1:3;
then A15: j in dom (mid f,i,(len f)) by FINSEQ_1:def 3;
1 <= (len f) -' 1 by A1, A5, XXREAL_0:2;
then (len f) -' 1 in Seg (len f) by A6, FINSEQ_1:3;
then A16: (len f) -' 1 in dom f by FINSEQ_1:def 3;
j in NAT by ORDINAL1:def 13;
hence ((mid f,i,((len f) -' 1)) ^ <*(f /. (len f))*>) /. j = (mid f,i,((len f) -' 1)) /. j by A11, A13, BOOLMARK:8
.= f /. ((j + i) -' 1) by A5, A12, A14, A16, SPRECT_2:7
.= (mid f,i,(len f)) /. j by A1, A12, A15, SPRECT_2:7 ;
:: thesis: verum

end;

suppose A17: 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 A10, FINSEQ_4:82
.= (mid f,i,(len f)) /. j by A12, A17, SPRECT_2:13 ;
:: thesis: verum

end;

end;

end;

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