for k, i, j being natural Number st i <= j holds
(j + k) -' i = (j + k) - i by NAT_1:12, XREAL_1:233;