let D be non empty set ; :: thesis: for f1 being FinSequence of D
for i1, i2 being Nat st 1 <= i2 & i2 <= i1 & i1 <= len f1 holds
len (mid (f1,i1,i2)) = (i1 -' i2) + 1
let f1 be FinSequence of D; :: thesis: for i1, i2 being Nat st 1 <= i2 & i2 <= i1 & i1 <= len f1 holds
len (mid (f1,i1,i2)) = (i1 -' i2) + 1
let i1, i2 be Nat; :: thesis: ( 1 <= i2 & i2 <= i1 & i1 <= len f1 implies len (mid (f1,i1,i2)) = (i1 -' i2) + 1 )
assume that
A1: 1 <= i2 and
A2: i2 <= i1 and
A3: i1 <= len f1 ; :: thesis: len (mid (f1,i1,i2)) = (i1 -' i2) + 1

per cases ( i1 = i2 or i2 < i1 ) by A2, XXREAL_0:1;

suppose i1 = i2 ; :: thesis: len (mid (f1,i1,i2)) = (i1 -' i2) + 1

hence len (mid (f1,i1,i2)) = (i1 -' i2) + 1 by A1, A3, Th117; :: thesis: verum

end;

suppose A4: i2 < i1 ; :: thesis: len (mid (f1,i1,i2)) = (i1 -' i2) + 1

A5: i2 <= len f1 by A2, A3, XXREAL_0:2;
1 <= i1 by A1, A2, XXREAL_0:2;
hence len (mid (f1,i1,i2)) = (i1 -' i2) + 1 by A1, A3, A4, A5, Th117; :: thesis: verum

end;

end;