let f be FinSequence; :: thesis: for k1, k2 being Nat st k1 <= k2 holds
smid (f,k1,k2) = mid (f,k1,k2)
let k1, k2 be Nat; :: thesis: ( k1 <= k2 implies smid (f,k1,k2) = mid (f,k1,k2) )
assume A1: k1 <= k2 ; :: thesis: 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; :: thesis: verum