let n, k, d, s be Nat; :: thesis: ( s in seq (n,k) iff s + d in seq ((n + d),k) )

hereby :: thesis: ( s + d in seq ((n + d),k) implies s in seq (n,k) )

assume s in seq (n,k) ; :: thesis: s + d in seq ((n + d),k)
then ( n < s & s <= n + k ) by Th73;
then ( n + d < s + d & s + d <= (n + k) + d & (n + k) + d = (n + d) + k ) by XREAL_1:7, XREAL_1:8;
hence s + d in seq ((n + d),k) by Th73; :: thesis: verum

end;

assume s + d in seq ((n + d),k) ; :: thesis: s in seq (n,k)
then ( n + d < s + d & s + d <= (n + d) + k & (n + d) + k = (n + k) + d ) by Th73;
then ( n < s & s <= n + k ) by XREAL_1:7, XREAL_1:8;
hence s in seq (n,k) by Th73; :: thesis: verum