let f be FinSequence; for k1, k2 being Nat st k1 <= k2 holds
smid (f,k1,k2) = mid (f,k1,k2)
let k1, k2 be Nat; ( k1 <= k2 implies smid (f,k1,k2) = mid (f,k1,k2) )
assume A1:
k1 <= k2
; smid (f,k1,k2) = mid (f,k1,k2)
then (k2 -' k1) + 1 =
(k2 - k1) + 1
by XREAL_1:233
.=
(k2 + 1) - k1
.=
(k2 + 1) -' k1
by A1, NAT_1:12, XREAL_1:233
;
hence
smid (f,k1,k2) = mid (f,k1,k2)
by A1, FINSEQ_6:def 3; verum