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 /. ((i -' k) + 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 /. ((i -' k) + 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 /. ((i -' k) + 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 /. ((i -' k) + 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 . ((i -' k) + 1) by A1, A5, A7, A6, JORDAN3:27
.= f /. ((i -' k) + 1) by A1, A2, A3, A4, Th6, PARTFUN1:def 8 ; :: thesis: verum