let i, j, k be Nat; 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 ; 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; ( 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))
; (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
; verum