let i, j be Nat; for D being non empty set
for f being FinSequence of D st i in dom f & j in dom f holds
(mid (f,i,j)) /. 1 = f /. i
let D be non empty set ; for f being FinSequence of D st i in dom f & j in dom f holds
(mid (f,i,j)) /. 1 = f /. i
let f be FinSequence of D; ( i in dom f & j in dom f implies (mid (f,i,j)) /. 1 = f /. i )
assume A1:
i in dom f
; ( not j in dom f or (mid (f,i,j)) /. 1 = f /. i )
then A2:
1 <= i
by FINSEQ_3:25;
A3:
i <= len f
by A1, FINSEQ_3:25;
assume A4:
j in dom f
; (mid (f,i,j)) /. 1 = f /. i
then A5:
1 <= j
by FINSEQ_3:25;
A6:
j <= len f
by A4, FINSEQ_3:25;
not mid (f,i,j) is empty
by A1, A4, Lm9;
then
1 in dom (mid (f,i,j))
by FINSEQ_5:6;
hence (mid (f,i,j)) /. 1 =
(mid (f,i,j)) . 1
by PARTFUN1:def 6
.=
f . i
by A2, A3, A5, A6, FINSEQ_6:118
.=
f /. i
by A1, PARTFUN1:def 6
;
verum