let i, j, k be Element of 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:27;
A6: ( 1 <= k & k <= len (mid f,i,j) ) by A4, FINSEQ_3:27;
A7: ( 1 <= j & j <= len f ) by A3, FINSEQ_3:27;
thus (mid f,i,j) /. k = (mid f,i,j) . k by A4, PARTFUN1:def 8
.= f . ((k + i) -' 1) by A1, A5, A7, A6, FINSEQ_6:124
.= f /. ((k + i) -' 1) by A1, A2, A3, A4, Th5, PARTFUN1:def 8 ; :: thesis: verum