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 ;
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