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 by FINSEQ_3:25;

A3: i <= len f by A1, FINSEQ_3:25;

assume A4: j in dom f ; :: thesis: (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 ;

:: thesis: verum

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 by FINSEQ_3:25;

A3: i <= len f by A1, FINSEQ_3:25;

assume A4: j in dom f ; :: thesis: (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 ;

:: thesis: verum