let i, j be Element of 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) /. (len (mid f,i,j)) = f /. j
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) /. (len (mid f,i,j)) = f /. j
let f be FinSequence of D; :: thesis: ( i in dom f & j in dom f implies (mid f,i,j) /. (len (mid f,i,j)) = f /. j )
assume A1: i in dom f ; :: thesis: ( not j in dom f or (mid f,i,j) /. (len (mid f,i,j)) = f /. j )
then A2: ( 1 <= i & i <= len f ) by FINSEQ_3:27;
assume A3: j in dom f ; :: thesis: (mid f,i,j) /. (len (mid f,i,j)) = f /. j
then A4: ( 1 <= j & j <= len f ) by FINSEQ_3:27;
not mid f,i,j is empty by A1, A3, Th11;
then len (mid f,i,j) in dom (mid f,i,j) by FINSEQ_5:6;
hence (mid f,i,j) /. (len (mid f,i,j)) = (mid f,i,j) . (len (mid f,i,j)) by PARTFUN1:def 8
.= f . j by A2, A4, JORDAN4:23
.= f /. j by A3, PARTFUN1:def 8 ;
:: thesis: verum