let i, j be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: ( i in dom f & j in dom f implies (mid (f,i,j)) /. 1 = f /. i )
assume A1: i in dom f ; :: thesis: ( not j in dom f or (mid (f,i,j)) /. 1 = f /. i )
then A2: ( 1 <= i & i <= len f ) by FINSEQ_3:25;
assume A3: j in dom f ; :: thesis: (mid (f,i,j)) /. 1 = f /. i
then A4: ( 1 <= j & j <= len f ) by FINSEQ_3:25;
not mid (f,i,j) is empty by A1, A3, Th7;
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, A4, FINSEQ_6:118
.= f /. i by A1, PARTFUN1:def 6 ;
:: thesis: verum