let i, j, k be Nat; :: thesis: for D being non empty set
for f being FinSequence of D st i <= j & i in dom f & j in dom f & k in dom (mid (f,i,j)) holds
(mid (f,i,j)) /. k = f /. ((k + i) -' 1)
let D be non empty set ; :: thesis: for f being FinSequence of D st i <= j & i in dom f & j in dom f & k in dom (mid (f,i,j)) holds
(mid (f,i,j)) /. k = f /. ((k + i) -' 1)
let f be FinSequence of D; :: thesis: ( i <= j & i in dom f & j in dom f & k in dom (mid (f,i,j)) implies (mid (f,i,j)) /. k = f /. ((k + i) -' 1) )
assume that
A1: i <= j and
A2: i in dom f and
A3: j in dom f and
A4: k in dom (mid (f,i,j)) ; :: thesis: (mid (f,i,j)) /. k = f /. ((k + i) -' 1)
A5: ( 1 <= i & i <= len f ) by A2, FINSEQ_3:25;
A6: ( 1 <= k & k <= len (mid (f,i,j)) ) by A4, FINSEQ_3:25;
A7: ( 1 <= j & j <= len f ) by A3, FINSEQ_3:25;
thus (mid (f,i,j)) /. k = (mid (f,i,j)) . k by A4, PARTFUN1:def 6
.= f . ((k + i) -' 1) by A1, A5, A7, A6, FINSEQ_6:118
.= f /. ((k + i) -' 1) by A1, A2, A3, A4, Th1, PARTFUN1:def 6 ; :: thesis: verum