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 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:11;
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:21;
then A6: ((len f) -' 1) - i >= 0 by A4, XREAL_0:def 2;
A7: (len f) - i >= 0 by A3, XREAL_1:21;
len f <= (len f) + 1 by NAT_1:11;
then (len f) - 1 <= ((len f) + 1) - 1 by XREAL_1:11;
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:20
.= ((((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:20 ;

A10: now

1 < len f by A1, A2, XXREAL_0:2;
then len f in Seg (len f) by FINSEQ_1:3;
then A11: len f in dom f by FINSEQ_1:def 3;
i in Seg (len f) by A1, A2, FINSEQ_1:3;
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:3;
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:3;
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:3;
then A18: j in dom (mid f,i,(len 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 A13, A15, BOOLMARK:8
.= f /. ((j + i) -' 1) by A5, A12, A16, A17, SPRECT_2:7
.= (mid f,i,(len f)) /. j by A2, A12, A11, A18, SPRECT_2:7 ;
:: 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:82
.= (mid f,i,(len f)) /. j by A12, A11, A19, SPRECT_2:13 ;
:: 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:19;
hence (mid f,i,((len f) -' 1)) ^ <*(f /. (len f))*> = mid f,i,(len f) by A9, A10, FINSEQ_5:14; :: thesis: verum