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 & len (mid (f,i,j)) = 1 holds
i = j
let D be non empty set ; :: thesis: for f being FinSequence of D st i in dom f & j in dom f & len (mid (f,i,j)) = 1 holds
i = j
let f be FinSequence of D; :: thesis: ( i in dom f & j in dom f & len (mid (f,i,j)) = 1 implies i = j )
assume A1: i in dom f ; :: thesis: ( not j in dom f or not len (mid (f,i,j)) = 1 or i = j )
then A2: 1 <= i by FINSEQ_3:25;
A3: i <= len f by A1, FINSEQ_3:25;
assume A4: j in dom f ; :: thesis: ( not len (mid (f,i,j)) = 1 or i = j )
then A5: 1 <= j by FINSEQ_3:25;
A6: j <= len f by A4, FINSEQ_3:25;
assume A7: len (mid (f,i,j)) = 1 ; :: thesis: i = j

per cases ( i <= j or i >= j ) ;

suppose A8: i <= j ; :: thesis: i = j

then 0 + 1 = (j -' i) + 1 by A2, A6, A7, FINSEQ_6:186;
then 0 = j - i by A8, XREAL_1:233;
hence i = j ; :: thesis: verum

end;

suppose A9: i >= j ; :: thesis: i = j

then 0 + 1 = (i -' j) + 1 by A3, A5, A7, FINSEQ_6:187;
then 0 = i - j by A9, XREAL_1:233;
hence i = j ; :: thesis: verum

end;

end;