let f be FinSequence; :: thesis: for k1, k2 being Element of NAT st k1 <= k2 holds
smid f,k1,k2 = mid f,k1,k2
let k1, k2 be Element of 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:235
.= (k2 + 1) - k1
.= (k2 + 1) -' k1 by A1, NAT_1:12, XREAL_1:235 ;
hence smid f,k1,k2 = mid f,k1,k2 by A1, JORDAN3:def 1; :: thesis: verum