let D be non empty set ; 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; 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; ( 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
; len (mid (f1,i1,i2)) = (i1 -' i2) + 1
per cases
( i1 = i2 or i2 < i1 )
by A2, XXREAL_0:1;
suppose A4:
i2 < i1
;
len (mid (f1,i1,i2)) = (i1 -' i2) + 1A5:
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, FINSEQ_6:118;
verum end; end;